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 b5ea9cb86728c9eb8b69b6875b713c4d9cb5b5e1..7d67fe881eb2a3e4b9d45e776362d6b70341df41 100644 (file)
--- 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 dc7952decf115494769612f61247bd49e834054c..8c9513597ace498cd3fd43ce9c77e977271d00bd 100644 (file)
--- 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);
       }