From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 21 Jan 2010 21:47:07 +0000 (+0000)
Subject: fixed an important problem with YACC STACK DEPTH. It was too low previously. Now... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=9c685df9d733b2eac17750210eaf4980afac01d1;p=francis%2Fstp.git

fixed an important problem with YACC STACK DEPTH. It was too low previously. Now fixed.

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

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 770273c..fd03be4 100644
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -9,7 +9,7 @@
 # ********************************************************************/
 
 #OPTIMIZE     = -g -pg            # Debugging and gprof-style profiling
-OPTIMIZE      = -g                # Debugging
+#OPTIMIZE      = -g                # Debugging
 #OPTIMIZE      = -O3 -fPIC         # Maximum optimization
 #OPTIMIZE      = -O3 -march=native -fomit-frame-pointer # Maximum optimization
 #OPTIMIZE      = -O3 -march=native -DNDEBUG -DLESSBYTES_PERNODE
@@ -18,16 +18,16 @@ OPTIMIZE      = -O3               # Maximum optimization
 CFLAGS_BASE   = $(OPTIMIZE)
 
 # 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
 #UNSOUND       = true
diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index da3aaee..80f92b3 100644
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -90,10 +90,15 @@ namespace BEEV
                           CounterExampleMap[s] = ASTFalse;
                         else
                           {
-                            int seed = 10000;
-                            srand(seed);
-                            CounterExampleMap[s] = 
-                              (rand() > seed) ? ASTFalse : ASTTrue;
+			    if(bm->UserFlags.random_seed_flag)
+			      {
+				int seed = bm->UserFlags.random_seed;
+				srand(seed);
+				CounterExampleMap[s] = 
+				  (rand() > seed) ? ASTFalse : ASTTrue;
+			      }
+			    else
+			      CounterExampleMap[s] = ASTFalse;
                           }
                       }
                   }
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 446db1a..8158a5f 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -164,6 +164,7 @@ int main(int argc, char ** argv) {
 	    case 'i':
 	      bm->UserFlags.random_seed_flag = true;
               bm->UserFlags.random_seed = atoi(argv[++i]);
+	      //cerr << "Random seed is: " << bm->UserFlags.random_seed << endl;
 	      if(!(0 <= bm->UserFlags.random_seed))
 		{
 		  FatalError("Random Seed should be an integer >= 0\n");
diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index e9c1873..7bf23c2 100644
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -18,7 +18,7 @@
 #undef __GNUC_MINOR__
   
 #define YYLTYPE_IS_TRIVIAL 1
-#define YYMAXDEPTH 10485760
+#define YYMAXDEPTH 1048576000
 #define YYERROR_VERBOSE 1
 #define YY_EXIT_FAILURE -1
 #define YYPARSE_PARAM AssertsQuery
diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index d2ac1e9..4d7f9f6 100644
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -84,9 +84,10 @@ namespace BEEV
       {
 #ifdef CRYPTOMINISAT2
 	newSolver.setSeed(bm->UserFlags.random_seed);
-	//cerr << "We have set the seed value to "
-	//   << bm->UserFlags.random_seed 
-	//   << endl;
+	//newSolver.greedyUnbound = true;
+	// 	cerr << "We have set the seed value to "
+	// 	     << bm->UserFlags.random_seed 
+	// 	     << endl;
 #endif
       }