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

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 770273c5ad59a1b674e8cb3248b3282d2138e91f..fd03be4f98d1722fc3e496a0d437c6a88ca7a4a6 100644 (file)
--- 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 da3aaeeedd3ee6128f4eb91b5cea5dbeac53efc2..80f92b3f230f36609662f1de587a9679b6316e26 100644 (file)
--- 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 446db1afeb4da510cf2c6fef6a0122b92c7003bf..8158a5f68b92a4052bae72d9fa58d3610dad7cb9 100644 (file)
--- 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 e9c18734c4691c75c66f330d8e39a0d3df7956e3..7bf23c21fe425ce2f4e85d279968ddcd07d35f42 100644 (file)
--- 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 d2ac1e980eb6a96f2a871ac88382cfab97b8d981..4d7f9f69ab02987844887674d5ce6ca628d50d1a 100644 (file)
--- 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
       }