From 52902491375b55d6d094fe8bae4ade251f27eeb6 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 2 Feb 2011 00:55:06 +0000
Subject: [PATCH] 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
---
 src/STPManager/STP.cpp | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

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);
 
-- 
2.47.3