From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 7 Dec 2009 17:45:45 +0000 (+0000)
Subject: minor edit
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=c1a062a72354f9d34cb2d9326b41059f177a3852;p=francis%2Fstp.git

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 53b0580..dac3120 100644
--- 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 884a990..2761230 100644
--- 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 1d3cbc4..5d099a5 100644
--- 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 0427379..c6be352 100644
--- 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