From 4ea5ec028715c642c6ddf1a25e61fbb0f2c9e1ba Mon Sep 17 00:00:00 2001 From: Arie <123119895+1arie1@users.noreply.github.com> Date: Mon, 11 May 2026 12:03:09 -0400 Subject: [PATCH] Throttle lia2card in QF_LIA preamble (mk_preamble_tactic) (#9489) mk_preamble_tactic in qflia_tactic.cpp constructed lia2card with a throttled params_ref but did not wrap the call in using_params, so when the preamble is invoked standalone the throttle is silently clobbered by and_then's ambient param propagation: each child gets updt_params(outer_p) called on it, re-reading lia2card.max_range from the outer params (default 101) and discarding the constructor override. mk_qflia_tactic masks the bug because it wraps the whole chain in using_params(..., main_p) where main_p also carries lia2card.max_range=1. But QF_UFNIA goals reach mk_preamble_tactic through the fall-through tail in mk_default_tactic (default_tactic.cpp:52) without that outer wrap: is_qfnia_probe rejects goals containing UF, so QF_UFNIA does not route through mk_qfnia_tactic and instead lands on the unguarded preamble. Any integer variable with concrete range hi-lo <= 101 then gets hot-encoded into ~hi-lo indicator Booleans plus a sum-of-ITEs, inflating SAT search and bloating each NLA refutation that touches the partition. Fix: wrap the call with using_params(mk_lia2card_tactic(m), lia2card_p) so the throttle survives ambient propagation. Verified on a Certora QF_UFNIA VC with a 0..98 integer: metrics now match running with explicit tactic.lia2card.max_range=0 (mk-bool-var, decisions, nlsat-restarts all within run-to-run noise of the workaround), confirming the built-in throttle is finally effective. This mirrors the pattern from commit 87e45accd ("Throttle lia2card in QF_NIA preamble", #9362) which fixed the same bug in mk_qfnia_preamble but did not propagate the fix to the QF_LIA preamble. The original throttle parameters (max_range=1, max_ite_nesting=1) were introduced by Nikolaj's commit 99cbfa715 ("Add a sharp throttle to lia2card tactic to control overhead in default tactic mode") in Feb 2025; that commit set the params at construction time, which works under mk_qflia_tactic's outer using_params wrap but not under standalone invocation. Co-authored-by: Claude Opus 4.7 (1M context) --- src/tactic/smtlogics/qflia_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp index e728a33ac..294df6f58 100644 --- a/src/tactic/smtlogics/qflia_tactic.cpp +++ b/src/tactic/smtlogics/qflia_tactic.cpp @@ -204,7 +204,7 @@ tactic * mk_preamble_tactic(ast_manager& m) { using_params(mk_ctx_simplify_tactic(m), ctx_simp_p), using_params(mk_simplify_tactic(m), pull_ite_p), mk_solve_eqs_tactic(m), - mk_lia2card_tactic(m, lia2card_p), + using_params(mk_lia2card_tactic(m), lia2card_p), mk_elim_uncnstr_tactic(m)); }