From a23a8cdfc5a9d3bf6d6ce287d58752cb4a7227ea Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 Oct 2024 19:08:33 -0700 Subject: [PATCH] add variables from definitions Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/model_reconstruction_trail.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp index 500e67f78..6905e0967 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.cpp +++ b/src/ast/simplifiers/model_reconstruction_trail.cpp @@ -76,8 +76,10 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt // and their removed formulas are added to the resulting constraints. if (t->is_loose() && !t->is_def() && t->is_subst()) { - for (auto const& [k, v] : t->m_subst->sub()) + for (auto const& [k, v] : t->m_subst->sub()) { + add_vars(v, free_vars); st.add(dependent_expr(m, m.mk_eq(k, v), nullptr, nullptr)); + } t->m_active = false; continue; }