mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
QF_FP default tactic bugfix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
2b7f9b7e5c
commit
7a5239ef70
|
@ -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 {
|
||||
|
|
Loading…
Reference in a new issue