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 3129e414a74725227b9634980d930ec349436e58..7b53c9d594354dcfeadd794182c5d7466810da07 100644 (file)
--- 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);