mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
This commit is contained in:
parent
89ed19a719
commit
614cb26489
|
@ -342,7 +342,7 @@ namespace euf {
|
|||
break;
|
||||
propagated = true;
|
||||
}
|
||||
DEBUG_CODE(if (!s().inconsistent()) check_missing_eq_propagation(););
|
||||
DEBUG_CODE(if (!propagated && !s().inconsistent()) check_missing_eq_propagation(););
|
||||
return propagated;
|
||||
}
|
||||
|
||||
|
@ -354,7 +354,7 @@ namespace euf {
|
|||
bool_var v = n->bool_var();
|
||||
SASSERT(m.is_bool(e));
|
||||
size_t cnstr;
|
||||
literal lit;
|
||||
literal lit;
|
||||
if (is_eq) {
|
||||
VERIFY(m.is_eq(e, a, b));
|
||||
cnstr = eq_constraint().to_index();
|
||||
|
|
Loading…
Reference in a new issue