mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

blast distinct in incremental BV solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-11-29 15:45:23 -08:00
parent 4b4365470d
commit d9227b95ea
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -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),