mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-21 17:39:36 +00:00
Code Activity

add solve-eqs to the qfnia tactic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-05-01 16:29:29 -07:00
parent e09964096e
commit eefb644c93
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/tactic/smtlogics/qfnia_tactic.cpp
View file

@ -82,6 +82,7 @@ static tactic * mk_qfnia_preamble(ast_manager & m, params_ref const & p_ref) {
return return
and_then(mk_simplify_tactic(m), and_then(mk_simplify_tactic(m),
mk_propagate_values_tactic(m), mk_propagate_values_tactic(m),
mk_solve_eqs_tactic(m),
using_params(mk_ctx_simplify_tactic(m), ctx_simp_p), using_params(mk_ctx_simplify_tactic(m), ctx_simp_p),
using_params(mk_simplify_tactic(m), pull_ite_p), using_params(mk_simplify_tactic(m), pull_ite_p),
mk_elim_uncnstr_tactic(m), mk_elim_uncnstr_tactic(m),