diff --git a/src/tactic/fpa/qffpa_tactic.cpp b/src/tactic/fpa/qffpa_tactic.cpp index 6cfc699c7..919cf0c1b 100644 --- a/src/tactic/fpa/qffpa_tactic.cpp +++ b/src/tactic/fpa/qffpa_tactic.cpp @@ -29,7 +29,8 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) { params_ref sat_simp_p = p; sat_simp_p .set_bool("elim_and", true); - return cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()), + tactic * st = + cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()), and_then(mk_simplify_tactic(m), mk_smt_tactic()), and_then( @@ -40,6 +41,9 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) { using_params(mk_simplify_tactic(m, p), sat_simp_p), mk_sat_tactic(m, p), mk_fail_if_undecided_tactic())); + + st->updt_params(p); + return st; } struct is_non_qffp_predicate {