diff options
Diffstat (limited to 'test/regress/regress1/nl/nl-unk-quant.smt2')
| -rw-r--r-- | test/regress/regress1/nl/nl-unk-quant.smt2 | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/test/regress/regress1/nl/nl-unk-quant.smt2 b/test/regress/regress1/nl/nl-unk-quant.smt2 new file mode 100644 index 000000000..bb5cd43df --- /dev/null +++ b/test/regress/regress1/nl/nl-unk-quant.smt2 @@ -0,0 +1,29 @@ +; 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) |