From eefb644c93406f7016ba7ca3d063edbd2458071a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 1 May 2026 16:29:29 -0700 Subject: [PATCH] add solve-eqs to the qfnia tactic Signed-off-by: Nikolaj Bjorner --- src/tactic/smtlogics/qfnia_tactic.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index 9bc47af1e..d17167f75 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -81,7 +81,8 @@ static tactic * mk_qfnia_preamble(ast_manager & m, params_ref const & p_ref) { return 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_simplify_tactic(m), pull_ite_p), mk_elim_uncnstr_tactic(m),