blob: d55e15925fff65251517e4fb6fb3f2f0a95b9d1f (
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
30
31
32
33
34
35
|
; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel --lang=smt2.5
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(declare-datatypes () ((Nat (succ (pred Nat)) (zero)) (Lst (cons (hd Nat) (tl Lst)) (nil))))
(declare-fun app (Lst Lst) Lst)
(declare-fun rev (Lst) Lst)
(declare-sort I_app 0)
(declare-sort I_rev 0)
(declare-fun a () I_app)
(declare-fun b () I_app)
(assert (not (= a b)))
(declare-fun app_0_3 (I_app) Lst)
(declare-fun app_1_4 (I_app) Lst)
(declare-fun rev_0_5 (I_rev) Lst)
(declare-fun xs () Lst)
(assert (and
(forall ((?i I_app)) (= (app (app_0_3 ?i) (app_1_4 ?i)) (ite (is-cons (app_0_3 ?i)) (cons (hd (app_0_3 ?i)) (app (tl (app_0_3 ?i)) (app_1_4 ?i))) (app_1_4 ?i))) )
(forall ((?i I_rev)) (= (rev (rev_0_5 ?i)) (ite (is-cons (rev_0_5 ?i)) (app (rev (tl (rev_0_5 ?i))) (cons (hd (rev_0_5 ?i)) nil)) nil)) )
(forall ((?i I_rev)) (or (not (is-cons (rev_0_5 ?i))) (and (not (forall ((?z I_app)) (not (and (= (app_0_3 ?z) (rev (tl (rev_0_5 ?i)))) (= (app_1_4 ?z) (cons (hd (rev_0_5 ?i)) nil)))) )) (not (forall ((?z I_rev)) (not (= (rev_0_5 ?z) (tl (rev_0_5 ?i)) )) )))) )
(not (or (= xs (rev xs)) (forall ((?z I_rev)) (not (= (rev_0_5 ?z) xs)) )))
))
(check-sat)
|
