mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-26 17:02:38 +00:00
Code Activity

nla: restore eager propagate_nla during theory_lra propagation

Browse source 
PR #10180 moved nonlinear bound propagation to final_check only, removing
the eager propagate_nla() from the search-time propagation path. This left
E-matching without nla-implied bound facts during search, causing an
instantiation blowup on number-theory goals (e.g. FStar.Math.Euclid),
which exhausted rlimit and returned unknown on queries previously proved.

Re-run propagate_nla() before propagate_bounds_with_lp_solver() in the
l_true case of propagate_core so tightened nonlinear bounds are surfaced
to the SMT core during search. Recovers FStar.Math.Euclid-1/-2.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
This commit is contained in:
Nikolaj Bjorner 2026-07-23 16:20:35 -07:00
parent e268a72eb9
commit e3cc338fc9
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_lra.cpp
View file

@ -2319,6 +2319,7 @@ public:
get_infeasibility_explanation_and_set_conflict();
break;
case l_true:
propagate_nla();
propagate_bounds_with_lp_solver();
break;
case l_undef: