mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 18:08:57 +00:00
Code Activity

Fix: revert maximize_objectives1 push/pop regression and backup LP state before NLA maximize

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-09 19:06:50 +00:00
parent a0923c601b
commit a85bdfe21b
2 changed files with 2 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/opt/opt_solver.cpp
View file

@ -202,29 +202,8 @@ namespace opt {
bool opt_solver::maximize_objectives1(expr_ref_vector& blockers) {
expr_ref blocker(m);
for (unsigned i = 0; i < m_objective_vars.size(); ++i) {
// Push context to isolate each objective's optimization.
// This prevents bounds created during one objective's optimization
// from affecting subsequent objectives (fixes issue #7677).
m_context.push();
if (!maximize_objective(i, blocker)) {
m_context.pop(1);
if (!maximize_objective(i, blocker))
return false;
}
// Save results before popping
inf_eps val = m_objective_values[i];
model_ref mdl;
if (m_models[i])
mdl = m_models[i];
m_context.pop(1);
// Restore the computed values after pop
m_objective_values[i] = val;
if (mdl)
m_models.set(i, mdl.get());
blockers.push_back(blocker);
}
return true;

2
src/smt/theory_lra.cpp
View file

@ -3988,7 +3988,7 @@ public:
lp::impq term_max;
lp::lp_status st;
lpvar vi = 0;
if (has_int()) {
if (has_int() || m_nla) {
lp().backup_x();
}
if (!is_registered_var(v)) {