From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 24 Jan 2011 14:28:17 +0000 (+0000)
Subject: Fix. Ooops. I'd commented out the fix of r1082 / r1083.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=5fe77c3cb1b3485f8128e0f184b6027be042740a;p=francis%2Fstp.git

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 73956d6..47a0fa9 100644
--- 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 =