disable ackermannize on goal

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Sep 7, 2019 · 85fb6f5 · 85fb6f5
1 parent ff3cff0
commit 85fb6f5
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
@@ -805,7 +805,8 @@ namespace opt {
             and_then(mk_simplify_tactic(m, m_params), 
                      mk_propagate_values_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
                      mk_simplify_tactic(m));   
         opt_params optp(m_params);