From a904f2bb2211bf5d7fdbeba66bd6a76fc148644b Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 12 Mar 2026 16:30:18 +0000
Subject: [PATCH] simplify max_result in theory_lra.cpp and remove extra blank
 lines in lar_solver.cpp

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

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 6e689c004..d6b8b0823 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -467,8 +467,6 @@ namespace lp {
         return ret;
     }
 
-
-
     lp_status lar_solver::solve() {
         if (m_imp->m_status == lp_status::INFEASIBLE || m_imp->m_status == lp_status::CANCELLED)
             return m_imp->m_status;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 72bf7354a..92950b192 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -4038,24 +4038,19 @@ public:
         return false;
     }
 
-    theory_lra::inf_eps max_result(theory_var v, lpvar vi, lp::lp_status st, expr_ref& blocker, bool& has_shared) {
-        switch (st) {
-        case lp::lp_status::OPTIMAL:
+    theory_lra::inf_eps max_result(theory_var v, lpvar vi, lp::lp_status st,
+                                    expr_ref& blocker, bool& has_shared) {
+        if (st == lp::lp_status::OPTIMAL)
             init_variable_values();
-            TRACE(arith, display(tout << st << " v" << v << " vi: " << vi << "\n"););
+        TRACE(arith, display(tout << st << " v" << v << " vi: " << vi << "\n"););
+        if (st != lp::lp_status::UNBOUNDED) {
             blocker = mk_gt(v);
             return value(v);
-        case lp::lp_status::FEASIBLE:
-            TRACE(arith, display(tout << st << " v" << v << " vi: " << vi << "\n"););
-            blocker = mk_gt(v);
-            return value(v);
-        default:
-            SASSERT(st == lp::lp_status::UNBOUNDED);
-            TRACE(arith, display(tout << st << " v" << v << " vi: " << vi << "\n"););
-            has_shared = false;
-            blocker = m.mk_false();
-            return inf_eps(rational::one(), inf_rational());
         }
+        SASSERT(st == lp::lp_status::UNBOUNDED);
+        has_shared = false;
+        blocker = m.mk_false();
+        return inf_eps(rational::one(), inf_rational());
     }
 
     theory_lra::inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared) {