From a849a29b4f0af61730e986b4aed89ba0d05c089f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Mar 2023 10:31:18 -0700 Subject: [PATCH] fix #6659 --- src/ast/simplifiers/dominator_simplifier.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/simplifiers/dominator_simplifier.h b/src/ast/simplifiers/dominator_simplifier.h index b412f6db0..048f6991b 100644 --- a/src/ast/simplifiers/dominator_simplifier.h +++ b/src/ast/simplifiers/dominator_simplifier.h @@ -41,7 +41,7 @@ class dominator_simplifier : public dependent_expr_simplifier { bool is_subexpr(expr * a, expr * b); 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 cache(expr *t, expr* r) { m_result.insert(t, r); m_trail.push_back(r); m_trail.push_back(t); } void reset_cache() { m_result.reset(); } ptr_vector const & tree(expr * e);