From 7a5239ef707251a409894eef7eed773a96ede48e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 31 Dec 2014 17:30:45 +0000 Subject: [PATCH] QF_FP default tactic bugfix Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/qffpa_tactic.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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 {