diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index e0bd2b876..81e58d7ff 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -74,7 +74,7 @@ namespace smt {
 
         std::ostream& display_last_failure(std::ostream& out) const;
         std::string last_failure_as_string() const;
-        void set_reason_unknown(char const* msg) { m_unknown = msg; std::cout << m_unknown << "\n"; }
+        void set_reason_unknown(char const* msg) { m_unknown = msg; }
         void set_progress_callback(progress_callback *callback);
 
 
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index 63b7f20a9..955327904 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -489,7 +489,7 @@ namespace smt {
 
     proto_model * model_generator::mk_model() {
         SASSERT(!m_model);
-        TRACE("model", m_context->display(tout););
+        TRACE("model_verbose", m_context->display(tout););
         init_model();
         register_existing_model_values();
         mk_bool_model();
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index a7f5db33d..df2491a3e 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -39,13 +39,35 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::found_underspecified_op(app * n) {
+        context& ctx = get_context();
         m_underspecified_ops.push_back(n);
-        get_context().push_trail(push_back_vector<context, ptr_vector<app>>(m_underspecified_ops));
+        ctx.push_trail(push_back_vector<context, ptr_vector<app>>(m_underspecified_ops));
         if (!m_found_underspecified_op) {
             TRACE("arith", tout << "found underspecified expression:\n" << mk_pp(n, get_manager()) << "\n";);
-            get_context().push_trail(value_trail<context, bool>(m_found_underspecified_op));
+            ctx.push_trail(value_trail<context, bool>(m_found_underspecified_op));
             m_found_underspecified_op = true;
         }
+
+        expr* e = nullptr;
+        if (m_util.is_div(n)) {                
+            e = m_util.mk_div0(n->get_arg(0), n->get_arg(1));
+        }
+        else if (m_util.is_idiv(n)) {                
+            e = m_util.mk_idiv0(n->get_arg(0), n->get_arg(1));
+        }
+        else if (m_util.is_rem(n)) {                
+            e = m_util.mk_rem0(n->get_arg(0), n->get_arg(1));
+        }
+        else if (m_util.is_mod(n)) {                
+            e = m_util.mk_mod0(n->get_arg(0), n->get_arg(1));
+        }
+        else if (m_util.is_power(n)) {                
+            e = m_util.mk_power0(n->get_arg(0), n->get_arg(1));
+        }
+        if (e) {
+            ctx.assign(mk_eq(e, n, false), nullptr);
+        }
+
     }
 
     template<typename Ext>
@@ -389,9 +411,9 @@ namespace smt {
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_div(app * n) {
         rational r(1);
-        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         theory_var s      = mk_binary_op(n);
         context & ctx     = get_context();
+        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         if (!ctx.relevancy())
             mk_div_axiom(n->get_arg(0), n->get_arg(1));
         return s;
@@ -400,9 +422,9 @@ namespace smt {
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_idiv(app * n) {
         rational r;
-        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         theory_var s      = mk_binary_op(n);
         context & ctx     = get_context();
+        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         app * mod         = m_util.mk_mod(n->get_arg(0), n->get_arg(1));
         ctx.internalize(mod, false);
         if (ctx.relevancy())
@@ -414,9 +436,9 @@ namespace smt {
     theory_var theory_arith<Ext>::internalize_mod(app * n) {
         TRACE("arith_mod", tout << "internalizing...\n" << mk_pp(n, get_manager()) << "\n";);
         rational r(1);
-        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         theory_var s      = mk_binary_op(n);
         context & ctx     = get_context();
+        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         if (!ctx.relevancy())
             mk_idiv_mod_axioms(n->get_arg(0), n->get_arg(1));
         return s;
@@ -425,9 +447,9 @@ namespace smt {
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_rem(app * n) {
         rational r(1);
-        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         theory_var s  = mk_binary_op(n);
         context & ctx = get_context();
+        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         if (!ctx.relevancy()) {
             mk_rem_axiom(n->get_arg(0), n->get_arg(1));
         }
@@ -3265,7 +3287,10 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::init_model(model_generator & m) {
-        TRACE("theory_arith", tout << "init model invoked...\n";);
+        TRACE("theory_arith", tout << "init model invoked...\n";
+              for (app* n : m_underspecified_ops) {
+                  tout << mk_pp(n, get_manager()) << "\n";
+              });
         context& ctx = get_context();
         m_factory = alloc(arith_factory, get_manager());
         m.register_factory(m_factory);
@@ -3273,28 +3298,6 @@ namespace smt {
         if (!m_model_depends_on_computed_epsilon) {
             refine_epsilon();
         }
-        for (app* n : m_underspecified_ops) {
-            enode* e = nullptr;
-            if (m_util.is_div(n)) {                
-                e = mk_enode(m_util.mk_div0(n->get_arg(0), n->get_arg(1)));
-            }
-            else if (m_util.is_idiv(n)) {                
-                e = mk_enode(m_util.mk_idiv0(n->get_arg(0), n->get_arg(1)));
-            }
-            else if (m_util.is_rem(n)) {                
-                e = mk_enode(m_util.mk_rem0(n->get_arg(0), n->get_arg(1)));
-            }
-            else if (m_util.is_mod(n)) {                
-                e = mk_enode(m_util.mk_mod0(n->get_arg(0), n->get_arg(1)));
-            }
-            else if (m_util.is_power(n)) {                
-                e = mk_enode(m_util.mk_power0(n->get_arg(0), n->get_arg(1)));
-            }
-            if (e) {
-                ctx.mark_as_relevant(e);
-                ctx.add_eq(e, ctx.get_enode(n), eq_justification());
-            }
-        }
     }
 
     template<typename Ext>