mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
check for m.get_sort(lhs->get_owner()) == m.get_sort(rhs->get_owner()) in equality propagation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
4b6ca6a10c
commit
6ced6995d0
|
@ -417,7 +417,9 @@ public:
|
|||
TRACE("cheap_eq", tout << "reporting eq " << j << ", " << k << "\n";
|
||||
for (auto p : exp) {
|
||||
lp().constraints().display(tout, [this](lpvar j) { return lp().get_variable_name(j);}, p.ci());
|
||||
});
|
||||
}
|
||||
tout << "theory_vars v" << lp().local_to_external(je) << " == v" << lp().local_to_external(ke) << "\n";
|
||||
);
|
||||
|
||||
m_imp.add_eq(je, ke, exp);
|
||||
lp().settings().stats().m_cheap_eqs++;
|
||||
|
|
|
@ -2423,7 +2423,8 @@ public:
|
|||
theory_var vv = lp().local_to_external(v); // so maybe better to have them already transformed to external form
|
||||
enode* n1 = get_enode(uv);
|
||||
enode* n2 = get_enode(vv);
|
||||
if (n1->get_root() == n2->get_root())
|
||||
if (n1->get_root() == n2->get_root() ||
|
||||
m.get_sort(n1->get_owner()) != m.get_sort(n2->get_owner()))
|
||||
return;
|
||||
reset_evidence();
|
||||
for (auto const& ev : e)
|
||||
|
|
Loading…
Reference in a new issue