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)) {