mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

disable aig tactic in inc_sat_solver (it can blow up the size of formulas significantly without sharing) and fix configuration update bug for optimization context exposed in example by Corina

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-11-20 14:34:31 -08:00
parent 95fe9a3a68
commit c1a6163bda
4 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -84,12 +84,14 @@ public:
simp2_p.set_uint("local_ctx_limit", 10000000);
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);
m_preprocess =
and_then(mk_card2bv_tactic(m, m_params),
using_params(mk_simplify_tactic(m), simp2_p),
mk_max_bv_sharing_tactic(m),
mk_bit_blaster_tactic(m, &m_bb_rewriter),
mk_aig_tactic(),
//mk_aig_tactic(),
using_params(mk_simplify_tactic(m), simp2_p));
}