From 7d8b56027fb6df40abf99851508adba9d360d6c6 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 21 Feb 2020 18:48:54 +0000 Subject: [PATCH] fix #3068: unsound cache of exprs in or expression this tactic has a quite broken caching mechanism (needs a stack).. :S --- src/tactic/core/dom_simplify_tactic.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index cec6eea09..ae2472348 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -348,6 +348,9 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) { } pop(scope_level() - old_lvl); + // TODO: add stack for cache rather than destroy it completely everywhere + if (!is_and) + reset_cache(); return { is_and ? mk_and(args) : mk_or(args), m }; }