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

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