Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_comparetozero_test / comparetozero_test.smt2 @ 6c3ea955

History | View | Annotate | Download (17.2 KB)

1
; comparetozero_test
2
(declare-var comparetozero_test.In1_1_1 Real)
3
(declare-var comparetozero_test.In2_1_1 Int)
4
(declare-var comparetozero_test.In3_1_1 Bool)
5
(declare-var comparetozero_test.In4_1_1 Real)
6
(declare-var comparetozero_test.In4_1_2 Real)
7
(declare-var comparetozero_test.In4_1_3 Real)
8
(declare-var comparetozero_test.In5_1_1 Int)
9
(declare-var comparetozero_test.In5_1_2 Int)
10
(declare-var comparetozero_test.In5_1_3 Int)
11
(declare-var comparetozero_test.In6_1_1 Bool)
12
(declare-var comparetozero_test.In6_1_2 Bool)
13
(declare-var comparetozero_test.In6_1_3 Bool)
14
(declare-var comparetozero_test.In7_1_1 Real)
15
(declare-var comparetozero_test.In7_1_2 Real)
16
(declare-var comparetozero_test.In7_1_3 Real)
17
(declare-var comparetozero_test.In7_1_4 Real)
18
(declare-var comparetozero_test.In7_1_5 Real)
19
(declare-var comparetozero_test.In7_1_6 Real)
20
(declare-var comparetozero_test.In8_1_1 Int)
21
(declare-var comparetozero_test.In8_1_2 Int)
22
(declare-var comparetozero_test.In8_1_3 Int)
23
(declare-var comparetozero_test.In8_1_4 Int)
24
(declare-var comparetozero_test.In8_1_5 Int)
25
(declare-var comparetozero_test.In8_1_6 Int)
26
(declare-var comparetozero_test.In9_1_1 Bool)
27
(declare-var comparetozero_test.In9_1_2 Bool)
28
(declare-var comparetozero_test.In9_1_3 Bool)
29
(declare-var comparetozero_test.In9_1_4 Bool)
30
(declare-var comparetozero_test.In9_1_5 Bool)
31
(declare-var comparetozero_test.In9_1_6 Bool)
32
(declare-var comparetozero_test.Out1_1_1 Bool)
33
(declare-var comparetozero_test.Out2_2_1 Bool)
34
(declare-var comparetozero_test.Out3_3_1 Bool)
35
(declare-var comparetozero_test.Out4_4_1 Bool)
36
(declare-var comparetozero_test.Out4_4_2 Bool)
37
(declare-var comparetozero_test.Out4_4_3 Bool)
38
(declare-var comparetozero_test.Out5_5_1 Bool)
39
(declare-var comparetozero_test.Out5_5_2 Bool)
40
(declare-var comparetozero_test.Out5_5_3 Bool)
41
(declare-var comparetozero_test.Out6_6_1 Bool)
42
(declare-var comparetozero_test.Out6_6_2 Bool)
43
(declare-var comparetozero_test.Out6_6_3 Bool)
44
(declare-var comparetozero_test.Out7_7_1 Bool)
45
(declare-var comparetozero_test.Out7_7_2 Bool)
46
(declare-var comparetozero_test.Out7_7_3 Bool)
47
(declare-var comparetozero_test.Out7_7_4 Bool)
48
(declare-var comparetozero_test.Out7_7_5 Bool)
49
(declare-var comparetozero_test.Out7_7_6 Bool)
50
(declare-var comparetozero_test.Out8_8_1 Bool)
51
(declare-var comparetozero_test.Out8_8_2 Bool)
52
(declare-var comparetozero_test.Out8_8_3 Bool)
53
(declare-var comparetozero_test.Out8_8_4 Bool)
54
(declare-var comparetozero_test.Out8_8_5 Bool)
55
(declare-var comparetozero_test.Out8_8_6 Bool)
56
(declare-var comparetozero_test.Out9_9_1 Bool)
57
(declare-var comparetozero_test.Out9_9_2 Bool)
58
(declare-var comparetozero_test.Out9_9_3 Bool)
59
(declare-var comparetozero_test.Out9_9_4 Bool)
60
(declare-var comparetozero_test.Out9_9_5 Bool)
61
(declare-var comparetozero_test.Out9_9_6 Bool)
62
(declare-var comparetozero_test.ni_0._arrow._first_c Bool)
63
(declare-var comparetozero_test.ni_0._arrow._first_m Bool)
64
(declare-var comparetozero_test.ni_0._arrow._first_x Bool)
65
(declare-var comparetozero_test.CompareToZero1_1_1 Bool)
66
(declare-var comparetozero_test.CompareToZero2_1_1 Bool)
67
(declare-var comparetozero_test.CompareToZero3_1_1 Bool)
68
(declare-var comparetozero_test.CompareToZero3_1_2 Bool)
69
(declare-var comparetozero_test.CompareToZero3_1_3 Bool)
70
(declare-var comparetozero_test.CompareToZero4_1_1 Bool)
71
(declare-var comparetozero_test.CompareToZero4_1_2 Bool)
72
(declare-var comparetozero_test.CompareToZero4_1_3 Bool)
73
(declare-var comparetozero_test.CompareToZero5_1_1 Bool)
74
(declare-var comparetozero_test.CompareToZero5_1_2 Bool)
75
(declare-var comparetozero_test.CompareToZero5_1_3 Bool)
76
(declare-var comparetozero_test.CompareToZero6_1_1 Bool)
77
(declare-var comparetozero_test.CompareToZero6_1_2 Bool)
78
(declare-var comparetozero_test.CompareToZero6_1_3 Bool)
79
(declare-var comparetozero_test.CompareToZero6_1_4 Bool)
80
(declare-var comparetozero_test.CompareToZero6_1_5 Bool)
81
(declare-var comparetozero_test.CompareToZero6_1_6 Bool)
82
(declare-var comparetozero_test.CompareToZero7_1_1 Bool)
83
(declare-var comparetozero_test.CompareToZero7_1_2 Bool)
84
(declare-var comparetozero_test.CompareToZero7_1_3 Bool)
85
(declare-var comparetozero_test.CompareToZero7_1_4 Bool)
86
(declare-var comparetozero_test.CompareToZero7_1_5 Bool)
87
(declare-var comparetozero_test.CompareToZero7_1_6 Bool)
88
(declare-var comparetozero_test.CompareToZero8_1_1 Bool)
89
(declare-var comparetozero_test.CompareToZero8_1_2 Bool)
90
(declare-var comparetozero_test.CompareToZero8_1_3 Bool)
91
(declare-var comparetozero_test.CompareToZero8_1_4 Bool)
92
(declare-var comparetozero_test.CompareToZero8_1_5 Bool)
93
(declare-var comparetozero_test.CompareToZero8_1_6 Bool)
94
(declare-var comparetozero_test.CompareToZero_1_1 Bool)
95
(declare-var comparetozero_test.__comparetozero_test_1 Bool)
96
(declare-var comparetozero_test.__comparetozero_test_10 Real)
97
(declare-var comparetozero_test.__comparetozero_test_11 Real)
98
(declare-var comparetozero_test.__comparetozero_test_2 Real)
99
(declare-var comparetozero_test.__comparetozero_test_3 Real)
100
(declare-var comparetozero_test.__comparetozero_test_4 Real)
101
(declare-var comparetozero_test.__comparetozero_test_5 Real)
102
(declare-var comparetozero_test.__comparetozero_test_6 Real)
103
(declare-var comparetozero_test.__comparetozero_test_7 Real)
104
(declare-var comparetozero_test.__comparetozero_test_8 Real)
105
(declare-var comparetozero_test.__comparetozero_test_9 Real)
106
(declare-var comparetozero_test.i_virtual_local Real)
107
(declare-rel comparetozero_test_reset (Bool Bool))
108
(declare-rel comparetozero_test_step (Real Int Bool Real Real Real Int Int Int Bool Bool Bool Real Real Real Real Real Real Int Int Int Int Int Int Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
109

    
110
(rule (=> 
111
  (and 
112
       
113
       (= comparetozero_test.ni_0._arrow._first_m true)
114
  )
115
  (comparetozero_test_reset comparetozero_test.ni_0._arrow._first_c
116
                            comparetozero_test.ni_0._arrow._first_m)
117
))
118

    
119
(rule (=> 
120
  (and (= comparetozero_test.ni_0._arrow._first_m comparetozero_test.ni_0._arrow._first_c)
121
       (and (= comparetozero_test.__comparetozero_test_1 (ite comparetozero_test.ni_0._arrow._first_m true false))
122
            (= comparetozero_test.ni_0._arrow._first_x false))
123
       (and (or (not (= comparetozero_test.__comparetozero_test_1 true))
124
               (= comparetozero_test.i_virtual_local 0.0))
125
            (or (not (= comparetozero_test.__comparetozero_test_1 false))
126
               (= comparetozero_test.i_virtual_local 1.0))
127
       )
128
       (and (or (not (= comparetozero_test.In6_1_2 true))
129
               (= comparetozero_test.__comparetozero_test_9 1.0))
130
            (or (not (= comparetozero_test.In6_1_2 false))
131
               (= comparetozero_test.__comparetozero_test_9 0.0))
132
       )
133
       (and (or (not (= comparetozero_test.In6_1_3 true))
134
               (= comparetozero_test.__comparetozero_test_8 1.0))
135
            (or (not (= comparetozero_test.In6_1_3 false))
136
               (= comparetozero_test.__comparetozero_test_8 0.0))
137
       )
138
       (and (or (not (= comparetozero_test.In9_1_1 true))
139
               (= comparetozero_test.__comparetozero_test_7 1.0))
140
            (or (not (= comparetozero_test.In9_1_1 false))
141
               (= comparetozero_test.__comparetozero_test_7 0.0))
142
       )
143
       (and (or (not (= comparetozero_test.In9_1_2 true))
144
               (= comparetozero_test.__comparetozero_test_6 1.0))
145
            (or (not (= comparetozero_test.In9_1_2 false))
146
               (= comparetozero_test.__comparetozero_test_6 0.0))
147
       )
148
       (and (or (not (= comparetozero_test.In9_1_3 true))
149
               (= comparetozero_test.__comparetozero_test_5 1.0))
150
            (or (not (= comparetozero_test.In9_1_3 false))
151
               (= comparetozero_test.__comparetozero_test_5 0.0))
152
       )
153
       (and (or (not (= comparetozero_test.In9_1_4 true))
154
               (= comparetozero_test.__comparetozero_test_4 1.0))
155
            (or (not (= comparetozero_test.In9_1_4 false))
156
               (= comparetozero_test.__comparetozero_test_4 0.0))
157
       )
158
       (and (or (not (= comparetozero_test.In9_1_5 true))
159
               (= comparetozero_test.__comparetozero_test_3 1.0))
160
            (or (not (= comparetozero_test.In9_1_5 false))
161
               (= comparetozero_test.__comparetozero_test_3 0.0))
162
       )
163
       (and (or (not (= comparetozero_test.In9_1_6 true))
164
               (= comparetozero_test.__comparetozero_test_2 1.0))
165
            (or (not (= comparetozero_test.In9_1_6 false))
166
               (= comparetozero_test.__comparetozero_test_2 0.0))
167
       )
168
       (and (or (not (= comparetozero_test.In3_1_1 true))
169
               (= comparetozero_test.__comparetozero_test_11 1.0))
170
            (or (not (= comparetozero_test.In3_1_1 false))
171
               (= comparetozero_test.__comparetozero_test_11 0.0))
172
       )
173
       (and (or (not (= comparetozero_test.In6_1_1 true))
174
               (= comparetozero_test.__comparetozero_test_10 1.0))
175
            (or (not (= comparetozero_test.In6_1_1 false))
176
               (= comparetozero_test.__comparetozero_test_10 0.0))
177
       )
178
       (= comparetozero_test.CompareToZero8_1_6 (<= comparetozero_test.__comparetozero_test_2 0.0))
179
       (= comparetozero_test.Out9_9_6 comparetozero_test.CompareToZero8_1_6)
180
       (= comparetozero_test.CompareToZero8_1_5 (<= comparetozero_test.__comparetozero_test_3 0.0))
181
       (= comparetozero_test.Out9_9_5 comparetozero_test.CompareToZero8_1_5)
182
       (= comparetozero_test.CompareToZero8_1_4 (<= comparetozero_test.__comparetozero_test_4 0.0))
183
       (= comparetozero_test.Out9_9_4 comparetozero_test.CompareToZero8_1_4)
184
       (= comparetozero_test.CompareToZero8_1_3 (<= comparetozero_test.__comparetozero_test_5 0.0))
185
       (= comparetozero_test.Out9_9_3 comparetozero_test.CompareToZero8_1_3)
186
       (= comparetozero_test.CompareToZero8_1_2 (<= comparetozero_test.__comparetozero_test_6 0.0))
187
       (= comparetozero_test.Out9_9_2 comparetozero_test.CompareToZero8_1_2)
188
       (= comparetozero_test.CompareToZero8_1_1 (<= comparetozero_test.__comparetozero_test_7 0.0))
189
       (= comparetozero_test.Out9_9_1 comparetozero_test.CompareToZero8_1_1)
190
       (= comparetozero_test.CompareToZero7_1_6 (<= comparetozero_test.In8_1_6 0))
191
       (= comparetozero_test.Out8_8_6 comparetozero_test.CompareToZero7_1_6)
192
       (= comparetozero_test.CompareToZero7_1_5 (<= comparetozero_test.In8_1_5 0))
193
       (= comparetozero_test.Out8_8_5 comparetozero_test.CompareToZero7_1_5)
194
       (= comparetozero_test.CompareToZero7_1_4 (<= comparetozero_test.In8_1_4 0))
195
       (= comparetozero_test.Out8_8_4 comparetozero_test.CompareToZero7_1_4)
196
       (= comparetozero_test.CompareToZero7_1_3 (<= comparetozero_test.In8_1_3 0))
197
       (= comparetozero_test.Out8_8_3 comparetozero_test.CompareToZero7_1_3)
198
       (= comparetozero_test.CompareToZero7_1_2 (<= comparetozero_test.In8_1_2 0))
199
       (= comparetozero_test.Out8_8_2 comparetozero_test.CompareToZero7_1_2)
200
       (= comparetozero_test.CompareToZero7_1_1 (<= comparetozero_test.In8_1_1 0))
201
       (= comparetozero_test.Out8_8_1 comparetozero_test.CompareToZero7_1_1)
202
       (= comparetozero_test.CompareToZero6_1_6 (<= comparetozero_test.In7_1_6 0.00000000))
203
       (= comparetozero_test.Out7_7_6 comparetozero_test.CompareToZero6_1_6)
204
       (= comparetozero_test.CompareToZero6_1_5 (<= comparetozero_test.In7_1_5 0.00000000))
205
       (= comparetozero_test.Out7_7_5 comparetozero_test.CompareToZero6_1_5)
206
       (= comparetozero_test.CompareToZero6_1_4 (<= comparetozero_test.In7_1_4 0.00000000))
207
       (= comparetozero_test.Out7_7_4 comparetozero_test.CompareToZero6_1_4)
208
       (= comparetozero_test.CompareToZero6_1_3 (<= comparetozero_test.In7_1_3 0.00000000))
209
       (= comparetozero_test.Out7_7_3 comparetozero_test.CompareToZero6_1_3)
210
       (= comparetozero_test.CompareToZero6_1_2 (<= comparetozero_test.In7_1_2 0.00000000))
211
       (= comparetozero_test.Out7_7_2 comparetozero_test.CompareToZero6_1_2)
212
       (= comparetozero_test.CompareToZero6_1_1 (<= comparetozero_test.In7_1_1 0.00000000))
213
       (= comparetozero_test.Out7_7_1 comparetozero_test.CompareToZero6_1_1)
214
       (= comparetozero_test.CompareToZero5_1_3 (<= comparetozero_test.__comparetozero_test_8 0.0))
215
       (= comparetozero_test.Out6_6_3 comparetozero_test.CompareToZero5_1_3)
216
       (= comparetozero_test.CompareToZero5_1_2 (<= comparetozero_test.__comparetozero_test_9 0.0))
217
       (= comparetozero_test.Out6_6_2 comparetozero_test.CompareToZero5_1_2)
218
       (= comparetozero_test.CompareToZero5_1_1 (<= comparetozero_test.__comparetozero_test_10 0.0))
219
       (= comparetozero_test.Out6_6_1 comparetozero_test.CompareToZero5_1_1)
220
       (= comparetozero_test.CompareToZero4_1_3 (<= comparetozero_test.In5_1_3 0))
221
       (= comparetozero_test.Out5_5_3 comparetozero_test.CompareToZero4_1_3)
222
       (= comparetozero_test.CompareToZero4_1_2 (<= comparetozero_test.In5_1_2 0))
223
       (= comparetozero_test.Out5_5_2 comparetozero_test.CompareToZero4_1_2)
224
       (= comparetozero_test.CompareToZero4_1_1 (<= comparetozero_test.In5_1_1 0))
225
       (= comparetozero_test.Out5_5_1 comparetozero_test.CompareToZero4_1_1)
226
       (= comparetozero_test.CompareToZero3_1_3 (<= comparetozero_test.In4_1_3 0.00000000))
227
       (= comparetozero_test.Out4_4_3 comparetozero_test.CompareToZero3_1_3)
228
       (= comparetozero_test.CompareToZero3_1_2 (<= comparetozero_test.In4_1_2 0.00000000))
229
       (= comparetozero_test.Out4_4_2 comparetozero_test.CompareToZero3_1_2)
230
       (= comparetozero_test.CompareToZero3_1_1 (<= comparetozero_test.In4_1_1 0.00000000))
231
       (= comparetozero_test.Out4_4_1 comparetozero_test.CompareToZero3_1_1)
232
       (= comparetozero_test.CompareToZero2_1_1 (<= comparetozero_test.__comparetozero_test_11 0.0))
233
       (= comparetozero_test.Out3_3_1 comparetozero_test.CompareToZero2_1_1)
234
       (= comparetozero_test.CompareToZero1_1_1 (<= comparetozero_test.In2_1_1 0))
235
       (= comparetozero_test.Out2_2_1 comparetozero_test.CompareToZero1_1_1)
236
       (= comparetozero_test.CompareToZero_1_1 (<= comparetozero_test.In1_1_1 0.00000000))
237
       (= comparetozero_test.Out1_1_1 comparetozero_test.CompareToZero_1_1)
238
       )
239
  (comparetozero_test_step comparetozero_test.In1_1_1
240
                           comparetozero_test.In2_1_1
241
                           comparetozero_test.In3_1_1
242
                           comparetozero_test.In4_1_1
243
                           comparetozero_test.In4_1_2
244
                           comparetozero_test.In4_1_3
245
                           comparetozero_test.In5_1_1
246
                           comparetozero_test.In5_1_2
247
                           comparetozero_test.In5_1_3
248
                           comparetozero_test.In6_1_1
249
                           comparetozero_test.In6_1_2
250
                           comparetozero_test.In6_1_3
251
                           comparetozero_test.In7_1_1
252
                           comparetozero_test.In7_1_2
253
                           comparetozero_test.In7_1_3
254
                           comparetozero_test.In7_1_4
255
                           comparetozero_test.In7_1_5
256
                           comparetozero_test.In7_1_6
257
                           comparetozero_test.In8_1_1
258
                           comparetozero_test.In8_1_2
259
                           comparetozero_test.In8_1_3
260
                           comparetozero_test.In8_1_4
261
                           comparetozero_test.In8_1_5
262
                           comparetozero_test.In8_1_6
263
                           comparetozero_test.In9_1_1
264
                           comparetozero_test.In9_1_2
265
                           comparetozero_test.In9_1_3
266
                           comparetozero_test.In9_1_4
267
                           comparetozero_test.In9_1_5
268
                           comparetozero_test.In9_1_6
269
                           comparetozero_test.Out1_1_1
270
                           comparetozero_test.Out2_2_1
271
                           comparetozero_test.Out3_3_1
272
                           comparetozero_test.Out4_4_1
273
                           comparetozero_test.Out4_4_2
274
                           comparetozero_test.Out4_4_3
275
                           comparetozero_test.Out5_5_1
276
                           comparetozero_test.Out5_5_2
277
                           comparetozero_test.Out5_5_3
278
                           comparetozero_test.Out6_6_1
279
                           comparetozero_test.Out6_6_2
280
                           comparetozero_test.Out6_6_3
281
                           comparetozero_test.Out7_7_1
282
                           comparetozero_test.Out7_7_2
283
                           comparetozero_test.Out7_7_3
284
                           comparetozero_test.Out7_7_4
285
                           comparetozero_test.Out7_7_5
286
                           comparetozero_test.Out7_7_6
287
                           comparetozero_test.Out8_8_1
288
                           comparetozero_test.Out8_8_2
289
                           comparetozero_test.Out8_8_3
290
                           comparetozero_test.Out8_8_4
291
                           comparetozero_test.Out8_8_5
292
                           comparetozero_test.Out8_8_6
293
                           comparetozero_test.Out9_9_1
294
                           comparetozero_test.Out9_9_2
295
                           comparetozero_test.Out9_9_3
296
                           comparetozero_test.Out9_9_4
297
                           comparetozero_test.Out9_9_5
298
                           comparetozero_test.Out9_9_6
299
                           comparetozero_test.ni_0._arrow._first_c
300
                           comparetozero_test.ni_0._arrow._first_x)
301
))
302