From d9227b95ea4e3894f63907c38c4b3a79e249c429 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 29 Nov 2016 15:45:23 -0800 Subject: [PATCH] blast distinct in incremental BV solver Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 682978287..e56abc50c 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -336,6 +336,7 @@ public: simp2_p.set_bool("flat", true); // required by som simp2_p.set_bool("hoist_mul", false); // required by som simp2_p.set_bool("elim_and", true); + simp2_p.set_bool("blast_distinct", true); m_preprocess = and_then(mk_card2bv_tactic(m, m_params), using_params(mk_simplify_tactic(m), simp2_p),