mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-07 05:02:48 +00:00
Code Activity

Fix LP solver pop invalidation: clear changed bounds on pop, guard mk_value

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/c9284821-5ce7-42c8-a4cc-f2a1aa582115

Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-04-04 20:14:52 +00:00 • committed by GitHub
parent 0cd17f4194
commit 260cf5c357
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/lp/lar_solver.cpp
View file

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

2
src/smt/theory_lra.cpp
View file

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