From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 6 Nov 2009 21:20:09 +0000 (+0000)
Subject: minor changes
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=7d5187f09ff77a68719ab95b1b026afd10038f1c;p=francis%2Fstp.git

minor changes

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

diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp
index 7d9ff84..a397003 100644
--- a/src/to-sat/CallSAT.cpp
+++ b/src/to-sat/CallSAT.cpp
@@ -84,15 +84,14 @@ namespace BEEV
     ClauseList* xorcl = cm->ReturnXorClauses();
 #endif
 
-    ClauseBuckets * cb = Sort_ClauseList_IntoBuckets(cl);
+    ClauseBuckets * cb = Sort_ClauseList_IntoBuckets(cl);    
+    bool sat = CallSAT_On_ClauseBuckets(SatSolver, cb);    
     //bool sat = toSATandSolve(SatSolver, *cl);
-    bool sat = CallSAT_On_ClauseBuckets(SatSolver, cb);
 
     for (ClauseBuckets::iterator it = cb->begin(); it != cb->end(); it++)
-    	delete it->second;
+      delete it->second;
     delete cb;
 
-
     if(!sat)
       {
 	return sat;
diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index faead43..75f3960 100644
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -1276,7 +1276,8 @@ namespace BEEV
 			   ((*(info[*it]->clausespos))[0])->end());
       }
     doRenamingPosXor(varphi);
-    //doRenamingPos(varphi, defs);
+    //ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs);
+    //info[varphi]->clausespos = psi;    
     ASTNode varXorNode = GetNodeFrom_SINGLETON(info[varphi]->clausespos);
     ASTNode NotVarXorNode = bm->CreateNode(NOT, varXorNode);
     xor_clause->push_back(ASTNodeToASTNodePtr(NotVarXorNode));
@@ -1842,7 +1843,9 @@ namespace BEEV
     if (bm->UserFlags.stats_flag)
       {
         cerr << "Number of clauses:" << defs->size() << endl;
-        //PrintClauseList(cout, *defs);
+        PrintClauseList(cout, *defs);
+	cerr << "Number of xor-clauses:" << clausesxor->size() << endl;
+	PrintClauseList(cout, *clausesxor);
       }
 
     return defs;
diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index a95f36a..949d064 100644
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -89,7 +89,8 @@ namespace BEEV
         //        }
 #ifdef CRYPTOMINISAT
 	if(add_xor_clauses)
-	  {
+	  {	    
+	    //cout << "addXorClause:\n";
 	    newS.addXorClause(satSolverClause, false, 0, "z");
 	  }
 	else