Important Bugfix. The recently introduced bvmod simplifications are wrong.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1611 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 0da30f95bcac2e0b5223352406c970ce9376f623..e576f72e28832dbd998079fcc18ae28aad3d19ba 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -2832,7 +2832,7 @@ namespace BEEV
            ASTNode div = nf->CreateTerm(BVMOD,rest,top,bottom);
            div = nf->CreateTerm(BVCONCAT,inputValueWidth,_bm->CreateZeroConst(inputValueWidth-rest),div);
 
-           output = nf->CreateTerm(ITE, inputValueWidth, cond, div, _bm->CreateZeroConst(inputValueWidth));
+           output = nf->CreateTerm(ITE, inputValueWidth, cond, div, inputterm[0]);
            break;
          }