diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp
index 89817a768..275acbd18 100644
--- a/src/tactic/arith/purify_arith_tactic.cpp
+++ b/src/tactic/arith/purify_arith_tactic.cpp
@@ -231,7 +231,8 @@ struct purify_arith_proc {
                 void operator()(app* a) {
                     for (expr* arg : *a) {
                         if (!is_ground(arg)) {
-                            o.m_cannot_purify.insert(a->get_decl());
+                            auto* f = a->get_decl();
+                            o.m_cannot_purify.insert(f);
                             break;
                         }
                     }
@@ -694,9 +695,13 @@ struct purify_arith_proc {
                 process_div(f, num, args, result, result_pr);
                 return BR_DONE;
             case OP_IDIV: 
+                if (!m_cannot_purify.empty())
+                    return BR_FAILED;
                 process_idiv(f, num, args, result, result_pr);
                 return BR_DONE;
             case OP_MOD:
+                if (!m_cannot_purify.empty())
+                    return BR_FAILED;
                 process_mod(f, num, args, result, result_pr);                
                 return BR_DONE;
             case OP_TO_INT:
diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp
index 8f6c4371f..f8bd98fa5 100644
--- a/src/tactic/core/dom_simplify_tactic.cpp
+++ b/src/tactic/core/dom_simplify_tactic.cpp
@@ -209,23 +209,22 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
         r = simplify_arg(e);
     }
     else {
-        for (expr * child : tree(ite)) {
-            if (is_subexpr(child, t) && !is_subexpr(child, e)) {
-                simplify_rec(child);
-            }
-        }
+        for (expr * child : tree(ite)) 
+            if (is_subexpr(child, t) && !is_subexpr(child, e)) 
+                simplify_rec(child);            
+        
         pop(scope_level() - old_lvl);
         expr_ref new_t = simplify_arg(t);
+        reset_cache();
         if (!assert_expr(new_c, true)) {
             return new_t;
         }
-        for (expr * child : tree(ite)) {
-            if (is_subexpr(child, e) && !is_subexpr(child, t)) {
+        for (expr * child : tree(ite)) 
+            if (is_subexpr(child, e) && !is_subexpr(child, t)) 
                 simplify_rec(child);
-            }
-        }
         pop(scope_level() - old_lvl);
         expr_ref new_e = simplify_arg(e);
+
         if (c == new_c && t == new_t && e == new_e) {
             r = ite;
         }
@@ -278,7 +277,8 @@ expr_ref dom_simplify_tactic::simplify_rec(expr * e0) {
     }
     else {
         for (expr * child : tree(e)) {
-            simplify_rec(child);
+            if (child != e)
+               simplify_rec(child);
         }
         if (is_app(e)) {
             m_args.reset();
@@ -382,9 +382,11 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
 
     SASSERT(scope_level() == 0);
     bool change = true;
+    unsigned n  = 0;
     m_depth = 0;
-    while (change) {
+    while (change && n < 10) {
         change = false;
+        ++n;
 
         // go forwards
         m_forward = true;