From c043de3e4668808eb6ee31cbb39f03c64b31031c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 22 Feb 2022 12:36:46 -0600 Subject: [PATCH] Remove refineConflicts option (#8129) Was introduced in 8a0c056. Fixes #8119. --- src/options/prop_options.toml | 8 -------- src/prop/minisat/core/Solver.cc | 9 +-------- 2 files changed, 1 insertion(+), 16 deletions(-) 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 { -- 2.30.2