blob: b43920c2175cbed83dc6278b1035f582be28e0af (
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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
|
; EXPECT: unsat
(set-logic HO_ALL)
(declare-sort A$ 0)
(declare-sort Com$ 0)
(declare-sort Loc$ 0)
(declare-sort Nat$ 0)
(declare-sort Pname$ 0)
(declare-sort State$ 0)
(declare-sort Vname$ 0)
(declare-sort Literal$ 0)
(declare-sort Natural$ 0)
(declare-sort Typerep$ 0)
(declare-sort A_triple$ 0)
(declare-sort Com_option$ 0)
(declare-fun p$ () (-> A$ (-> State$ Bool)))
(declare-fun q$ () (-> A$ (-> State$ Bool)))
(declare-fun pn$ () Pname$)
(declare-fun wt$ (Com$) Bool)
(declare-fun ass$ (Vname$ (-> State$ Nat$)) Com$)
(declare-fun suc$ (Nat$) Nat$)
(declare-fun the$ (Com_option$) Com$)
(declare-fun body$ (Pname$) Com$)
(declare-fun call$ (Vname$ Pname$ (-> State$ Nat$)) Com$)
(declare-fun cond$ ((-> State$ Bool) Com$ Com$) Com$)
(declare-fun none$ () Com_option$)
(declare-fun plus$ (Nat$ Nat$) Nat$)
(declare-fun semi$ (Com$ Com$) Com$)
(declare-fun size$ (A_triple$) Nat$)
(declare-fun skip$ () Com$)
(declare-fun some$ (Com$) Com_option$)
(declare-fun suc$a (Natural$) Natural$)
(declare-fun zero$ () Nat$)
(declare-fun body$a (Pname$) Com_option$)
(declare-fun evalc$ (Com$ State$ State$) Bool)
(declare-fun evaln$ (Com$ State$ Nat$ State$) Bool)
(declare-fun local$ (Loc$ (-> State$ Nat$) Com$) Com$)
(declare-fun plus$a (Natural$ Natural$) Natural$)
(declare-fun size$a (Com$) Nat$)
(declare-fun size$b (Natural$) Nat$)
(declare-fun size$c (Bool) Nat$)
(declare-fun size$d (Com_option$) Nat$)
(declare-fun size$e (Typerep$) Nat$)
(declare-fun size$f (Literal$) Nat$)
(declare-fun while$ ((-> State$ Bool) Com$) Com$)
(declare-fun zero$a () Natural$)
(declare-fun triple$ ((-> A$ (-> State$ Bool)) Com$ (-> A$ (-> State$ Bool))) A_triple$)
(declare-fun rec_bool$ (Nat$ Nat$) (-> Bool Nat$))
(declare-fun size_com$ (Com$) Nat$)
(declare-fun size_bool$ (Bool) Nat$)
(declare-fun wT_bodies$ () Bool)
(declare-fun size_option$ ((-> Com$ Nat$)) (-> Com_option$ Nat$))
(declare-fun size_triple$ ((-> A$ Nat$) A_triple$) Nat$)
(declare-fun size_natural$ (Natural$) Nat$)
(declare-fun triple_valid$ (Nat$ A_triple$) Bool)
(assert (! (not (triple_valid$ zero$ (triple$ p$ (body$ pn$) q$))) :named a0))
(assert (! (forall ((?v0 Nat$) (?v1 (-> A$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> A$ (-> State$ Bool)))) (= (triple_valid$ ?v0 (triple$ ?v1 ?v2 ?v3)) (forall ((?v4 A$) (?v5 State$)) (=> (?v1 ?v4 ?v5) (forall ((?v6 State$)) (=> (evaln$ ?v2 ?v5 ?v0 ?v6) (?v3 ?v4 ?v6))))))) :named a6))
(assert (! (= (size_bool$ true) zero$) :named a13))
(assert (! (= size_bool$ (rec_bool$ zero$ zero$)) :named a14))
(assert (! (forall ((?v0 Nat$)) (not (= zero$ (suc$ ?v0)))) :named a37))
(assert (! (forall ((?v0 Pname$) (?v1 State$) (?v2 Nat$) (?v3 State$)) (=> (and (evaln$ (body$ ?v0) ?v1 ?v2 ?v3) (forall ((?v4 Nat$)) (=> (and (= ?v2 (suc$ ?v4)) (evaln$ (the$ (body$a ?v0)) ?v1 ?v4 ?v3)) false))) false)) :named a204))
(check-sat)
;(get-proof)
|
