From eb705ce752bdd4585e5db9424c738e9cc905f79b Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 25 Apr 2012 13:49:31 +0000 Subject: [PATCH] Fix. didn't work properly for 1 bit division. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1656 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/simplifier.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index edcefae..e6bd137 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -2775,9 +2775,9 @@ namespace BEEV break; } unsigned int nlz= numberOfLeadingZeroes(inputterm[0]); + nlz = std::min(inputValueWidth-1,nlz); if (nlz > 0) { - nlz = std::min(inputValueWidth-1,nlz); int rest = inputValueWidth-nlz; ASTNode low = _bm->CreateBVConst(32,rest); ASTNode high =_bm->CreateBVConst(32,inputValueWidth-1); -- 2.47.3