From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 28 Apr 2010 12:33:15 +0000 (+0000)
Subject: Bugfix. Refactoring of ToCNF broke some ifdef CRYPTOMINISAT2 code.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=2dba99d28c1911c07871162beaf3265206afafaa;p=francis%2Fstp.git

Bugfix. Refactoring of ToCNF broke some ifdef CRYPTOMINISAT2 code.


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

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index b5ea9cb..7d67fe8 100644
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -1163,8 +1163,8 @@ namespace BEEV
         //doRenamingPos(*it, defs);
         doRenamingNeg(*it, defs);
         xor_clause->insert(xor_clause->end(), 
-                           ((*(info[*it]->clausespos))[0])->begin(),
-                           ((*(info[*it]->clausespos))[0])->end());
+                           ((*(info[*it]->clausespos)).asList()->front())->begin(),
+                           ((*(info[*it]->clausespos)).asList()->front())->end());
 	if(renameAllSiblings)
           {
 	    assert(info[*it]->clausespos->size() ==1);
@@ -1542,9 +1542,10 @@ namespace BEEV
         //XOR node doRenamingPos(*it, defs);
         //doRenamingPos(*it, defs);
         doRenamingNeg(*it, defs);
+
         xor_clause->insert(xor_clause->end(), 
-                           ((*(info[*it]->clausespos))[0])->begin(),
-                           ((*(info[*it]->clausespos))[0])->end());
+                           ((*(info[*it]->clausespos)).asList()->front())->begin(),
+                           ((*(info[*it]->clausespos)).asList()->front())->end());
       }
     doRenamingPosXor(varphi);
     //ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs);
diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index dc7952d..8c95135 100644
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -338,7 +338,7 @@ namespace BEEV
       }
 
 #if defined CRYPTOMINISAT2
-    if(!xorcl->empty())
+    if(!xorcl->asList()->empty())
       {
         sat = toSATandSolve(SatSolver, *xorcl, true);
       }