diff options
Diffstat (limited to 'test/regress/regress0/nl/nl-unk-quant.smt2')
| -rw-r--r-- | test/regress/regress0/nl/nl-unk-quant.smt2 | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/test/regress/regress0/nl/nl-unk-quant.smt2 b/test/regress/regress0/nl/nl-unk-quant.smt2 deleted file mode 100644 index bb5cd43df..000000000 --- a/test/regress/regress0/nl/nl-unk-quant.smt2 +++ /dev/null @@ -1,29 +0,0 @@ -; COMMAND-LINE: --nl-ext -; EXPECT: unsat -(set-logic UFNIA) -(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|) -(set-info :smt-lib-version 2.0) -(set-info :category "industrial") -(set-info :status unsat) -(declare-sort S1 0) -(declare-sort S2 0) -(declare-sort S3 0) -(declare-sort S4 0) -(declare-fun f1 () S1) -(declare-fun f2 () S1) -(declare-fun f3 () S2) -(declare-fun f4 (S3 Int) S2) -(declare-fun f5 () S3) -(declare-fun f6 (S4 S2) Int) -(declare-fun f7 () S4) -(declare-fun f8 () Int) -(declare-fun f9 (Int) S1) -(declare-fun f10 () Int) -(declare-fun f11 () S2) -(assert (not (= f1 f2))) -(assert (let ((?v_0 (f6 f7 f3)) (?v_1 (f6 f7 f11))) (not (=> (and (= f3 (f4 f5 (- (f6 f7 (f4 f5 f8)) 1))) (= (f9 (* (+ (* 4 f10) 1) (+ 1 ?v_0))) f1)) (=> (< f8 (+ 1 ?v_1)) (=> (< 0 f8) (< ?v_0 ?v_1))))))) -(assert (forall ((?v0 S2)) (= (f4 f5 (f6 f7 ?v0)) ?v0))) -(assert (forall ((?v0 Int)) (=> (<= 0 ?v0) (= (f6 f7 (f4 f5 ?v0)) ?v0)))) -(assert (forall ((?v0 Int)) (=> (< ?v0 0) (= (f6 f7 (f4 f5 ?v0)) 0)))) -(check-sat) -(exit) |