From: msoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 2 Jul 2010 14:58:09 +0000 (+0000)
Subject: Correcting small bug in CMS2
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=5f6e2282a5c516f78b82560c7d7ca9f46b0c8b8e;p=francis%2Fstp.git

Correcting small bug in CMS2

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

diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index 1eeeba0..37b8c68 100644
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,2 +1,2 @@
 CryptoMiniSat
-GIT revision: 65b49fef48c45a6d516f159f6a5bbf82f3dd5981
+GIT revision: 819a9f4377ef8c9ed0f4b493517a84c853b30a98
diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp
index 3fbf609..fd82cde 100644
--- a/src/sat/cryptominisat2/VarReplacer.cpp
+++ b/src/sat/cryptominisat2/VarReplacer.cpp
@@ -88,11 +88,15 @@ const bool VarReplacer::performReplaceInternal()
     #endif
     
     Var var = 0;
-    const vec<char>& removedVars = solver.xorSubsumer->getVarElimed();
-    const vec<lbool>& removedVars2 = solver.partHandler->getSavedState();
-    const vec<char>& removedVars3 = solver.subsumer->getVarElimed();
+    const vec<char>* removedVars = solver.doXorSubsumption ? &solver.xorSubsumer->getVarElimed() : NULL;
+    const vec<lbool>* removedVars2 = solver.doPartHandler ?  &solver.partHandler->getSavedState() : NULL;
+    const vec<char>* removedVars3 = solver.doSubsumption ? &solver.subsumer->getVarElimed() : NULL;
     for (vector<Lit>::const_iterator it = table.begin(); it != table.end(); it++, var++) {
-        if (it->var() == var || removedVars[it->var()] || removedVars2[it->var()] != l_Undef || removedVars3[it->var()]) continue;
+        if (it->var() == var
+            || (removedVars != NULL && (*removedVars)[it->var()])
+            || (removedVars2 != NULL && (*removedVars2)[it->var()] != l_Undef)
+            || (removedVars3!= NULL && (*removedVars3)[it->var()])
+        ) continue;
         #ifdef VERBOSE_DEBUG
         cout << "Setting var " << var+1 << " to a non-decision var" << endl;
         #endif