From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 22 Feb 2022 18:36:46 +0000 (-0600)
Subject: Remove refineConflicts option (#8129)
X-Git-Tag: cvc5-1.0.0~406
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c043de3e4668808eb6ee31cbb39f03c64b31031c;p=cvc5.git

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 efdc89c3e..8404ab920 100644
--- 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 c0e524cde..2b3974511 100644
--- 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
     {