Bugfix. STP returned the wrong answer when something like bitwidth of 1: (0 = (1...

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

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index fa3d4cd0f2d43810a09fdcf7ca0b8ab8f0f27df9..44d85d36cbc0b12c98bd16da594e6d1f7412afff 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -40,6 +40,7 @@ namespace BEEV
 {
        const bool flatten_ands = true;
        const bool sort_extracts_last = false;
+       const bool debug_bvsolver = false;
 
   //check the solver map for 'key'. If key is present, then return the
   //value by reference in the argument 'output'
@@ -262,6 +263,13 @@ namespace BEEV
       _bm->CreateTerm(BVPLUS, lhs.GetValueWidth(), o) : 
       o[0];
 
+    if (debug_bvsolver)
+      {
+        cerr << "Initial:" << eq;
+        cerr << "Chosen Monomial:" << outmonom;
+        cerr << "Output LHS:" << modifiedlhs;
+      }
+
     // can be SYMBOL or (BVUMINUS SYMBOL) or (BVMULT ODD_BVCONST SYMBOL) or
     // (BVMULT ODD_BVCONST (EXTRACT SYMBOL BV_CONST ZERO))
     return outmonom;
@@ -742,8 +750,8 @@ namespace BEEV
         don't have time. Trev.
                  */
 #if 1
-      ASTNode aaa = (any_solved && EQ == it->GetKind()) ? _simp->applySubstitutionMapUntilArrays(*it) : *it;
-#else
+        ASTNode aaa = (any_solved && EQ == it->GetKind()) ? _simp->SimplifyFormula(_simp->applySubstitutionMapUntilArrays(*it),false,NULL) : *it;
+      #else
           ASTNode aaa = *it;
 
           if (any_solved && EQ == aaa.GetKind())
@@ -871,6 +879,8 @@ namespace BEEV
 
         if (BVCONST == itk)
           {
+            assert(savetheconst == rhs); // Returns the wrong result if there are >1 constants.
+
             //check later if the constant is even or not
             savetheconst = aaa;
             continue;

diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
index f8848abd4ac0dce6d8496f546b5f25dd50c54a1f..b81f023343b9f71812a12e8171d1195ab4408eab 100644 (file)
--- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp
+++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
@@ -339,14 +339,19 @@ namespace simplifier
             }
         }
 
-
      // Write the constants into the main graph.
       ASTNodeMap cache;
       ASTNode result = SubstitutionMap::replace(top, fromTo, cache,nf);
 
       if (0 != toConjoin.size())
         {
-          result = nf->CreateNode(AND, result, toConjoin); // conjoin the new conditions.
+          // It doesn't happen very often. But the "toConjoin" might contain a variable
+          // that was added to the substitution map (because the value was determined just now
+          // during propagation.
+          ASTNode conjunct = (1 == toConjoin.size())? toConjoin[0]: nf->CreateNode(AND,toConjoin);
+          conjunct = simplifier->applySubstitutionMap(conjunct);
+
+          result = nf->CreateNode(AND, result, conjunct); // conjoin the new conditions.
         }