diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index d1136a636..015ca1273 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -87,8 +87,13 @@ namespace opt {
     smt::theory_opt& opt_solver::get_optimizer() {
         smt::context& ctx = m_context.get_context();                        
         smt::theory_id arith_id = m_context.m().get_family_id("arith");     
-        smt::theory* arith_theory = ctx.get_theory(arith_id);               
+        smt::theory* arith_theory = ctx.get_theory(arith_id);
         
+        if (!arith_theory) {
+            ctx.register_plugin(alloc(smt::theory_mi_arith, m, m_params));
+            arith_theory = ctx.get_theory(arith_id);
+            SASSERT(arith_theory);
+        }
         if (typeid(smt::theory_mi_arith) == typeid(*arith_theory)) {        
             return dynamic_cast<smt::theory_mi_arith&>(*arith_theory); 
         }                                                                   
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index aeb70752b..a97c82369 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -870,6 +870,7 @@ namespace smt {
         atom_kind kind2 = a2->get_atom_kind();
         bool v_is_int = is_int(v);
         SASSERT(v == a2->get_var());
+        if (k1 == k2 && kind1 == kind2) return;
         SASSERT(k1 != k2 || kind1 != kind2);
         parameter coeffs[3] = { parameter(symbol("farkas")), 
                                 parameter(rational(1)), parameter(rational(1)) };