From 3313590b95baf964e7f508a28b3ce9b4f8ec8221 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 6 Apr 2020 12:11:26 +0100 Subject: [PATCH] fix #3713: too much caching in dom-simplify for OR expressions --- src/tactic/core/dom_simplify_tactic.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 2230269db..f26783e41 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -331,6 +331,8 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) { if (!assert_expr(r, !is_and)) { \ pop(scope_level() - old_lvl); \ r = is_and ? m.mk_false() : m.mk_true(); \ + if (!is_and) \ + reset_cache(); \ return r; \ } _SIMP_ARG(arg);