diff options
Diffstat (limited to 'test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2')
-rw-r--r-- | test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 b/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 new file mode 100644 index 000000000..539f181af --- /dev/null +++ b/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 @@ -0,0 +1,45 @@ +(set-logic UFLIA) +(set-info :status unsat) +(declare-fun P (Int) Bool) + +(assert (P 0)) +(assert (P 1)) +(assert (P 2)) +(assert (P 3)) +(assert (P 4)) +(assert (P 5)) +(assert (P 6)) +(assert (P 7)) +(assert (P 8)) +(assert (P 9)) + +(assert (P 10)) +(assert (P 11)) +(assert (P 12)) +(assert (P 13)) +(assert (P 14)) +(assert (P 15)) +(assert (P 16)) +(assert (P 17)) +(assert (P 18)) +(assert (P 19)) + +(assert (P 20)) +(assert (P 21)) +(assert (P 22)) +(assert (P 23)) +(assert (P 24)) +(assert (P 25)) +(assert (P 26)) +(assert (P 27)) +(assert (P 28)) +(assert (P 29)) + +(declare-fun Q (Int Int Int Int Int) Bool) +(assert (forall ((x Int) (y Int) (z Int) (w Int) (q Int)) (or (not (P x)) (not (P y)) (not (P z)) (not (P w)) (not (P q)) (Q x y z w q)))) + +(declare-fun R (Int) Bool) +(assert (R 0)) +(assert (forall ((x Int)) (not (R x)))) + +(check-sat) |