mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

bug fix for #6319

Browse source 
literals that are replayed need to be registered with respective theories, otherwise, they will not propagate with the theories (the enode have to be attached with relevant theory variables).
This commit is contained in:
Nikolaj Bjorner 2022-09-18 17:22:44 -07:00
parent e54635e0ed
commit 13f43ea107
1 changed files with 11 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/sat/smt/euf_solver.cpp
View file

@ -616,15 +616,17 @@ namespace euf {
else
lit = si.internalize(e, false);
VERIFY(lit.var() == v);
if (!m_egraph.find(e) && (!m.is_iff(e) && !m.is_or(e) && !m.is_and(e) && !m.is_not(e))) {
if (!m_egraph.find(e) && !m.is_iff(e) && !m.is_or(e) && !m.is_and(e) && !m.is_not(e) && !m.is_implies(e) && !m.is_xor(e)) {
ptr_buffer<euf::enode> args;
if (is_app(e))
for (expr* arg : *to_app(e))
args.push_back(e_internalize(arg));
internalize(e, true);
if (!m_egraph.find(e))
mk_enode(e, args.size(), args.data());
}
attach_lit(lit, e);
else
attach_lit(lit, e);
}
if (relevancy_enabled())
@ -863,7 +865,13 @@ namespace euf {
out << "bool-vars\n";
for (unsigned v : m_var_trail) {
expr* e = m_bool_var2expr[v];
out << v << (is_relevant(v)?"":"n") << ": " << e->get_id() << " " << m_solver->value(v) << " " << mk_bounded_pp(e, m, 1) << "\n";
out << v << (is_relevant(v)?"":"n") << ": " << e->get_id() << " " << m_solver->value(v) << " " << mk_bounded_pp(e, m, 1);
euf::enode* n = m_egraph.find(e);
if (n) {
for (auto const& th : enode_th_vars(n))
out << " " << m_id2solver[th.get_id()]->name();
}
out << "\n";
}
for (auto* e : m_solvers)
e->display(out);