From d12523e4c0426002c966273858cfde720cb674e0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 27 Jan 2020 08:57:16 -0800
Subject: [PATCH] fix #2883

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

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index c6ba038f0..a138fe4f4 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1558,9 +1558,6 @@ public:
             if (delayed_assume_eqs()) {
                 return FC_CONTINUE;
             }
-            if (assume_eqs()) {
-                return FC_CONTINUE;
-            }            
 
             switch (check_lia()) {
             case l_true:
@@ -1587,6 +1584,10 @@ public:
                 TRACE("arith", tout << "unhandled operator " << mk_pp(m_not_handled, m) << "\n";);        
                 st = FC_GIVEUP;
             }
+
+            if (assume_eqs()) {
+                return FC_CONTINUE;
+            }            
                 
             return st;
         case l_false: