minor edit

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

diff --git a/src/AST/UsefulDefs.h b/src/AST/UsefulDefs.h
index 27e1399b0aacf94ac32d69902ee81e5282b78542..e23c2fff270160df40c3282410ac0a37bb6709e4 100644 (file)
--- a/src/AST/UsefulDefs.h
+++ b/src/AST/UsefulDefs.h
@@ -46,7 +46,7 @@
 #define HASHMULTISET hash_multiset
 #define INITIAL_TABLE_SIZE 100
 #define CLAUSAL_ABSTRACTION_CUTOFF 0.5
-#define CLAUSAL_BUCKET_LIMIT 3
+#define CLAUSAL_BUCKET_LIMIT 4
 
 using namespace std;
 namespace BEEV {

diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp
index 984b8f4aaac51aea4f33110aec803d497de6800a..a0b4be6d5b75d1b6bad7aed4bd9afd4528e2e954 100644 (file)
--- a/src/to-sat/CallSAT.cpp
+++ b/src/to-sat/CallSAT.cpp
@@ -54,11 +54,11 @@ namespace BEEV
     for(int count=1;it!=itend;it++, count++)
       {
         ClauseList *cl = (*it).second;
-//     if(CLAUSAL_BUCKET_LIMIT == count)
-//       {
-//         sat = toSATandSolve(SatSolver,*cl, false, true);
-//       }
-//     else
+       // if(CLAUSAL_BUCKET_LIMIT == count)
+       //        {
+       //          sat = toSATandSolve(SatSolver,*cl, false, true);
+       //        }
+       //      else
          {
            sat = toSATandSolve(SatSolver,*cl);
          }