From e3cc338fc9c8146fced4204bed95c25d9db63ab4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 23 Jul 2026 16:20:35 -0700 Subject: [PATCH] nla: restore eager propagate_nla during theory_lra propagation 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 --- src/smt/theory_lra.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 9c4588f32a..1ea654be0b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -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: