From a85bdfe21be634147861c9c4c2c429034f265bdf Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 9 Mar 2026 19:06:50 +0000
Subject: [PATCH] Fix: revert maximize_objectives1 push/pop regression and
 backup LP state before NLA maximize

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/opt/opt_solver.cpp | 23 +----------------------
 src/smt/theory_lra.cpp |  2 +-
 2 files changed, 2 insertions(+), 23 deletions(-)

diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index b058c58b7..9aeb79133 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -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;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 05053f4ea..a9f833ce0 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -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)) {