fix #6659

Z3Prover · Mar 31, 2023 · a849a29 · a849a29
1 parent 6aaaa3b
commit a849a29
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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<expr> const & tree(expr * e);