diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp
index fc8acee4f..5b602148c 100644
--- a/src/tactic/core/dom_simplify_tactic.cpp
+++ b/src/tactic/core/dom_simplify_tactic.cpp
@@ -237,7 +237,8 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
             TRACE("simplify", tout << new_c << "\n" << new_t << "\n" << new_e << "\n";);
             r = m.mk_ite(new_c, new_t, new_e);
         }        
-    }    
+    }
+    reset_cache();
     return r;
 }
 
@@ -281,7 +282,12 @@ expr_ref dom_simplify_tactic::simplify_rec(expr * e0) {
         if (is_app(e)) {
             m_args.reset();
             for (expr* arg : *to_app(e)) {
-                m_args.push_back(simplify_arg(arg)); 
+                // we don't have a way to distinguish between e.g.
+                // ite(c, f(c), foo)  (which should go to ite(c, f(true), foo))
+                // from and(or(x, y), f(x)), where we do a "trial" with x=false
+                // Trials are good for boolean formula simplification but not sound
+                // for fn applications.
+                m_args.push_back(m.is_bool(arg) ? arg : simplify_arg(arg));
             }
             r = m.mk_app(to_app(e)->get_decl(), m_args.size(), m_args.c_ptr());
         }
diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h
index 292cf538a..f214851f9 100644
--- a/src/tactic/core/dom_simplify_tactic.h
+++ b/src/tactic/core/dom_simplify_tactic.h
@@ -114,6 +114,7 @@ class dom_simplify_tactic : public tactic {
 
     expr_ref get_cached(expr* t) { expr* r = nullptr; if (!m_result.find(t, r)) r = t; return expr_ref(r, m); }
     void cache(expr *t, expr* r) { m_result.insert(t, r); m_trail.push_back(r); }
+    void reset_cache() { m_result.reset(); }
 
     ptr_vector<expr> const & tree(expr * e);
     expr* idom(expr *e) const { return m_dominators.idom(e); }