From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 2 Feb 2011 00:55:06 +0000 (+0000)
Subject: Fix. Apply substitutions in another place to avoid an assertion error.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=52902491375b55d6d094fe8bae4ade251f27eeb6;p=francis%2Fstp.git

Fix. Apply substitutions in another place to avoid an assertion error.

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 3129e41..7b53c9d 100644
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -174,9 +174,17 @@ namespace BEEV {
 
         if(bm->UserFlags.optimize_flag) 
           {
-            simplified_solved_InputToSAT = 
+        	int initialSize = simp->Return_SolverMap()->size();
+
+        	simplified_solved_InputToSAT =
             	simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer);
 
+			if (initialSize != simp->Return_SolverMap()->size())
+			{
+				simplified_solved_InputToSAT = simp->applySubstitutionMap(simplified_solved_InputToSAT);
+				simp->haveAppliedSubstitutionMap();
+			}
+
             bm->ASTNodeStats("after pure substitution: ",
                              simplified_solved_InputToSAT);