mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 20:05:51 +00:00
Code Activity

#6104 also in the new core

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-07-05 12:38:07 -07:00
parent de41cfd277
commit f82ca197d2
4 changed files with 32 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/sat/smt/bv_solver.cpp
View file

@ -208,7 +208,33 @@ namespace bv {
if (is_bv(eq.v1())) {
m_find.merge(eq.v1(), eq.v2());
VERIFY(eq.is_eq());
return;
}
euf::enode* n1 = var2enode(eq.v1());
euf::enode* int2bv = nullptr;
for (euf::enode* sib : euf::enode_class(n1)) {
if (bv.is_bv2int(sib->get_expr())) {
int2bv = sib;
break;
}
}
if (!int2bv)
return;
for (euf::enode* p : euf::enode_parents(n1->get_root())) {
if (bv.is_int2bv(p->get_expr())) {
euf::enode* int2bv_arg = int2bv->get_arg(0);
if (p->get_root() != int2bv_arg->get_root()) {
euf::enode_pair_vector eqs;
eqs.push_back({ n1, p->get_arg(0) });
eqs.push_back({ n1, int2bv });
ctx.propagate(p, int2bv_arg, euf::th_explain::propagate(*this, eqs, p, int2bv_arg));
break;
}
}
}
}
void solver::new_diseq_eh(euf::th_eq const& ne) {