diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 703e19f1d..8ccee885a 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -547,6 +547,7 @@ namespace smt {
         ptr_vector<expr> m_todo;
         bool is_int_expr(expr* e);
         bool is_int(theory_var v) const { return m_data[v].m_is_int; }
+        bool is_int_src(theory_var v) const { return m_util.is_int(var2expr(v)); }
         bool is_real(theory_var v) const { return !is_int(v); }
         bool get_implied_old_value(theory_var v, inf_numeral & r) const;
         inf_numeral const & get_implied_value(theory_var v) const;
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 64aa2b638..1b1b9a1a6 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -66,9 +66,9 @@ namespace smt {
 
     template<typename Ext>
     bool theory_arith<Ext>::is_int_expr(expr* e) {
-        return m_util.is_int(e);
 #if 0
-        Disable refined integer until equality propagation is fixed.
+        return m_util.is_int(e);
+#else
         if (m_util.is_int(e)) return true;
         if (is_uninterp(e)) return false;
         m_todo.reset();
@@ -3077,7 +3077,7 @@ namespace smt {
             theory_var num = get_num_vars();
             bool refine = false;
             for (theory_var v = 0; v < num; v++) {
-                if (is_int(v))
+                if (is_int_src(v))
                     continue;
                 if (!get_context().is_shared(get_enode(v)))
                     continue;
@@ -3088,7 +3088,7 @@ namespace smt {
                 rational value = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational();
                 theory_var v2;
                 if (mapping.find(value, v2)) {
-                    SASSERT(!is_int(v2));
+                    SASSERT(!is_int_src(v2));
                     if (get_value(v) != get_value(v2)) {
                         // v and v2 are not known to be equal. 
                         // The choice of m_epsilon is making them equal.
diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h
index 4a5dad34f..8e1b52ee5 100644
--- a/src/smt/theory_arith_eq.h
+++ b/src/smt/theory_arith_eq.h
@@ -43,7 +43,7 @@ namespace smt {
         CTRACE("arith_bug", !lower_bound(v).is_rational(), display_var(tout, v););
         SASSERT(lower_bound(v).is_rational());
         numeral const & val = lower_bound(v).get_rational();
-        value_sort_pair key(val, is_int(v));
+        value_sort_pair key(val, is_int_src(v));
         theory_var v2;
         if (m_fixed_var_table.find(key, v2)) {
             if (v2 < static_cast<int>(get_num_vars()) && is_fixed(v2) && lower_bound(v2).get_rational() == val) {
@@ -51,7 +51,7 @@ namespace smt {
                 // The table m_fixed_var_table is not restored during backtrack. So, it may
                 // contain invalid (key -> value) pairs. So, we must check whether v2 is really equal to val (previous test) AND it has
                 // the same sort of v. The following test was missing in a previous version of Z3. 
-                if (!is_equal(v, v2) && is_int(v) == is_int(v2)) {
+                if (!is_equal(v, v2) && is_int_src(v) == is_int_src(v2)) {
                     antecedents ante(*this);
 
                     //
@@ -226,7 +226,7 @@ namespace smt {
             
             if (y == null_theory_var) {
                 // x is an implied fixed var at k.
-                value_sort_pair key(k, is_int(x));
+                value_sort_pair key(k, is_int_src(x));
                 theory_var x2;
                 if (m_fixed_var_table.find(key, x2) && 
                     x2 < static_cast<int>(get_num_vars()) && 
@@ -238,7 +238,7 @@ namespace smt {
                     // So, we must check whether x2 is really equal to k (previous test) 
                     // AND has the same sort of x.
                     // The following test was missing in a previous version of Z3. 
-                    is_int(x) == is_int(x2) &&
+                    is_int_src(x) == is_int_src(x2) &&
                     !is_equal(x, x2)) {
 
                     antecedents ante(*this);
@@ -254,7 +254,7 @@ namespace smt {
                 }
             }
 
-            if (k.is_zero() && y != null_theory_var && !is_equal(x, y) && is_int(x) == is_int(y)) {
+            if (k.is_zero() && y != null_theory_var && !is_equal(x, y) && is_int_src(x) == is_int_src(y)) {
                 // found equality x = y
                 antecedents ante(*this);
                 collect_fixed_var_justifications(r, ante);
@@ -294,7 +294,7 @@ namespace smt {
                     }
 
                     if (new_eq) {
-                        if (!is_equal(x, x2) && is_int(x) == is_int(x2)) {
+                        if (!is_equal(x, x2) && is_int_src(x) == is_int_src(x2)) {
                             SASSERT(y == y2 && k == k2);
                             antecedents ante(*this);
                             collect_fixed_var_justifications(r, ante);
@@ -323,11 +323,10 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::propagate_eq_to_core(theory_var x, theory_var y, antecedents& antecedents) {
-        // I doesn't make sense to propagate an equality (to the core) of variables of different sort.
-        SASSERT(is_int(x) == is_int(y));
         // Ignore equality if variables are already known to be equal.
         if (is_equal(x, y))
             return;
+        // I doesn't make sense to propagate an equality (to the core) of variables of different sort.
         if (get_manager().get_sort(var2expr(x)) != get_manager().get_sort(var2expr(y))) {
             TRACE("arith", tout << mk_pp(var2expr(x), get_manager()) << " = " << mk_pp(var2expr(y), get_manager()) << "\n";);
             return;