From 87e45accd9a6c51f85a665454788c992c2b83eed Mon Sep 17 00:00:00 2001 From: Arie <123119895+1arie1@users.noreply.github.com> Date: Wed, 22 Apr 2026 11:58:28 -0400 Subject: [PATCH] Throttle lia2card in QF_NIA preamble (#9362) mk_qfnia_preamble invoked lia2card with no params, so the default max_range=101 was in effect. Any integer variable with a concrete range hi-lo <= 101 was expanded into that many fresh Booleans plus a sum-of-ITEs, bloating SAT search alongside the nonlinear structure. On an observed QF_UFNIA benchmark this drove a 0.2s problem to a 30s timeout. Mirror the throttle already applied in mk_preamble_tactic (qflia_tactic.cpp, commit 99cbfa715): limit lia2card to 0-1 integer variables and nesting depth 1. Wrap with using_params so the override survives and_then's downstream updt_params calls (passing the params to mk_lia2card_tactic alone is overwritten when and_then re-propagates the ambient params to each child). Co-authored-by: Claude Opus 4.7 (1M context) --- src/tactic/smtlogics/qfnia_tactic.cpp | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index 25dc34d9c..f3c36dc4c 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -71,14 +71,21 @@ static tactic * mk_qfnia_preamble(ast_manager & m, params_ref const & p_ref) { params_ref elim_p = p_ref; elim_p.set_uint("max_memory",20); - + + // Match the throttle applied in mk_preamble_tactic (qflia_tactic.cpp): + // lia2card is by default harmful (see commit 99cbfa715). Limit it to + // 0-1 integer variables. + params_ref lia2card_p = p_ref; + lia2card_p.set_uint("lia2card.max_range", 1); + lia2card_p.set_uint("lia2card.max_ite_nesting", 1); + return - and_then(mk_simplify_tactic(m), + and_then(mk_simplify_tactic(m), mk_propagate_values_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), - mk_lia2card_tactic(m), + using_params(mk_lia2card_tactic(m, lia2card_p), lia2card_p), mk_card2bv_tactic(m, p_ref), skip_if_failed(using_params(mk_cofactor_term_ite_tactic(m), elim_p))); }