From: vijay_ganesh Date: Tue, 8 Dec 2009 20:50:21 +0000 (+0000) Subject: fixed a small bug in cryptominisat2 X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=37ae56c23c4c94f6a43ce3051a9f468c1c2c39d8;p=francis%2Fstp.git 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 623b625..a4fe3b5 100644 --- 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 595da0b..c4115fd 100644 --- 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 bqueue { @@ -72,6 +74,8 @@ public: void clear(bool dealloc = false) { elems.clear(dealloc); first = 0; maxsize=0; queuesize=0;sumofqueue=0;} +}; + }; //=================================================================================================