diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index 98ba56470..96b4446c4 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -319,8 +319,7 @@ public:
     
     void cheap_eq_table(unsigned rid) {
         TRACE("cheap_eqs", tout << "checking if row " << rid << " can propagate equality.\n";  display_row_info(rid, tout););
-        unsigned x;
-        unsigned y;
+        unsigned x, y;
         mpq k;
         if (is_offset_row(rid, x, y, k)) {
             if (y == null_lpvar) {
@@ -358,41 +357,28 @@ public:
             unsigned row_id;
             var_offset key(y, k);
             if (m_var_offset2row_id.find(key, row_id)) {               
-                if (row_id == rid) {
-                    // it is the same row.
+                if (row_id == rid) { // it is the same row.
                     return;
                 }
-                unsigned x2;
-                unsigned y2;
+                unsigned x2, y2;
                 mpq  k2;
                 if (is_offset_row(row_id, x2, y2, k2)) {
-
                     bool new_eq  = false;
-#ifdef _TRACE
-                    bool swapped = false;
-#endif
                     if (y == y2 && k == k2) {
                         new_eq = true;
                     }
-                    else if (y2 != null_lpvar) {
-#ifdef _TRACE
-                        swapped = true;
-#endif
-                        std::swap(x2, y2);
-                        k2.neg();
-                        if (y == y2 && k == k2) {
+                    else if (y2 != null_lpvar && x2 == y && k == - k2) {
+                            std::swap(x2, y2);
                             new_eq = true;
-                        }
                     }
-
+                    
                     if (new_eq) {
                         if (!is_equal(x, x2) && is_int(x) == is_int(x2)) {
-                            SASSERT(y == y2 && k == k2);
+                            //    SASSERT(y == y2 && k == k2 );
                             explanation ex;
                             explain_fixed_in_row(rid, ex);
                             explain_fixed_in_row(row_id, ex);
                             TRACE("arith_eq", tout << "propagate eq two rows:\n"; 
-                                  tout << "swapped: " << swapped << "\n";
                                   tout << "x  : v" << x << "\n";
                                   tout << "x2 : v" << x2 << "\n";
                                   display_row_info(rid, tout); 
@@ -400,10 +386,9 @@ public:
                             add_eq_on_columns(ex, x, x2);
                         }
                         return;
-                        }
-                        }
+                    }
+                }
                 // the original row was deleted or it is not offset row anymore ===> remove it from table 
-                m_var_offset2row_id.erase(key);
             }
             // add new entry
             m_var_offset2row_id.insert(key, rid);
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 805a18def..96e46dbbf 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -755,8 +755,10 @@ namespace smt {
     }
 
     void setup::setup_lra_arith() {
-        // m_context.register_plugin(alloc(smt::theory_mi_arith, m_context));
-        m_context.register_plugin(alloc(smt::theory_lra, m_context));
+        if (m_params.m_arith_mode == AS_OLD_ARITH)
+            m_context.register_plugin(alloc(smt::theory_mi_arith, m_context));
+        else
+            m_context.register_plugin(alloc(smt::theory_lra, m_context));
     }
 
     void setup::setup_mi_arith() {
diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h
index 2c31e84ea..6dae5f60e 100644
--- a/src/smt/theory_arith_eq.h
+++ b/src/smt/theory_arith_eq.h
@@ -253,6 +253,7 @@ namespace smt {
                     m_stats.m_fixed_eqs++;
                     propagate_eq_to_core(x, x2, ante);
                 }
+                //return;
             }
 
             if (k.is_zero() && y != null_theory_var && !is_equal(x, y) && is_int_src(x) == is_int_src(y)) {
@@ -277,16 +278,10 @@ namespace smt {
                 numeral    k2;
                 if (r2.get_base_var() != null_theory_var && is_offset_row(r2, x2, y2, k2)) {
                     bool new_eq  = false;
-#ifdef _TRACE
-                    bool swapped = false;
-#endif
                     if (y == y2 && k == k2) {
                         new_eq = true;
                     }
                     else if (y2 != null_theory_var) {
-#ifdef _TRACE
-                        swapped = true;
-#endif
                         std::swap(x2, y2);
                         k2.neg();
                         if (y == y2 && k == k2) {
@@ -301,7 +296,6 @@ namespace smt {
                             collect_fixed_var_justifications(r, ante);
                             collect_fixed_var_justifications(r2, ante);
                             TRACE("arith_eq", tout << "propagate eq two rows:\n"; 
-                                  tout << "swapped: " << swapped << "\n";
                                   tout << "x  : v" << x << "\n";
                                   tout << "x2 : v" << x2 << "\n";
                                   display_row_info(tout, r); 
@@ -312,9 +306,11 @@ namespace smt {
                         return;
                     }
                 }
+
                 // the original row was delete or it is not offset row anymore ===> remove it from table 
-                m_var_offset2row_id.erase(key);
             }
+            if (y == -1)
+                std::cout << "h";
             // add new entry
             m_var_offset2row_id.insert(key, rid);
         }