From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 26 Sep 2009 19:37:00 +0000 (+0000)
Subject: git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=abb93f39a0d012becb22340c8d45a28048acfa36;p=francis%2Fstp.git

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

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 5055d1e..a6bb14d 100644
--- 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);