Remove refineConflicts option (#8129)

Was introduced in 8a0c056.

Fixes #8119.

diff --git a/src/options/prop_options.toml b/src/options/prop_options.toml
index efdc89c3e538f51134ee503a6d37fe4ce62d0bf0..8404ab9202973433732a1f8f04ddffcb3d0c80c6 100644 (file)
--- a/src/options/prop_options.toml
+++ b/src/options/prop_options.toml
@@ -55,14 +55,6 @@ name   = "SAT Layer"
   minimum    = "0.0"
   help       = "sets the restart interval increase factor for the sat solver (F=3.0 by default)"
 
-[[option]]
-  name       = "sat_refine_conflicts"
-  category   = "regular"
-  long       = "refine-conflicts"
-  type       = "bool"
-  default    = "false"
-  help       = "refine theory conflict clauses (default false)"
-
 [[option]]
   name       = "minisatUseElim"
   category   = "regular"

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index c0e524cde915df0307d053af209f33c4d648fbc8..2b39745111839582b1b368bc0c79f3a41c2fe682 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1595,14 +1595,7 @@ lbool Solver::search(int nof_conflicts)
                  progressEstimate() * 100);
       }
 
-      if (theoryConflict && options::sat_refine_conflicts())
-      {
-        check_type = CHECK_FINAL_FAKE;
-      }
-      else
-      {
-        check_type = CHECK_WITH_THEORY;
-      }
+      check_type = CHECK_WITH_THEORY;
     }
     else
     {