minor edit

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

diff --git a/Makefile b/Makefile
index 53b0580b62751ee226cbd9d21ebfeacbc701147a..dac312054d6553476e4f26b6b8fbc077f8b85a66 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -226,7 +226,7 @@ regresssmtbasic:
        @echo "*********************************************************" \
           | tee -a $(SMTBASIC_LOG)
 
-SYNTHESIS_LOG = `date +%Y-%m-%d`"-regress-cvc.log"
+SYNTHESIS_LOG = `date +%Y-%m-%d`"-regress-synthesis.log"
 .PHONY: regresssyn
 regresssyn:
        @echo "*********************************************************" \

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 884a99055b66cab1ede8c441985122bd42bb00c8..2761230c41a8fff39a7044f7171b36942287bee1 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -23,16 +23,16 @@ CFLAGS_BASE   = $(OPTIMIZE)
 #SOLVER_INCLUDE = ../sat/cryptominisat
 
 # OPTION to compile CRYPTOMiniSAT version 2.x
-CRYPTOMINISAT2 = true
-CFLAGS_BASE    = $(OPTIMIZE) -DCRYPTOMINISAT2
-MTL            = ../sat/cryptominisat2/mtl
-SOLVER_INCLUDE = ../sat/cryptominisat2
+#CRYPTOMINISAT2 = true
+#CFLAGS_BASE    = $(OPTIMIZE) -DCRYPTOMINISAT2
+#MTL            = ../sat/cryptominisat2/mtl
+#SOLVER_INCLUDE = ../sat/cryptominisat2
 
 # OPTION to compile MiniSAT
-#CORE          = true
-#CFLAGS_BASE   = $(OPTIMIZE) -DCORE
-#MTL            = ../sat/mtl
-#SOLVER_INCLUDE = ../sat/core
+CORE          = true
+CFLAGS_BASE   = $(OPTIMIZE) -DCORE
+MTL            = ../sat/mtl
+SOLVER_INCLUDE = ../sat/core
 
 
 # OPTION to compile UNSOUND MiniSAT

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 1d3cbc4e6b16d462ce64bc19401377b27f82e155..5d099a5d97b80a7ffc51f08ea26061538a7068a2 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -90,7 +90,7 @@ int main(int argc, char ** argv) {
   helpstring +=  
     "-h  : help\n";
   helpstring +=  
-    "-i <random_seed>  : Randomize STP's satisfiable output. Random_seed is an integer >= 0\n";
+    "-i <random_seed>  : Randomize STP's satisfiable output. Random_seed is an integer >= 0. Needs CRYPTOMINISAT2\n";
   helpstring +=  
     "-m  : use the SMTLIB parser\n";
   helpstring +=  

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 0427379c26d6d10c45021602a5597699f1c85c50..c6be352b8714dd217f665162e3b8b7ef360060ee 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -82,10 +82,12 @@ namespace BEEV
 
     if(bm->UserFlags.random_seed_flag)
       {
+#ifdef CRYPTOMINISAT2
        newSolver.setSeed(bm->UserFlags.random_seed);
        //cerr << "We have set the seed value to "
        //   << bm->UserFlags.random_seed 
        //   << endl;
+#endif
       }
 
     if(bm->UserFlags.print_cnf_flag)
@@ -147,7 +149,7 @@ namespace BEEV
             bm->GetRunTimes()->start(RunTimes::Solving);
 
 #if defined CRYPTOMINISAT2
-           newSolver.set_gaussian_decision_until(100);
+           newSolver.set_gaussian_decision_until(300);
            newSolver.performReplace = false;
            newSolver.xorFinder = false;
 #endif