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) <noreply@anthropic.com>

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));
 }