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 1eeeba07894d3eb37ba8d13ea94ffcb6b1ade88e..37b8c68597501831dc3573b0cb74be20ee9a130b 100644 (file)
--- 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 3fbf60938934b267c1ab8dda263f36b32b196491..fd82cdefa08dc3e961c4aa88dcc25a456a16941c 100644 (file)
--- 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