Updating CMS2 to get rid of a small bug

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

diff --git a/src/sat/cryptominisat2/PartHandler.cpp b/src/sat/cryptominisat2/PartHandler.cpp
index 94e1cc9978e8543d1689549ea287cbc8ae97b818..75032fe2c8772a93cc9b151c5a8f5cfc3a005db7 100644 (file)
--- a/src/sat/cryptominisat2/PartHandler.cpp
+++ b/src/sat/cryptominisat2/PartHandler.cpp
@@ -92,6 +92,8 @@ const bool PartHandler::handle()
         newSolver.doSubsumption = false;
         newSolver.doXorSubsumption = false;
         newSolver.doPartHandler = false;
+        newSolver.subsumeWithNonExistBinaries = false;
+        newSolver.regularSubsumeWithNonExistBinaries = false;
 
         std::sort(vars.begin(), vars.end());
         uint32_t i2 = 0;

diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index fa1d8b6dba5528f6d831e160a746d05fd5996bf1..1afa7cf0dc3d9a34f9e7e4ed31e88a38d019b32b 100644 (file)
--- a/src/sat/cryptominisat2/Solver.cpp
+++ b/src/sat/cryptominisat2/Solver.cpp
@@ -213,7 +213,7 @@ Var Solver::newVar(bool dvar)
     
     varReplacer->newVar();
     if (doPartHandler) partHandler->newVar();
-    if (doSubsumption) subsumer->newVar();
+    if (doSubsumption || subsumeWithNonExistBinaries || regularSubsumeWithNonExistBinaries) subsumer->newVar();
     if (doXorSubsumption) xorSubsumer->newVar();
 
     insertVarOrder(v);

diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index c99107a6d56f9aeb184059bc4eb91ce917d6642d..1eeeba07894d3eb37ba8d13ea94ffcb6b1ade88e 100644 (file)
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,2 +1,2 @@
 CryptoMiniSat
-GIT revision: 8b7c29dd9b4650dcc40a7a522ac51137d2a017e5
+GIT revision: 65b49fef48c45a6d516f159f6a5bbf82f3dd5981