mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
detect conflicts in cut_simplifier
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d8423a4b46
commit
dc31478d82
|
@ -358,6 +358,13 @@ namespace sat {
|
|||
}
|
||||
while (first != idx);
|
||||
}
|
||||
for (unsigned i = s.num_vars(); i-- > 0; ) {
|
||||
literal lit(i, false);
|
||||
if (uf2.find(lit.index()) == uf2.find((~lit).index())) {
|
||||
s.set_conflict();
|
||||
return;
|
||||
}
|
||||
}
|
||||
if (new_eq) {
|
||||
elim_eqs elim(s);
|
||||
elim(uf2);
|
||||
|
|
Loading…
Reference in a new issue