From: msoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 2 Jul 2010 14:35:49 +0000 (+0000)
Subject: Updating CryptoMiniSat2 to fix some minor bugs
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=bd7dace0744601b077892f3da289abc46ede5015;p=francis%2Fstp.git

Updating CryptoMiniSat2 to fix some minor bugs

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

diff --git a/src/sat/cryptominisat2/Clause.h b/src/sat/cryptominisat2/Clause.h
index ec515fc..c7faf60 100644
--- a/src/sat/cryptominisat2/Clause.h
+++ b/src/sat/cryptominisat2/Clause.h
@@ -24,6 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifdef _MSC_VER
 #include <msvc/stdint.h>
 #else
+#include "SmallPtr.h"
 #include <stdint.h>
 #endif //_MSC_VER
 
diff --git a/src/sat/cryptominisat2/ClauseAllocator.cpp b/src/sat/cryptominisat2/ClauseAllocator.cpp
index 826ae72..f0d7fa6 100644
--- a/src/sat/cryptominisat2/ClauseAllocator.cpp
+++ b/src/sat/cryptominisat2/ClauseAllocator.cpp
@@ -37,6 +37,13 @@ ClauseAllocator::ClauseAllocator() :
     clausePoolBin(sizeof(Clause) + 2*sizeof(Lit))
 {}
 
+ClauseAllocator::~ClauseAllocator()
+{
+    for (uint32_t i = 0; i < dataStarts.size(); i++) {
+        free(dataStarts[i]);
+    }
+}
+
 template<class T>
 Clause* ClauseAllocator::Clause_new(const T& ps, const unsigned int group, const bool learnt)
 {
diff --git a/src/sat/cryptominisat2/ClauseAllocator.h b/src/sat/cryptominisat2/ClauseAllocator.h
index 71c479f..db38eea 100644
--- a/src/sat/cryptominisat2/ClauseAllocator.h
+++ b/src/sat/cryptominisat2/ClauseAllocator.h
@@ -44,6 +44,7 @@ typedef uint32_t ClauseOffset;
 class ClauseAllocator {
     public:
         ClauseAllocator();
+        ~ClauseAllocator();
         
         template<class T>
         Clause* Clause_new(const T& ps, const uint group, const bool learnt = false);
diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index cb7ee3e..fa1d8b6 100644
--- a/src/sat/cryptominisat2/Solver.cpp
+++ b/src/sat/cryptominisat2/Solver.cpp
@@ -2258,7 +2258,9 @@ lbool Solver::solve(const vec<Lit>& assumps)
 #endif
         
         if (subsumer->getNumElimed() || xorSubsumer->getNumElimed()) {
-            std::cout << "c Solution needs extension. Extending." << std::endl;
+            if (verbosity >= 1) {
+                std::cout << "c Solution needs extension. Extending." << std::endl;
+            }
             Solver s;
             s.doSubsumption = false;
             s.performReplace = false;
diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index 75dc444..0e6fa53 100644
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,2 +1,2 @@
 CryptoMiniSat
-GIT revision: d1a89e619d41131629e6c4e74f9424453225ba2d
+GIT revision: fda5b5a9d05a6b2ddfa4659671d6232173c30e0e