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>
* Compute term generations based on minimal match
* Tidy up get_*_f_app
* Update euf_mam to the minimum generation number among matches
* Update euf_mam.cpp
* Move the UNREACHABLE() test to smt_mam.cpp
* Enforce stickiness of max-generation
* Add current generation tracking to bind structure
* Fix build error
---------
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Two TRACE blocks under the existing nla_solver tag:
1. theory_lra::false_case_of_check_nla emits a "varmap:" line for each
NLA lemma, listing j-var → SMT-name mappings for variables in the
lemma's collect_vars set. Lets lemur nla resolve the LP-internal
j-numbering back to the original SMT term names when displaying
lemmas. Without this, lemma-level analysis has to either guess at
variable identities (and j-numbers are reused across nlsat
invocations under backtracking — see j-vars-unstable note) or use a
different trace tag entirely (-tr:nra) for stable algebraic-number
IDs.
2. nla_grobner emits a "grobner-linear-eq:" line at each call to
add_term + update_column_type_and_bound that produces a Linear
Propagation row from completion. Lets us count Gröbner's effective
contribution to the LP tableau independently of the lemma stream.
Useful when investigating Gröbner-deficit hypotheses in NLA cascade
diagnosis.
Both are pure trace emission, behind TRACE(nla_solver, ...). Zero
runtime cost when tracing is off; no semantic change.
* Add adaptive growth knobs for Gröbner under arith.nl.grobner_adaptive
When enabled, the per-call growth budget (m_eqs_growth, m_expr_size_growth,
m_expr_degree_growth, m_max_simplified) is scaled by m_growth_boost:
- two consecutive productive runs bump the boost by 3/2 (cap 4x)
- a miss resets the streak and decays the boost toward 1.0x by 1/4 of excess
Default is off; the existing miss-frequency throttle (m_quota / m_delay_base)
is unchanged, so this only affects per-call power, not call frequency.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Update src/params/smt_params_helper.pyg
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-authored-by: Arie Gurfinkel <arie.gurfinkel@gmail.com>
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
theory_lra reports num_final_check_levels()==2: full nlsat (m_nra.check)
only runs at level >= 2. When a level-1 round-trip ends with FC_GIVEUP
and the loop escalates to level 2, the previously accumulated 'result',
'f', and 'm_incomplete_theories' were retained, so a subsequent
successful (FC_DONE) round at level 2 was still reported as
(incomplete (theory arithmetic)). Reset that state on each level
escalation.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
