diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index c0f878814..cec6eea09 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -22,7 +22,6 @@ Notes: #include "ast/ast_pp.h" #include "tactic/core/dom_simplify_tactic.h" - /** \brief compute a post-order traversal for e. Also populate the set of parents @@ -358,6 +357,7 @@ expr_ref dom_simplify_tactic::simplify_not(app * e) { unsigned old_lvl = scope_level(); expr_ref t = simplify_rec(ee); pop(scope_level() - old_lvl); + reset_cache(); return mk_not(t); }