Bugfix. An assertion error would be produced because a term was not simplified.

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index e5bdf7e6d460a4b9128fbc0e9082fe5374b87953..73956d6080da11891c1f27d93d80819901e87eb1 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -103,13 +103,24 @@ namespace BEEV {
         if(bm->UserFlags.optimize_flag) 
           {
 
+               int initialSize = simp->Return_SolverMap()->size();
+
             simplified_solved_InputToSAT = 
                simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer);
 
-            //printf("##################################################\n");
             bm->ASTNodeStats("after pure substitution: ", 
                              simplified_solved_InputToSAT);
 
+            // Imagine:
+            // The simplifier simplifies (0 + T) to T
+            // Then bvsolve introduces (0 + T)
+            // Then CreateSubstitutionMap decides T maps to a constant, but leaving another (0+T).
+            // When we go to simplify (0 + T) will still be in the simplify cache, so will be mapped to T.
+            // But it shouldn't be T, it should be a constant.
+            // Applying the substitution map fixes this unusual case... expensively...
+           // if (initialSize != simp->Return_SolverMap()->size())
+            // simplified_solved_InputToSAT = simp->applySubstitutionMapUntilArrays(simplified_solved_InputToSAT);
+
 
             simplified_solved_InputToSAT = 
               simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT,