When sending clauses to the SAT solver, create fewer objects. This speeds up sending...

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

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 8c9513597ace498cd3fd43ce9c77e977271d00bd..72a23d8c4eaf5d5ce1663ddba765da705b10b7ce 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -91,14 +91,14 @@ namespace BEEV
       }
 
        ClauseContainer& cc = *cll.asList();
+    //Clause for the SATSolver
+       MINISAT::vec<MINISAT::Lit> satSolverClause;
 
     //iterate through the list (conjunction) of ASTclauses cll
     ClauseContainer::const_iterator i = cc.begin(), iend = cc.end();
     for (int count=0, flag=0; i != iend; i++)
       {
-        //Clause for the SATSolver
-        MINISAT::vec<MINISAT::Lit> satSolverClause;
-        satSolverClause.capacity((*i)->size());        
+        satSolverClause.clear();
         vector<const ASTNode*>::const_iterator j    = (*i)->begin(); 
         vector<const ASTNode*>::const_iterator jend = (*i)->end();      
         //ASTVec  clauseVec;