From: msoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 2 Jul 2010 14:49:00 +0000 (+0000)
Subject: Updating CMS2 to get rid of a small bug
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=3628a6fd5b9c65a9e672f543192a14e951348277;p=francis%2Fstp.git

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 94e1cc9..75032fe 100644
--- 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 fa1d8b6..1afa7cf 100644
--- 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 c99107a..1eeeba0 100644
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,2 +1,2 @@
 CryptoMiniSat
-GIT revision: 8b7c29dd9b4650dcc40a7a522ac51137d2a017e5
+GIT revision: 65b49fef48c45a6d516f159f6a5bbf82f3dd5981