mirror of
https://github.com/Z3Prover/z3
synced 2025-06-06 06:03:23 +00:00
n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
1149955893
commit
340b460f74
1 changed files with 1 additions and 0 deletions
|
@ -1117,6 +1117,7 @@ namespace sat {
|
||||||
if (was_eliminated) continue;
|
if (was_eliminated) continue;
|
||||||
|
|
||||||
switch (c.size()) {
|
switch (c.size()) {
|
||||||
|
case 0: set_conflict(); break;
|
||||||
case 1: assign(c[0]); break;
|
case 1: assign(c[0]); break;
|
||||||
case 2: add_binary(c[0],c[1]); break;
|
case 2: add_binary(c[0],c[1]); break;
|
||||||
case 3: add_ternary(c[0],c[1],c[2]); break;
|
case 3: add_ternary(c[0],c[1],c[2]); break;
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue