From 6553382ec8f03663813da1e7a0de337dd76a2f50 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 15 Oct 2023 12:30:24 -0700
Subject: [PATCH] remove extra assume-eqs

---
 src/smt/theory_lra.cpp | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 284c34b54..abbcea199 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1635,7 +1635,7 @@ public:
         switch (is_sat) {
         case l_true:
             TRACE("arith", display(tout));            
-            
+                
             switch (check_lia()) {
             case FC_DONE:
                 break;
@@ -1647,7 +1647,6 @@ public:
                     st = FC_CONTINUE;
                 break;
             }
-            
 
             switch (check_nla()) {
             case FC_DONE:
@@ -1658,7 +1657,7 @@ public:
                 TRACE("arith", tout << "check-nra giveup\n";);
                 st = FC_GIVEUP;
                 break;
-            }
+            }                        
                         
             if (assume_eqs()) {
                 ++m_stats.m_assume_eqs;
@@ -1970,9 +1969,6 @@ public:
         }
         if (!check_idiv_bounds())
             return FC_CONTINUE;
-
-        if (assume_eqs())
-            return FC_CONTINUE;
         
         return FC_DONE;
     }
@@ -2027,7 +2023,7 @@ public:
             add_lemmas();
             return FC_CONTINUE;
         case l_true:
-            return assume_eqs()? FC_CONTINUE: FC_DONE;
+            return FC_DONE;
         default:
             return FC_GIVEUP;
         }