mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
l -> eq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
dd9aec5552
commit
1634a21e75
|
@ -120,7 +120,7 @@ namespace smt {
|
||||||
literal eq = mk_eq(t1, t2, false);
|
literal eq = mk_eq(t1, t2, false);
|
||||||
for (auto const& kv : m_relations) {
|
for (auto const& kv : m_relations) {
|
||||||
relation& r = *kv.m_value;
|
relation& r = *kv.m_value;
|
||||||
if (!r.new_eq_eh(l, v1, v2)) {
|
if (!r.new_eq_eh(eq, v1, v2)) {
|
||||||
set_neg_cycle_conflict(r);
|
set_neg_cycle_conflict(r);
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in a new issue