diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index 96b4446c4..a51b0fe41 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -216,7 +216,7 @@ public:
             else 
                 return false;
         }
-        if (x_index == UINT_MAX && y_index == UINT_MAX)
+        if (x_index == UINT_MAX || y_index == UINT_MAX)
             return false;
         if (lp().column_is_int(row[x_index].var()) != lp().column_is_int(row[y_index].var()))
             return false; 
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 8330ca98d..96e46dbbf 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -755,10 +755,10 @@ namespace smt {
     }
 
     void setup::setup_lra_arith() {
-        // 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));
+        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() {