From d5231f8b3318ca4eee922a29414218d9f7a82922 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 27 Apr 2023 08:43:59 -0700
Subject: [PATCH] fix regressions #6703

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_lra.cpp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index a5a31709b..c6bd12f03 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1661,7 +1661,7 @@ public:
         }
         bool giveup = false;
         final_check_status st = FC_DONE;
-        // m_final_check_idx = 0; // remove to experiment.
+        m_final_check_idx = 0; // remove to experiment.
         unsigned old_idx = m_final_check_idx;
         switch (is_sat) {
         case l_true:
@@ -1713,12 +1713,12 @@ public:
                 
                 switch (m_final_check_idx) {
                 case 0:
-                    st = check_lia();
-                    break;
-                case 1:
                     if (assume_eqs()) 
                         st = FC_CONTINUE;                    
                     break;
+                case 1:
+                    st = check_lia();
+                    break;
                 case 2:
                     st = check_nla();
                     break;