From 260cf5c357a215a40ee499c62aad1f74862d8a02 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 4 Apr 2026 20:14:52 +0000 Subject: [PATCH] Fix LP solver pop invalidation: clear changed bounds on pop, guard mk_value Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/c9284821-5ce7-42c8-a4cc-f2a1aa582115 Co-authored-by: levnach <5377127+levnach@users.noreply.github.com> --- src/math/lp/lar_solver.cpp | 3 +++ src/smt/theory_lra.cpp | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 6e689c004..bd4b4cc8c 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -593,6 +593,9 @@ namespace lp { m_imp->m_dependencies.pop_scope(k); // init the nbasis sorting m_imp->require_nbasis_sort(); + // bounds were restored by the trail; any entries in m_columns_with_changed_bounds + // are stale and must be cleared so init_model/get_value see a clean slate + clear_columns_with_changed_bounds(); set_status(lp_status::UNKNOWN); } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 901785378..099708ad6 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3702,7 +3702,7 @@ public: return alloc(expr_wrapper_proc, a.mk_numeral(m_nla->am(), nl_value(v, m_nla->tmp1()), a.is_int(o))); } else { - rational r = get_value(v); + rational r = can_get_value(v) ? get_value(v) : rational::zero(); TRACE(arith, tout << mk_pp(o, m) << " v" << v << " := " << r << "\n";); SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().is_canceled())); if (a.is_int(o) && !r.is_int()) r = floor(r);