git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk...

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 5055d1eafdeba986e419de2bd65de7d9a62e7884..a6bb14d2eef69c9dedb27047a76b936d79de8d67 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -1022,31 +1022,6 @@ namespace BEEV
       }
 
     TermsAlreadySeenMap.clear();
-    // do
-    //       {
-    //         inputToSAT = simplified_solved_InputToSAT;
-    
-    //         if(optimize_flag) 
-    //           {
-    //             runTimes.start(RunTimes::CreateSubstitutionMap);
-    //             simplified_solved_InputToSAT = 
-    //               CreateSubstitutionMap(simplified_solved_InputToSAT);
-    //             runTimes.stop(RunTimes::CreateSubstitutionMap);
-    //             ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
-    
-    //             simplified_solved_InputToSAT = 
-    //               SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
-    //             ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
-    //           }
-    
-    //         if(wordlevel_solve_flag)
-    //           {
-    //             simplified_solved_InputToSAT = 
-    //               bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
-    //             ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
-    //           }
-    //       } while (inputToSAT != simplified_solved_InputToSAT);
-    
     if (start_abstracting)
       {
         ASTNodeStats("After abstraction: ", simplified_solved_InputToSAT);