Fix. Ooops. I'd commented out the fix of r1082 / r1083.

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 73956d6080da11891c1f27d93d80819901e87eb1..47a0fa9001d308dfc5a38ca59ccbba2d0614a711 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -118,8 +118,8 @@ namespace BEEV {
             // 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);
+            if (initialSize != simp->Return_SolverMap()->size())
+               simplified_solved_InputToSAT = simp->applySubstitutionMapUntilArrays(simplified_solved_InputToSAT);
 
 
             simplified_solved_InputToSAT =