diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index ed36562ca..00f2c04ae 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -1569,21 +1569,48 @@ br_status arith_rewriter::mk_to_real_core(expr * arg, expr_ref & result) {
 }
 
 br_status arith_rewriter::mk_is_int(expr * arg, expr_ref & result) {
-    numeral a;
-    if (m_util.is_numeral(arg, a)) {
-        result = a.is_int() ? m.mk_true() : m.mk_false();
+    numeral n;
+    
+    if (m_util.is_numeral(arg, n)) {
+        result = n.is_int() ? m.mk_true() : m.mk_false();
         return BR_DONE;
     }
-    else if (m_util.is_to_real(arg)) {
+    
+    if (m_util.is_to_real(arg)) {
         result = m.mk_true();
         return BR_DONE;
     }
-    else {
-        result = m.mk_eq(m.mk_app(get_fid(), OP_TO_REAL,
-                                      m.mk_app(get_fid(), OP_TO_INT, arg)),
-                           arg);
-        return BR_REWRITE3;
+
+    ptr_buffer<expr> todo;
+    todo.push_back(arg);
+    expr_fast_mark1 mark; 
+    for (unsigned i = 0; i < todo.size(); ++i) {
+        expr* e = todo[i];
+        if (mark.is_marked(e))
+            continue;
+        mark.mark(e, true);
+        if (m_util.is_to_real(e))
+            continue;
+        if (m_util.is_numeral(e, n)) {
+            if (n.is_int())
+                continue;
+            goto bail;
+        }
+        if (m_util.is_mul(e) || m_util.is_add(e) || m_util.is_sub(e) || m_util.is_uminus(e)) {
+            for (expr* a : *to_app(e))
+                todo.push_back(a);
+            continue;
+        }
+        goto bail;
     }
+    result = m.mk_true();
+    return BR_DONE;
+
+ bail:
+    result = m.mk_eq(m.mk_app(get_fid(), OP_TO_REAL,
+                              m.mk_app(get_fid(), OP_TO_INT, arg)),
+                     arg);
+    return BR_REWRITE3;
 }
 
 br_status arith_rewriter::mk_abs_core(expr * arg, expr_ref & result) {