updating the minisat restart parameters after running some experiments

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 39978ab5eaad5902f3fa4b38109276b99528a342..e8efe3d03cfd93a252665529f6365898f4c3e8b3 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -42,8 +42,8 @@ static IntOption     opt_ccmin_mode        (_cat, "ccmin-mode",  "Controls confl
 static IntOption     opt_phase_saving      (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2));
 static BoolOption    opt_rnd_init_act      (_cat, "rnd-init",    "Randomize the initial activity", false);
 static BoolOption    opt_luby_restart      (_cat, "luby",        "Use the Luby restart sequence", true);
-static IntOption     opt_restart_first     (_cat, "rfirst",      "The base restart interval", 100, IntRange(1, INT32_MAX));
-static DoubleOption  opt_restart_inc       (_cat, "rinc",        "Restart interval increase factor", 2, DoubleRange(1, false, HUGE_VAL, false));
+static IntOption     opt_restart_first     (_cat, "rfirst",      "The base restart interval", 25, IntRange(1, INT32_MAX));
+static DoubleOption  opt_restart_inc       (_cat, "rinc",        "Restart interval increase factor", 3, DoubleRange(1, false, HUGE_VAL, false));
 static DoubleOption  opt_garbage_frac      (_cat, "gc-frac",     "The fraction of wasted memory allowed before a garbage collection is triggered",  0.20, DoubleRange(0, false, HUGE_VAL, false));
 
 

diff --git a/src/prop/sat.h b/src/prop/sat.h
index 8581cd9a07c1342ac6a4ad644cfe029b8b86b59f..7229b35657dfdda76f36a60a07f54d5e5b12ab8d 100644 (file)
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -233,8 +233,6 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
   d_minisat = new Minisat::SimpSolver(this, d_context);
   // Setup the verbosity
   d_minisat->verbosity = (options->verbosity > 0) ? 1 : -1;
-  // Do not delete the satisfied clauses, just the learnt ones
-  d_minisat->remove_satisfied = false;
 
   // No random choices
   if(Debug.isOn("no_rnd_decisions")){