3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-15 00:24:43 -07:00
parent b7d4501bc3
commit bebf2d6a52

View file

@ -339,7 +339,7 @@ void der::apply_substitution(quantifier * q, expr_ref_vector& ors, expr_ref & r)
m_new_args.push_back(ors.get(i));
}
expr_ref t = mk_or(m, m_new_args.size(), m_new_args.data());
expr_ref t(mk_or(m, m_new_args.size(), m_new_args.data()), m);
expr_ref new_e = m_subst(t, m_subst_map);
// don't forget to update the quantifier patterns