blob: bb5cd43dfa9b65ef20e4b433337a03f44726fbf0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
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)
|
