diff options
Diffstat (limited to 'src/lfsc/tests/hole.smt2')
-rw-r--r-- | src/lfsc/tests/hole.smt2 | 99 |
1 files changed, 99 insertions, 0 deletions
diff --git a/src/lfsc/tests/hole.smt2 b/src/lfsc/tests/hole.smt2 new file mode 100644 index 0000000..3c07466 --- /dev/null +++ b/src/lfsc/tests/hole.smt2 @@ -0,0 +1,99 @@ +(set-logic QF_UF) +(declare-fun a1 () Bool) +(declare-fun a2 () Bool) +(declare-fun a3 () Bool) +(declare-fun a4 () Bool) +(declare-fun a5 () Bool) +(declare-fun a6 () Bool) +(declare-fun a7 () Bool) +(declare-fun a8 () Bool) +(declare-fun a9 () Bool) +(declare-fun a10 () Bool) +(declare-fun a11 () Bool) +(declare-fun a12 () Bool) +(declare-fun a13 () Bool) +(declare-fun a14 () Bool) +(declare-fun a15 () Bool) +(declare-fun a16 () Bool) +(declare-fun a17 () Bool) +(declare-fun a18 () Bool) +(declare-fun a19 () Bool) +(declare-fun a20 () Bool) +(assert +(and (or a1 (or a2 (or a3 a4))) +(and (or a5 (or a6 (or a7 a8))) +(and (or a9 (or a10 (or a11 a12))) +(and (or a13 (or a14 (or a15 a16))) +(and (or a17 (or a18 (or a19 a20))) +(and (or (not a1) (not a2)) +(and (or (not a1) (not a3)) +(and (or (not a1) (not a4)) +(and (or (not a2) (not a3)) +(and (or (not a2) (not a4)) +(and (or (not a3) (not a4)) +(and (or (not a5) (not a6)) +(and (or (not a5) (not a7)) +(and (or (not a5) (not a8)) +(and (or (not a6) (not a7)) +(and (or (not a6) (not a8)) +(and (or (not a7) (not a8)) +(and (or (not a9) (not a10)) +(and (or (not a9) (not a11)) +(and (or (not a9) (not a12)) +(and (or (not a10) (not a11)) +(and (or (not a10) (not a12)) +(and (or (not a11) (not a12)) +(and (or (not a13) (not a14)) +(and (or (not a13) (not a15)) +(and (or (not a13) (not a16)) +(and (or (not a14) (not a15)) +(and (or (not a14) (not a16)) +(and (or (not a15) (not a16)) +(and (or (not a17) (not a18)) +(and (or (not a17) (not a19)) +(and (or (not a17) (not a20)) +(and (or (not a18) (not a19)) +(and (or (not a18) (not a20)) +(and (or (not a19) (not a20)) +(and (or (not a1) (not a5)) +(and (or (not a1) (not a9)) +(and (or (not a1) (not a13)) +(and (or (not a1) (not a17)) +(and (or (not a5) (not a9)) +(and (or (not a5) (not a13)) +(and (or (not a5) (not a17)) +(and (or (not a9) (not a13)) +(and (or (not a9) (not a17)) +(and (or (not a13) (not a17)) +(and (or (not a2) (not a6)) +(and (or (not a2) (not a10)) +(and (or (not a2) (not a14)) +(and (or (not a2) (not a18)) +(and (or (not a6) (not a10)) +(and (or (not a6) (not a14)) +(and (or (not a6) (not a18)) +(and (or (not a10) (not a14)) +(and (or (not a10) (not a18)) +(and (or (not a14) (not a18)) +(and (or (not a3) (not a7)) +(and (or (not a3) (not a11)) +(and (or (not a3) (not a15)) +(and (or (not a3) (not a19)) +(and (or (not a7) (not a11)) +(and (or (not a7) (not a15)) +(and (or (not a7) (not a19)) +(and (or (not a11) (not a15)) +(and (or (not a11) (not a19)) +(and (or (not a15) (not a19)) +(and (or (not a4) (not a8)) +(and (or (not a4) (not a12)) +(and (or (not a4) (not a16)) +(and (or (not a4) (not a20)) +(and (or (not a8) (not a12)) +(and (or (not a8) (not a16)) +(and (or (not a8) (not a20)) +(and (or (not a12) (not a16)) +(and (or (not a12) (not a20)) +(or (not a16) (not a20))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(check-sat) +(exit) |