From d61957bd268a51cfb8872aa3995ecd307abc3675 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 17 Sep 2009 15:40:50 +0000
Subject: [PATCH] * -t times how long sending the clauses to the SAT solver
 takes. * Remove unreachable code in the loop sending clauses to the SAT
 solver.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@239 e59a4935-1847-0410-ae03-e826735625c1
---
 src/AST/RunTimes.cpp |  2 +-
 src/AST/RunTimes.h   |  2 +-
 src/to-sat/ToSAT.cpp | 12 ++++++------
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp
index 4c30ceb..069a51d 100644
--- a/src/AST/RunTimes.cpp
+++ b/src/AST/RunTimes.cpp
@@ -15,7 +15,7 @@
 #include <utility>
 
 // BE VERY CAREFUL> Update the Category Names to match.
-std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap"};
+std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver"};
 
 namespace BEEV
 {
diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h
index a7c9fd6..832587c 100644
--- a/src/AST/RunTimes.h
+++ b/src/AST/RunTimes.h
@@ -10,7 +10,7 @@ class RunTimes
 public:
 	enum Category
 		{
-			Transforming = 0, SimplifyTopLevel, Parsing, CNFConversion, BitBlasting, Solving, BVSolver, CreateSubstitutionMap
+			Transforming = 0, SimplifyTopLevel, Parsing, CNFConversion, BitBlasting, Solving, BVSolver, CreateSubstitutionMap, SendingToSAT
 	};
 
 	static std::string CategoryNames[];
diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 55582e3..f26884b 100644
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -54,6 +54,8 @@ namespace BEEV
   {
     CountersAndStats("SAT Solver");
 
+    runTimes.start(RunTimes::SendingToSAT);
+
     //iterate through the list (conjunction) of ASTclauses cll
     BeevMgr::ClauseList::const_iterator i = cll.begin(), iend = cll.end();
 
@@ -74,6 +76,7 @@ namespace BEEV
       {
         //Clause for the SATSolver
         MINISAT::vec<MINISAT::Lit> satSolverClause;
+        satSolverClause.capacity((*i)->size());
 
         //now iterate through the internals of the ASTclause itself
         vector<const ASTNode*>::const_iterator j = (*i)->begin(), jend = (*i)->end();
@@ -104,15 +107,12 @@ namespace BEEV
         else
           {
             PrintStats(newS);
+            runTimes.stop(RunTimes::SendingToSAT);
             return false;
           }
-
-        if (!newS.simplify())
-          {
-            PrintStats(newS);
-            return false;
           }
-      }
+
+    runTimes.stop(RunTimes::SendingToSAT);
 
     // if input is UNSAT return false, else return true
     if (!newS.simplify())
-- 
2.47.3