diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 5a0f8db95..77882f186 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -946,6 +946,7 @@ namespace smt {
         //
         // -----------------------------------
         typedef int_hashtable<int_hash, default_eq<int> > row_set;
+        bool            m_model_depends_on_computed_epsilon;
         unsigned        m_nl_rounds;
         bool            m_nl_gb_exhausted;
         unsigned        m_nl_strategy_idx; // for fairness
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 9db5e8c72..513cf36a4 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -1405,6 +1405,7 @@ namespace smt {
 
     template<typename Ext>
     final_check_status theory_arith<Ext>::final_check_core() {
+        m_model_depends_on_computed_epsilon = false;
         unsigned old_idx = m_final_check_idx;
         final_check_status result = FC_DONE;
         final_check_status ok;
@@ -1669,6 +1670,7 @@ namespace smt {
         m_liberal_final_check(true),
         m_changed_assignment(false),
         m_assume_eq_head(0),
+        m_model_depends_on_computed_epsilon(false),
         m_nl_rounds(0),
         m_nl_gb_exhausted(false),
         m_nl_new_exprs(m),
@@ -3220,7 +3222,9 @@ namespace smt {
         m_factory = alloc(arith_factory, get_manager());
         m.register_factory(m_factory);
         compute_epsilon();
-        refine_epsilon();
+        if (!m_model_depends_on_computed_epsilon) {
+            refine_epsilon();
+        }
     }
 
     template<typename Ext>
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index dd91ffbfb..52a117cd5 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -638,6 +638,7 @@ namespace smt {
         if (!val.get_infinitesimal().is_zero() && !computed_epsilon) {
             compute_epsilon();
             computed_epsilon = true;
+            m_model_depends_on_computed_epsilon = true;
         }
         return  val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational();
     }
@@ -652,14 +653,18 @@ namespace smt {
     bool theory_arith<Ext>::check_monomial_assignment(theory_var v, bool & computed_epsilon) {
         SASSERT(is_pure_monomial(var2expr(v)));
         expr * m      = var2expr(v);
-        rational val(1);
+        rational val(1), v_val;
         for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
             expr * arg = to_app(m)->get_arg(i);
             theory_var curr = expr2var(arg);
             SASSERT(curr != null_theory_var);
-            val *= get_value(curr, computed_epsilon);
+            v_val = get_value(curr, computed_epsilon);
+            TRACE("non_linear", tout << mk_pp(arg, get_manager()) << " = " << v_val << "\n";);
+            val *= v_val;
         }
-        return get_value(v, computed_epsilon) == val;
+        v_val = get_value(v, computed_epsilon);
+        TRACE("non_linear", tout << "v" << v << " := " << v_val << " == " << val << "\n";);
+        return v_val == val;
     }
 
 
@@ -2356,6 +2361,7 @@ namespace smt {
     */
     template<typename Ext>
     final_check_status theory_arith<Ext>::process_non_linear() {
+        m_model_depends_on_computed_epsilon = false;
         if (m_nl_monomials.empty())
             return FC_DONE;