test/regress/regress0/bug239.smt


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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185

(benchmark fuzzsmt
:logic QF_LRA
:status sat
:extrafuns ((v0 Real))
:extrafuns ((v1 Real))
:extrafuns ((v2 Real))
:formula
(let (?e3 5)
(let (?e4 0)
(let (?e5 2)
(let (?e6 (+ v0 v1))
(let (?e7 (* v1 ?e3))
(let (?e8 (~ v0))
(let (?e9 (- v2 v1))
(let (?e10 (- v0 ?e9))
(let (?e11 (* v0 (~ ?e3)))
(let (?e12 (/ ?e4 (~ ?e3)))
(let (?e13 (+ ?e8 ?e7))
(let (?e14 (/ ?e4 (~ ?e5)))
(flet ($e15 (<= v2 ?e7))
(flet ($e16 (<= ?e11 ?e11))
(flet ($e17 (= ?e11 ?e13))
(flet ($e18 (<= ?e7 ?e14))
(flet ($e19 (> ?e14 v1))
(flet ($e20 (< v0 ?e10))
(flet ($e21 (= ?e8 ?e11))
(flet ($e22 (>= ?e8 ?e13))
(flet ($e23 (< ?e10 v2))
(flet ($e24 (>= ?e10 ?e8))
(flet ($e25 (= ?e6 ?e7))
(flet ($e26 (distinct ?e12 ?e11))
(flet ($e27 (distinct ?e10 ?e9))
(let (?e28 (ite $e27 ?e13 ?e6))
(let (?e29 (ite $e21 v2 ?e28))
(let (?e30 (ite $e26 ?e12 ?e12))
(let (?e31 (ite $e18 ?e28 v0))
(let (?e32 (ite $e20 ?e9 ?e10))
(let (?e33 (ite $e22 ?e11 ?e28))
(let (?e34 (ite $e17 ?e8 ?e13))
(let (?e35 (ite $e26 ?e14 v1))
(let (?e36 (ite $e21 ?e14 ?e30))
(let (?e37 (ite $e19 ?e7 ?e11))
(let (?e38 (ite $e25 v1 ?e8))
(let (?e39 (ite $e22 ?e28 ?e28))
(let (?e40 (ite $e25 v0 ?e14))
(let (?e41 (ite $e24 ?e37 v2))
(let (?e42 (ite $e16 ?e6 v2))
(let (?e43 (ite $e19 ?e11 ?e7))
(let (?e44 (ite $e23 ?e36 v2))
(let (?e45 (ite $e20 v1 ?e7))
(let (?e46 (ite $e15 ?e45 ?e13))
(flet ($e47 (= ?e32 ?e9))
(flet ($e48 (< ?e41 v0))
(flet ($e49 (distinct ?e14 ?e43))
(flet ($e50 (distinct ?e8 ?e10))
(flet ($e51 (> ?e8 ?e37))
(flet ($e52 (< v1 ?e11))
(flet ($e53 (< ?e30 ?e8))
(flet ($e54 (< v2 ?e12))
(flet ($e55 (>= ?e8 ?e31))
(flet ($e56 (= ?e12 ?e44))
(flet ($e57 (= ?e45 v0))
(flet ($e58 (= ?e36 ?e39))
(flet ($e59 (= ?e31 v0))
(flet ($e60 (< ?e9 ?e43))
(flet ($e61 (distinct ?e14 ?e44))
(flet ($e62 (= ?e45 ?e29))
(flet ($e63 (<= ?e12 ?e9))
(flet ($e64 (>= ?e41 ?e28))
(flet ($e65 (<= ?e11 v0))
(flet ($e66 (< ?e29 ?e14))
(flet ($e67 (< ?e44 v2))
(flet ($e68 (< ?e40 ?e45))
(flet ($e69 (> ?e34 ?e7))
(flet ($e70 (= ?e38 ?e30))
(flet ($e71 (>= ?e36 ?e31))
(flet ($e72 (= ?e32 ?e38))
(flet ($e73 (<= ?e30 ?e42))
(flet ($e74 (= ?e11 ?e9))
(flet ($e75 (> ?e40 ?e7))
(flet ($e76 (distinct ?e39 ?e41))
(flet ($e77 (< ?e11 ?e28))
(flet ($e78 (distinct ?e31 ?e45))
(flet ($e79 (= ?e45 ?e11))
(flet ($e80 (>= ?e11 ?e42))
(flet ($e81 (< ?e12 ?e7))
(flet ($e82 (>= ?e11 ?e41))
(flet ($e83 (<= ?e8 v0))
(flet ($e84 (< ?e8 ?e8))
(flet ($e85 (> ?e30 v2))
(flet ($e86 (= ?e9 ?e30))
(flet ($e87 (= ?e33 ?e7))
(flet ($e88 (<= ?e32 ?e44))
(flet ($e89 (<= ?e36 ?e33))
(flet ($e90 (distinct ?e45 ?e45))
(flet ($e91 (distinct ?e14 ?e44))
(flet ($e92 (<= v1 ?e12))
(flet ($e93 (>= v0 ?e12))
(flet ($e94 (>= ?e46 ?e29))
(flet ($e95 (> ?e14 ?e6))
(flet ($e96 (>= v2 ?e14))
(flet ($e97 (>= ?e39 ?e44))
(flet ($e98 (>= ?e38 ?e28))
(flet ($e99 (> v2 ?e9))
(flet ($e100 (<= ?e42 ?e33))
(flet ($e101 (= ?e30 ?e29))
(flet ($e102 (= ?e9 v0))
(flet ($e103 (distinct ?e37 ?e40))
(flet ($e104 (= ?e43 ?e14))
(flet ($e105 (<= ?e35 ?e13))
(flet ($e106 (and $e102 $e70))
(flet ($e107 (implies $e84 $e84))
(flet ($e108 (implies $e69 $e60))
(flet ($e109 (iff $e105 $e99))
(flet ($e110 (iff $e100 $e80))
(flet ($e111 (or $e52 $e86))
(flet ($e112 (xor $e26 $e18))
(flet ($e113 (or $e20 $e107))
(flet ($e114 (not $e94))
(flet ($e115 (or $e79 $e104))
(flet ($e116 (not $e76))
(flet ($e117 (if_then_else $e112 $e22 $e90))
(flet ($e118 (xor $e77 $e57))
(flet ($e119 (xor $e88 $e55))
(flet ($e120 (and $e92 $e68))
(flet ($e121 (or $e82 $e25))
(flet ($e122 (implies $e19 $e119))
(flet ($e123 (implies $e66 $e117))
(flet ($e124 (if_then_else $e15 $e73 $e65))
(flet ($e125 (iff $e64 $e103))
(flet ($e126 (iff $e121 $e122))
(flet ($e127 (if_then_else $e50 $e47 $e101))
(flet ($e128 (iff $e81 $e127))
(flet ($e129 (implies $e124 $e21))
(flet ($e130 (iff $e87 $e129))
(flet ($e131 (iff $e116 $e51))
(flet ($e132 (implies $e72 $e97))
(flet ($e133 (and $e56 $e98))
(flet ($e134 (implies $e91 $e53))
(flet ($e135 (xor $e133 $e114))
(flet ($e136 (xor $e17 $e110))
(flet ($e137 (iff $e96 $e128))
(flet ($e138 (or $e125 $e59))
(flet ($e139 (or $e23 $e48))
(flet ($e140 (iff $e62 $e95))
(flet ($e141 (not $e61))
(flet ($e142 (and $e132 $e63))
(flet ($e143 (xor $e109 $e131))
(flet ($e144 (iff $e54 $e126))
(flet ($e145 (xor $e74 $e67))
(flet ($e146 (if_then_else $e89 $e93 $e140))
(flet ($e147 (iff $e71 $e138))
(flet ($e148 (and $e143 $e146))
(flet ($e149 (xor $e147 $e142))
(flet ($e150 (implies $e85 $e58))
(flet ($e151 (or $e24 $e78))
(flet ($e152 (if_then_else $e137 $e113 $e123))
(flet ($e153 (and $e145 $e16))
(flet ($e154 (not $e150))
(flet ($e155 (implies $e151 $e154))
(flet ($e156 (if_then_else $e118 $e136 $e75))
(flet ($e157 (and $e108 $e108))
(flet ($e158 (or $e83 $e141))
(flet ($e159 (iff $e155 $e149))
(flet ($e160 (iff $e158 $e156))
(flet ($e161 (or $e115 $e130))
(flet ($e162 (or $e157 $e160))
(flet ($e163 (if_then_else $e152 $e153 $e139))
(flet ($e164 (not $e144))
(flet ($e165 (not $e27))
(flet ($e166 (or $e148 $e162))
(flet ($e167 (iff $e134 $e166))
(flet ($e168 (or $e111 $e159))
(flet ($e169 (or $e106 $e164))
(flet ($e170 (xor $e161 $e120))
(flet ($e171 (and $e168 $e165))
(flet ($e172 (or $e170 $e135))
(flet ($e173 (or $e169 $e163))
(flet ($e174 (implies $e49 $e172))
(flet ($e175 (xor $e174 $e173))
(flet ($e176 (and $e171 $e175))
(flet ($e177 (implies $e167 $e176))
$e177
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))