mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

add variables from definitions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-16 19:08:33 -07:00
parent 92376e67f2
commit a23a8cdfc5
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/simplifiers/model_reconstruction_trail.cpp
View file

@ -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;
}