mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

disable ackermannize on goal

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-09-07 17:56:21 +03:00
parent ff3cff06b2
commit 85fb6f59de
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/opt/opt_context.cpp
View file

@ -805,7 +805,8 @@ namespace opt {
and_then(mk_simplify_tactic(m, m_params), and_then(mk_simplify_tactic(m, m_params),
mk_propagate_values_tactic(m), mk_propagate_values_tactic(m),
mk_solve_eqs_tactic(m), mk_solve_eqs_tactic(m),
mk_ackermannize_bv_tactic(m, m_params), // NB: cannot ackermannize because max/min objectives would disappear
// mk_ackermannize_bv_tactic(m, m_params),
// NB: mk_elim_uncstr_tactic(m) is not sound with soft constraints // NB: mk_elim_uncstr_tactic(m) is not sound with soft constraints
mk_simplify_tactic(m)); mk_simplify_tactic(m));
opt_params optp(m_params); opt_params optp(m_params);