diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 631e1d8f3..acc3b889f 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -843,6 +843,8 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
                 continue;
             if (m_util.is_numeral(arg, arg_v) && mod(arg_v, v2) == arg_v)
                 continue;
+            if (m().is_ite(arg)) 
+                continue;
             // found target for rewriting
             break;
         }
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index e4730ea63..ce2249a88 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -155,7 +155,7 @@ public:
         return res;
     }
 
-    void scan_skolems(const ast &proof){
+    void scan_skolems(const ast &proof) {
         hash_map<ast,int> memo;
         scan_skolems_rec(memo,proof, INT_MAX);
     }