fixed a small bug in cryptominisat2

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 623b6250381425518ab0826ee08349222fce36cc..a4fe3b52cfe0f2da08dac57878eec3168681523e 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -30,7 +30,7 @@ namespace BEEV {
       {
        NewSolver.needLibraryCNFFile(bm->UserFlags.cnf_dump_filename);
       }
-
+    NewSolver.dynamicRestarts = true;
 #endif
 #ifdef SIMP
     MINISAT::SimpSolver NewSolver;

diff --git a/src/sat/cryptominisat2/BoundedQueue.h b/src/sat/cryptominisat2/BoundedQueue.h
index 595da0bba978eb18a865ac92a20ef241d5e19f0b..c4115fdeaedbf6db24bc65d12d03e9037dd6752e 100644 (file)
--- a/src/sat/cryptominisat2/BoundedQueue.h
+++ b/src/sat/cryptominisat2/BoundedQueue.h
@@ -21,10 +21,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef BoundedQueue_h
 #define BoundedQueue_h
 
-#include "Vec.h"
+#include "../mtl/Vec.h"
 
 //=================================================================================================
 
+namespace MINISAT
+{
 
 template <class T>
 class bqueue {
@@ -72,6 +74,8 @@ public:
     void clear(bool dealloc = false)   { elems.clear(dealloc); first = 0; maxsize=0; queuesize=0;sumofqueue=0;}
 
 
+};
+
 };
 
 //=================================================================================================