From a52bf415dcc89e2ab1f1faa8a318a51e01ef753e Mon Sep 17 00:00:00 2001
From: msoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 19 Apr 2010 10:12:30 +0000
Subject: [PATCH] Fixing CMS2's library debug routine

It didn't work correctly when re-adding removed clauses: variable
elimination, conglomeration, and part-handling all dumped data, but they
shouldn't have been

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@693 e59a4935-1847-0410-ae03-e826735625c1
---
 src/sat/cryptominisat2/Conglomerate.cpp | 3 +++
 src/sat/cryptominisat2/PartHandler.cpp  | 3 +++
 src/sat/cryptominisat2/Subsumer.cpp     | 5 ++++-
 src/sat/cryptominisat2/VERSION          | 2 +-
 4 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp
index 1868051..770c88a 100644
--- a/src/sat/cryptominisat2/Conglomerate.cpp
+++ b/src/sat/cryptominisat2/Conglomerate.cpp
@@ -502,12 +502,15 @@ const bool Conglomerate::addRemovedClauses()
         for(Lit *l = c.getData(), *end2 = c.getDataEnd(); l != end2 ; l++)
             *l = l->unsign();
         
+        FILE* backup_libraryCNFfile = solver.libraryCNFFile;
+        solver.libraryCNFFile = NULL;
         if (!solver.addXorClause(c, c.xor_clause_inverted(), c.getGroup())) {
             for (;it != end; it++)
                 free(&c);
             calcAtFinish.clear();
             return false;
         }
+        solver.libraryCNFFile = backup_libraryCNFfile;
         free(&c);
     }
     calcAtFinish.clear();
diff --git a/src/sat/cryptominisat2/PartHandler.cpp b/src/sat/cryptominisat2/PartHandler.cpp
index c7f666a..c1773bd 100644
--- a/src/sat/cryptominisat2/PartHandler.cpp
+++ b/src/sat/cryptominisat2/PartHandler.cpp
@@ -286,6 +286,8 @@ void PartHandler::addSavedState()
 
 void PartHandler::readdRemovedClauses()
 {
+    FILE* backup_libraryCNFfile = solver.libraryCNFFile;
+    solver.libraryCNFFile = NULL;
     for (Clause **it = clausesRemoved.getData(), **end = clausesRemoved.getDataEnd(); it != end; it++) {
         solver.addClause(**it, (*it)->getGroup());
         assert(solver.ok);
@@ -300,6 +302,7 @@ void PartHandler::readdRemovedClauses()
         assert(solver.ok);
     }
     xorClausesRemoved.clear();
+    solver.libraryCNFFile = backup_libraryCNFfile;
 }
 
 }; //NAMESPACE MINISAT
diff --git a/src/sat/cryptominisat2/Subsumer.cpp b/src/sat/cryptominisat2/Subsumer.cpp
index 40152cd..cf711e4 100644
--- a/src/sat/cryptominisat2/Subsumer.cpp
+++ b/src/sat/cryptominisat2/Subsumer.cpp
@@ -90,12 +90,15 @@ const bool Subsumer::unEliminate(const Var var)
     solver.setDecisionVar(var, true);
     var_elimed[var] = false;
     numElimed--;
+    FILE* backup_libraryCNFfile = solver.libraryCNFFile;
+    solver.libraryCNFFile = NULL;
     for (vector<vector<Lit> >::iterator it2 = it->second.begin(), end2 = it->second.end(); it2 != end2; it2++) {
         tmp.clear();
         tmp.growTo(it2->size());
-        memcpy(tmp.getData(), &((*it2)[0]), sizeof(Lit)*it2->size());  //*it2 is never empty
+        std::copy(it2->begin(), it2->end(), tmp.getData());
         solver.addClause(tmp);
     }
+    solver.libraryCNFFile = backup_libraryCNFfile;
     elimedOutVar.erase(it);
     
     if (!solver.ok) return false;
diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index a01b800..5069102 100644
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,2 +1,2 @@
 CryptoMiniSat
-GIT revision: cebb0caeb2928eb96e114864c580c341e904245d
+GIT revision: 8dccdf7df73e761aba7a8c9a0251e2327a9bd97c
-- 
2.47.3