diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp
index e8ae816fe..85ceb41c1 100644
--- a/src/math/lp/emonics.cpp
+++ b/src/math/lp/emonics.cpp
@@ -226,7 +226,6 @@ bool emonics::elists_are_consistent(std::unordered_map<unsigned_vector, std::uno
             c.insert(e.var());
         auto it = lists.find(m.rvars());
         (void)it;
-        
         CTRACE("nla_solver_mons",  it->second != c,
                tout << "m = " << m << "\n";
                tout << "c = " ; print_vector(c, tout); tout << "\n";
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index ff0bb4d44..f341c5c01 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -40,8 +40,9 @@ bool int_solver::has_inf_int() const {
 int int_solver::find_inf_int_base_column() {
     unsigned inf_int_count = 0;
     int j = find_inf_int_boxed_base_column_with_smallest_range(inf_int_count);
-    if (j != -1) 
+    if (j != -1) {
         return j;
+    }
     if (inf_int_count == 0)
         return -1;
     unsigned k = random() % inf_int_count;
@@ -58,8 +59,9 @@ int int_solver::get_kth_inf_int(unsigned k) const {
 
 int int_solver::find_inf_int_nbasis_column() const {
     for (unsigned j : m_lar_solver->r_nbasis())
-        if (!column_is_int_inf(j)) 
+        if (!column_is_int_inf(j)) {
             return j;    
+        }
     return -1; 
 }
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 04afd7152..5e280ca14 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1692,7 +1692,6 @@ public:
             
         ctx().push_trail(value_trail<context, unsigned>(m_assume_eq_head));
         while (m_assume_eq_head < m_assume_eq_candidates.size()) {
-            ++m_stats.m_assume_eqs;
             std::pair<theory_var, theory_var> const & p = m_assume_eq_candidates[m_assume_eq_head];
             theory_var v1 = p.first;
             theory_var v2 = p.second;
@@ -1703,6 +1702,7 @@ public:
                    is_eq(v1, v2) && n1->get_root() != n2->get_root(),
                    tout << "assuming eq: v" << v1 << " = v" << v2 << "\n";);
             if (is_eq(v1, v2) &&  n1->get_root() != n2->get_root() && th.assume_eq(n1, n2)) {
+                std::cout << v1 << " == " << v2 << "\n"; // mk_pp(n1->get_owner(), m) << " == " << mk_pp(n2->get_owner(), m) << "\n";
                 return true;
             }
         }
@@ -1734,11 +1734,17 @@ public:
         final_check_status st = FC_DONE;
         switch (is_sat) {
         case l_true:
-                
+
             if (delayed_assume_eqs()) {
+                ++m_stats.m_assume_eqs;
                 return FC_CONTINUE;
             }
 
+            if (assume_eqs()) {
+                ++m_stats.m_assume_eqs;
+                return FC_CONTINUE;
+            }    
+                
             TRACE("arith", display(tout););
             switch (check_lia()) {
             case l_true:
@@ -1761,14 +1767,10 @@ public:
                 st = FC_GIVEUP;
                 break;
             }
-            if (assume_eqs()) {
-                return FC_CONTINUE;
-            }    
             if (m_not_handled != nullptr) {
                 TRACE("arith", tout << "unhandled operator " << mk_pp(m_not_handled, m) << "\n";);        
                 st = FC_GIVEUP;
-            }
-                
+            }                
             return st;
         case l_false:
             get_infeasibility_explanation_and_set_conflict();