blob: 87a8696b6b343e4f12fac557ab7a834b365159d1 (
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
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
; COMMAND-LINE: --lang=smt2.5
; EXPECT: sat
; Preamble --------------
(set-logic ALL)
(set-info :status sat)
(declare-datatypes () ((UNIT (Unit))))
(declare-datatypes () ((BOOL (Truth) (Falsity))))
; Decls --------------
(declare-sort A 0)
(declare-sort B 0)
(declare-sort C 0)
(declare-sort D 0)
(declare-datatypes () ((E (one) (two) (three))))
(declare-datatypes () ((F (four) (five) (six))))
(declare-datatypes () ((G (c_G (seven BOOL)))))
(declare-datatypes ()
((H
(c_H
(foo1 BOOL)
(foo2 A)
(foo3 B)
(foo4 B)
(foo5 Int)
)
))
)
(declare-datatypes ()
((I
(c_I
(bar1 E)
(bar2 Int)
(bar3 Int)
(bar4 A)
)
))
)
(declare-datatypes ()
((J
(c_J
(f1 BOOL)
(f2 Int)
(f3 Int)
(f4 Int)
(f5 I)
(f6 B)
(f7 C)
)
))
)
(declare-datatypes ()
((K
(c_K
(g1 BOOL)
(g2 F)
(g3 A)
(g4 BOOL)
)
))
)
; Var Decls --------------
(declare-fun s1 () (Array A J))
(declare-fun s2 () (Array A J))
(declare-fun e1 () (Array A K))
(declare-fun e2 () (Array A K))
(declare-fun x () A)
(declare-fun y () A)
(declare-fun foo (A) A)
(declare-fun bar (A) C)
; Asserts --------------
(assert
(not
(=
(ite
(=>
(= y (g3 (select e1 x)))
(=>
(= s2
(store
s1
y
(let ((z (select s1 y)))
(c_J
(f1 z)
(f2 z)
(- (f3 (select s1 y)) 1)
(f4 z)
(f5 z)
(f6 z)
(f7 z)
)
)
)
)
(forall ((s A)) (= (g3 (select e2 s)) s))
)
)
Truth
Falsity
)
Truth
)
)
)
(check-sat)
|
