mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
More cases needed to find all ite clauses.
This commit is contained in:
parent
00e43b6b88
commit
290b4dfabc
|
@ -217,8 +217,11 @@ namespace sat {
|
|||
if (c.size() != 3 || c.was_used()) continue;
|
||||
literal x = c[0], y = c[1], z = c[2];
|
||||
if (try_ite(x, z, y, c)) continue;
|
||||
if (try_ite(x, y, z, c)) continue;
|
||||
if (try_ite(y, x, z, c)) continue;
|
||||
if (try_ite(z, y, x, c)) continue;
|
||||
if (try_ite(z, x, y, c)) continue;
|
||||
if (try_ite(z, y, x, c)) continue;
|
||||
if (try_ite(y, z, x, c)) continue;
|
||||
}
|
||||
|
||||
std::function<bool(clause*)> not_used = [](clause* cp) { return !cp->was_used(); };
|
||||
|
|
Loading…
Reference in a new issue