Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_relop_multi_test / relop_multi_test.smt2 @ 6c3ea955

History | View | Annotate | Download (19.3 KB)

1 6c3ea955 bourbouh
; relop_multi_test
2
(declare-var relop_multi_test.In1_1_1 Real)
3
(declare-var relop_multi_test.In1_1_2 Real)
4
(declare-var relop_multi_test.In1_1_3 Real)
5
(declare-var relop_multi_test.In2_1_1 Real)
6
(declare-var relop_multi_test.In2_1_2 Real)
7
(declare-var relop_multi_test.In2_1_3 Real)
8
(declare-var relop_multi_test.In3_1_1 Int)
9
(declare-var relop_multi_test.In3_1_2 Int)
10
(declare-var relop_multi_test.In3_1_3 Int)
11
(declare-var relop_multi_test.In4_1_1 Int)
12
(declare-var relop_multi_test.In5_1_1 Bool)
13
(declare-var relop_multi_test.In6_1_1 Bool)
14
(declare-var relop_multi_test.In6_1_2 Bool)
15
(declare-var relop_multi_test.In6_1_3 Bool)
16
(declare-var relop_multi_test.In19_1_1 Real)
17
(declare-var relop_multi_test.In19_1_2 Real)
18
(declare-var relop_multi_test.In19_1_3 Real)
19
(declare-var relop_multi_test.In19_1_4 Real)
20
(declare-var relop_multi_test.In19_1_5 Real)
21
(declare-var relop_multi_test.In19_1_6 Real)
22
(declare-var relop_multi_test.In20_1_1 Real)
23
(declare-var relop_multi_test.In21_1_1 Int)
24
(declare-var relop_multi_test.In22_1_1 Int)
25
(declare-var relop_multi_test.In22_1_2 Int)
26
(declare-var relop_multi_test.In22_1_3 Int)
27
(declare-var relop_multi_test.In22_1_4 Int)
28
(declare-var relop_multi_test.In22_1_5 Int)
29
(declare-var relop_multi_test.In22_1_6 Int)
30
(declare-var relop_multi_test.In23_1_1 Bool)
31
(declare-var relop_multi_test.In23_1_2 Bool)
32
(declare-var relop_multi_test.In23_1_3 Bool)
33
(declare-var relop_multi_test.In23_1_4 Bool)
34
(declare-var relop_multi_test.In23_1_5 Bool)
35
(declare-var relop_multi_test.In23_1_6 Bool)
36
(declare-var relop_multi_test.In24_1_1 Bool)
37
(declare-var relop_multi_test.In24_1_2 Bool)
38
(declare-var relop_multi_test.In24_1_3 Bool)
39
(declare-var relop_multi_test.In24_1_4 Bool)
40
(declare-var relop_multi_test.In24_1_5 Bool)
41
(declare-var relop_multi_test.In24_1_6 Bool)
42
(declare-var relop_multi_test.Out1_1_1 Bool)
43
(declare-var relop_multi_test.Out1_1_2 Bool)
44
(declare-var relop_multi_test.Out1_1_3 Bool)
45
(declare-var relop_multi_test.Out2_2_1 Bool)
46
(declare-var relop_multi_test.Out2_2_2 Bool)
47
(declare-var relop_multi_test.Out2_2_3 Bool)
48
(declare-var relop_multi_test.Out3_3_1 Bool)
49
(declare-var relop_multi_test.Out3_3_2 Bool)
50
(declare-var relop_multi_test.Out3_3_3 Bool)
51
(declare-var relop_multi_test.Out10_4_1 Bool)
52
(declare-var relop_multi_test.Out10_4_2 Bool)
53
(declare-var relop_multi_test.Out10_4_3 Bool)
54
(declare-var relop_multi_test.Out10_4_4 Bool)
55
(declare-var relop_multi_test.Out10_4_5 Bool)
56
(declare-var relop_multi_test.Out10_4_6 Bool)
57
(declare-var relop_multi_test.Out11_5_1 Bool)
58
(declare-var relop_multi_test.Out11_5_2 Bool)
59
(declare-var relop_multi_test.Out11_5_3 Bool)
60
(declare-var relop_multi_test.Out11_5_4 Bool)
61
(declare-var relop_multi_test.Out11_5_5 Bool)
62
(declare-var relop_multi_test.Out11_5_6 Bool)
63
(declare-var relop_multi_test.Out12_6_1 Bool)
64
(declare-var relop_multi_test.Out12_6_2 Bool)
65
(declare-var relop_multi_test.Out12_6_3 Bool)
66
(declare-var relop_multi_test.Out12_6_4 Bool)
67
(declare-var relop_multi_test.Out12_6_5 Bool)
68
(declare-var relop_multi_test.Out12_6_6 Bool)
69
(declare-var relop_multi_test.ni_0._arrow._first_c Bool)
70
(declare-var relop_multi_test.ni_0._arrow._first_m Bool)
71
(declare-var relop_multi_test.ni_0._arrow._first_x Bool)
72
(declare-var relop_multi_test.RelationalOperator10_1_1 Bool)
73
(declare-var relop_multi_test.RelationalOperator10_1_2 Bool)
74
(declare-var relop_multi_test.RelationalOperator10_1_3 Bool)
75
(declare-var relop_multi_test.RelationalOperator10_1_4 Bool)
76
(declare-var relop_multi_test.RelationalOperator10_1_5 Bool)
77
(declare-var relop_multi_test.RelationalOperator10_1_6 Bool)
78
(declare-var relop_multi_test.RelationalOperator11_1_1 Bool)
79
(declare-var relop_multi_test.RelationalOperator11_1_2 Bool)
80
(declare-var relop_multi_test.RelationalOperator11_1_3 Bool)
81
(declare-var relop_multi_test.RelationalOperator11_1_4 Bool)
82
(declare-var relop_multi_test.RelationalOperator11_1_5 Bool)
83
(declare-var relop_multi_test.RelationalOperator11_1_6 Bool)
84
(declare-var relop_multi_test.RelationalOperator1_1_1 Bool)
85
(declare-var relop_multi_test.RelationalOperator1_1_2 Bool)
86
(declare-var relop_multi_test.RelationalOperator1_1_3 Bool)
87
(declare-var relop_multi_test.RelationalOperator2_1_1 Bool)
88
(declare-var relop_multi_test.RelationalOperator2_1_2 Bool)
89
(declare-var relop_multi_test.RelationalOperator2_1_3 Bool)
90
(declare-var relop_multi_test.RelationalOperator9_1_1 Bool)
91
(declare-var relop_multi_test.RelationalOperator9_1_2 Bool)
92
(declare-var relop_multi_test.RelationalOperator9_1_3 Bool)
93
(declare-var relop_multi_test.RelationalOperator9_1_4 Bool)
94
(declare-var relop_multi_test.RelationalOperator9_1_5 Bool)
95
(declare-var relop_multi_test.RelationalOperator9_1_6 Bool)
96
(declare-var relop_multi_test.RelationalOperator_1_1 Bool)
97
(declare-var relop_multi_test.RelationalOperator_1_2 Bool)
98
(declare-var relop_multi_test.RelationalOperator_1_3 Bool)
99
(declare-var relop_multi_test.__relop_multi_test_1 Bool)
100
(declare-var relop_multi_test.__relop_multi_test_10 Int)
101
(declare-var relop_multi_test.__relop_multi_test_11 Int)
102
(declare-var relop_multi_test.__relop_multi_test_12 Int)
103
(declare-var relop_multi_test.__relop_multi_test_13 Int)
104
(declare-var relop_multi_test.__relop_multi_test_14 Int)
105
(declare-var relop_multi_test.__relop_multi_test_15 Int)
106
(declare-var relop_multi_test.__relop_multi_test_16 Int)
107
(declare-var relop_multi_test.__relop_multi_test_17 Int)
108
(declare-var relop_multi_test.__relop_multi_test_2 Int)
109
(declare-var relop_multi_test.__relop_multi_test_3 Int)
110
(declare-var relop_multi_test.__relop_multi_test_4 Int)
111
(declare-var relop_multi_test.__relop_multi_test_5 Int)
112
(declare-var relop_multi_test.__relop_multi_test_6 Int)
113
(declare-var relop_multi_test.__relop_multi_test_7 Int)
114
(declare-var relop_multi_test.__relop_multi_test_8 Int)
115
(declare-var relop_multi_test.__relop_multi_test_9 Int)
116
(declare-var relop_multi_test.i_virtual_local Real)
117
(declare-rel relop_multi_test_reset (Bool Bool))
118
(declare-rel relop_multi_test_step (Real Real Real Real Real Real Int Int Int Int Bool Bool Bool Bool Real Real Real Real Real Real Real Int 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 Bool Bool Bool))
119
120
(rule (=> 
121
  (and 
122
       
123
       (= relop_multi_test.ni_0._arrow._first_m true)
124
  )
125
  (relop_multi_test_reset relop_multi_test.ni_0._arrow._first_c
126
                          relop_multi_test.ni_0._arrow._first_m)
127
))
128
129
(rule (=> 
130
  (and (= relop_multi_test.ni_0._arrow._first_m relop_multi_test.ni_0._arrow._first_c)
131
       (and (= relop_multi_test.__relop_multi_test_1 (ite relop_multi_test.ni_0._arrow._first_m true false))
132
            (= relop_multi_test.ni_0._arrow._first_x false))
133
       (and (or (not (= relop_multi_test.__relop_multi_test_1 true))
134
               (= relop_multi_test.i_virtual_local 0.0))
135
            (or (not (= relop_multi_test.__relop_multi_test_1 false))
136
               (= relop_multi_test.i_virtual_local 1.0))
137
       )
138
       (and (or (not (= relop_multi_test.In23_1_5 true))
139
               (= relop_multi_test.__relop_multi_test_9 1))
140
            (or (not (= relop_multi_test.In23_1_5 false))
141
               (= relop_multi_test.__relop_multi_test_9 0))
142
       )
143
       (and (or (not (= relop_multi_test.In24_1_5 true))
144
               (= relop_multi_test.__relop_multi_test_8 1))
145
            (or (not (= relop_multi_test.In24_1_5 false))
146
               (= relop_multi_test.__relop_multi_test_8 0))
147
       )
148
       (and (or (not (= relop_multi_test.In23_1_6 true))
149
               (= relop_multi_test.__relop_multi_test_7 1))
150
            (or (not (= relop_multi_test.In23_1_6 false))
151
               (= relop_multi_test.__relop_multi_test_7 0))
152
       )
153
       (and (or (not (= relop_multi_test.In24_1_6 true))
154
               (= relop_multi_test.__relop_multi_test_6 1))
155
            (or (not (= relop_multi_test.In24_1_6 false))
156
               (= relop_multi_test.__relop_multi_test_6 0))
157
       )
158
       (and (or (not (= relop_multi_test.In6_1_1 true))
159
               (= relop_multi_test.__relop_multi_test_5 1))
160
            (or (not (= relop_multi_test.In6_1_1 false))
161
               (= relop_multi_test.__relop_multi_test_5 0))
162
       )
163
       (and (or (not (= relop_multi_test.In6_1_2 true))
164
               (= relop_multi_test.__relop_multi_test_4 1))
165
            (or (not (= relop_multi_test.In6_1_2 false))
166
               (= relop_multi_test.__relop_multi_test_4 0))
167
       )
168
       (and (or (not (= relop_multi_test.In5_1_1 true))
169
               (= relop_multi_test.__relop_multi_test_3 1))
170
            (or (not (= relop_multi_test.In5_1_1 false))
171
               (= relop_multi_test.__relop_multi_test_3 0))
172
       )
173
       (and (or (not (= relop_multi_test.In6_1_3 true))
174
               (= relop_multi_test.__relop_multi_test_2 1))
175
            (or (not (= relop_multi_test.In6_1_3 false))
176
               (= relop_multi_test.__relop_multi_test_2 0))
177
       )
178
       (and (or (not (= relop_multi_test.In23_1_1 true))
179
               (= relop_multi_test.__relop_multi_test_17 1))
180
            (or (not (= relop_multi_test.In23_1_1 false))
181
               (= relop_multi_test.__relop_multi_test_17 0))
182
       )
183
       (and (or (not (= relop_multi_test.In24_1_1 true))
184
               (= relop_multi_test.__relop_multi_test_16 1))
185
            (or (not (= relop_multi_test.In24_1_1 false))
186
               (= relop_multi_test.__relop_multi_test_16 0))
187
       )
188
       (and (or (not (= relop_multi_test.In23_1_2 true))
189
               (= relop_multi_test.__relop_multi_test_15 1))
190
            (or (not (= relop_multi_test.In23_1_2 false))
191
               (= relop_multi_test.__relop_multi_test_15 0))
192
       )
193
       (and (or (not (= relop_multi_test.In24_1_2 true))
194
               (= relop_multi_test.__relop_multi_test_14 1))
195
            (or (not (= relop_multi_test.In24_1_2 false))
196
               (= relop_multi_test.__relop_multi_test_14 0))
197
       )
198
       (and (or (not (= relop_multi_test.In23_1_3 true))
199
               (= relop_multi_test.__relop_multi_test_13 1))
200
            (or (not (= relop_multi_test.In23_1_3 false))
201
               (= relop_multi_test.__relop_multi_test_13 0))
202
       )
203
       (and (or (not (= relop_multi_test.In24_1_3 true))
204
               (= relop_multi_test.__relop_multi_test_12 1))
205
            (or (not (= relop_multi_test.In24_1_3 false))
206
               (= relop_multi_test.__relop_multi_test_12 0))
207
       )
208
       (and (or (not (= relop_multi_test.In23_1_4 true))
209
               (= relop_multi_test.__relop_multi_test_11 1))
210
            (or (not (= relop_multi_test.In23_1_4 false))
211
               (= relop_multi_test.__relop_multi_test_11 0))
212
       )
213
       (and (or (not (= relop_multi_test.In24_1_4 true))
214
               (= relop_multi_test.__relop_multi_test_10 1))
215
            (or (not (= relop_multi_test.In24_1_4 false))
216
               (= relop_multi_test.__relop_multi_test_10 0))
217
       )
218
       (= relop_multi_test.RelationalOperator_1_3 (<= relop_multi_test.In1_1_3 relop_multi_test.In2_1_3))
219
       (= relop_multi_test.RelationalOperator_1_2 (<= relop_multi_test.In1_1_2 relop_multi_test.In2_1_2))
220
       (= relop_multi_test.RelationalOperator_1_1 (<= relop_multi_test.In1_1_1 relop_multi_test.In2_1_1))
221
       (= relop_multi_test.RelationalOperator9_1_6 (< relop_multi_test.In19_1_6 relop_multi_test.In20_1_1))
222
       (= relop_multi_test.RelationalOperator9_1_5 (< relop_multi_test.In19_1_5 relop_multi_test.In20_1_1))
223
       (= relop_multi_test.RelationalOperator9_1_4 (< relop_multi_test.In19_1_4 relop_multi_test.In20_1_1))
224
       (= relop_multi_test.RelationalOperator9_1_3 (< relop_multi_test.In19_1_3 relop_multi_test.In20_1_1))
225
       (= relop_multi_test.RelationalOperator9_1_2 (< relop_multi_test.In19_1_2 relop_multi_test.In20_1_1))
226
       (= relop_multi_test.RelationalOperator9_1_1 (< relop_multi_test.In19_1_1 relop_multi_test.In20_1_1))
227
       (= relop_multi_test.RelationalOperator2_1_3 (<= relop_multi_test.__relop_multi_test_3 relop_multi_test.__relop_multi_test_2))
228
       (= relop_multi_test.RelationalOperator2_1_2 (<= relop_multi_test.__relop_multi_test_3 relop_multi_test.__relop_multi_test_4))
229
       (= relop_multi_test.RelationalOperator2_1_1 (<= relop_multi_test.__relop_multi_test_3 relop_multi_test.__relop_multi_test_5))
230
       (= relop_multi_test.RelationalOperator1_1_3 (<= relop_multi_test.In3_1_3 relop_multi_test.In4_1_1))
231
       (= relop_multi_test.RelationalOperator1_1_2 (<= relop_multi_test.In3_1_2 relop_multi_test.In4_1_1))
232
       (= relop_multi_test.RelationalOperator1_1_1 (<= relop_multi_test.In3_1_1 relop_multi_test.In4_1_1))
233
       (= relop_multi_test.RelationalOperator11_1_6 (< relop_multi_test.__relop_multi_test_7 relop_multi_test.__relop_multi_test_6))
234
       (= relop_multi_test.RelationalOperator11_1_5 (< relop_multi_test.__relop_multi_test_9 relop_multi_test.__relop_multi_test_8))
235
       (= relop_multi_test.RelationalOperator11_1_4 (< relop_multi_test.__relop_multi_test_11 relop_multi_test.__relop_multi_test_10))
236
       (= relop_multi_test.RelationalOperator11_1_3 (< relop_multi_test.__relop_multi_test_13 relop_multi_test.__relop_multi_test_12))
237
       (= relop_multi_test.RelationalOperator11_1_2 (< relop_multi_test.__relop_multi_test_15 relop_multi_test.__relop_multi_test_14))
238
       (= relop_multi_test.RelationalOperator11_1_1 (< relop_multi_test.__relop_multi_test_17 relop_multi_test.__relop_multi_test_16))
239
       (= relop_multi_test.RelationalOperator10_1_6 (< relop_multi_test.In21_1_1 relop_multi_test.In22_1_6))
240
       (= relop_multi_test.RelationalOperator10_1_5 (< relop_multi_test.In21_1_1 relop_multi_test.In22_1_5))
241
       (= relop_multi_test.RelationalOperator10_1_4 (< relop_multi_test.In21_1_1 relop_multi_test.In22_1_4))
242
       (= relop_multi_test.RelationalOperator10_1_3 (< relop_multi_test.In21_1_1 relop_multi_test.In22_1_3))
243
       (= relop_multi_test.RelationalOperator10_1_2 (< relop_multi_test.In21_1_1 relop_multi_test.In22_1_2))
244
       (= relop_multi_test.RelationalOperator10_1_1 (< relop_multi_test.In21_1_1 relop_multi_test.In22_1_1))
245
       (= relop_multi_test.Out3_3_3 relop_multi_test.RelationalOperator2_1_3)
246
       (= relop_multi_test.Out3_3_2 relop_multi_test.RelationalOperator2_1_2)
247
       (= relop_multi_test.Out3_3_1 relop_multi_test.RelationalOperator2_1_1)
248
       (= relop_multi_test.Out2_2_3 relop_multi_test.RelationalOperator1_1_3)
249
       (= relop_multi_test.Out2_2_2 relop_multi_test.RelationalOperator1_1_2)
250
       (= relop_multi_test.Out2_2_1 relop_multi_test.RelationalOperator1_1_1)
251
       (= relop_multi_test.Out1_1_3 relop_multi_test.RelationalOperator_1_3)
252
       (= relop_multi_test.Out1_1_2 relop_multi_test.RelationalOperator_1_2)
253
       (= relop_multi_test.Out1_1_1 relop_multi_test.RelationalOperator_1_1)
254
       (= relop_multi_test.Out12_6_6 relop_multi_test.RelationalOperator11_1_6)
255
       (= relop_multi_test.Out12_6_5 relop_multi_test.RelationalOperator11_1_5)
256
       (= relop_multi_test.Out12_6_4 relop_multi_test.RelationalOperator11_1_4)
257
       (= relop_multi_test.Out12_6_3 relop_multi_test.RelationalOperator11_1_3)
258
       (= relop_multi_test.Out12_6_2 relop_multi_test.RelationalOperator11_1_2)
259
       (= relop_multi_test.Out12_6_1 relop_multi_test.RelationalOperator11_1_1)
260
       (= relop_multi_test.Out11_5_6 relop_multi_test.RelationalOperator10_1_6)
261
       (= relop_multi_test.Out11_5_5 relop_multi_test.RelationalOperator10_1_5)
262
       (= relop_multi_test.Out11_5_4 relop_multi_test.RelationalOperator10_1_4)
263
       (= relop_multi_test.Out11_5_3 relop_multi_test.RelationalOperator10_1_3)
264
       (= relop_multi_test.Out11_5_2 relop_multi_test.RelationalOperator10_1_2)
265
       (= relop_multi_test.Out11_5_1 relop_multi_test.RelationalOperator10_1_1)
266
       (= relop_multi_test.Out10_4_6 relop_multi_test.RelationalOperator9_1_6)
267
       (= relop_multi_test.Out10_4_5 relop_multi_test.RelationalOperator9_1_5)
268
       (= relop_multi_test.Out10_4_4 relop_multi_test.RelationalOperator9_1_4)
269
       (= relop_multi_test.Out10_4_3 relop_multi_test.RelationalOperator9_1_3)
270
       (= relop_multi_test.Out10_4_2 relop_multi_test.RelationalOperator9_1_2)
271
       (= relop_multi_test.Out10_4_1 relop_multi_test.RelationalOperator9_1_1)
272
       )
273
  (relop_multi_test_step relop_multi_test.In1_1_1
274
                         relop_multi_test.In1_1_2
275
                         relop_multi_test.In1_1_3
276
                         relop_multi_test.In2_1_1
277
                         relop_multi_test.In2_1_2
278
                         relop_multi_test.In2_1_3
279
                         relop_multi_test.In3_1_1
280
                         relop_multi_test.In3_1_2
281
                         relop_multi_test.In3_1_3
282
                         relop_multi_test.In4_1_1
283
                         relop_multi_test.In5_1_1
284
                         relop_multi_test.In6_1_1
285
                         relop_multi_test.In6_1_2
286
                         relop_multi_test.In6_1_3
287
                         relop_multi_test.In19_1_1
288
                         relop_multi_test.In19_1_2
289
                         relop_multi_test.In19_1_3
290
                         relop_multi_test.In19_1_4
291
                         relop_multi_test.In19_1_5
292
                         relop_multi_test.In19_1_6
293
                         relop_multi_test.In20_1_1
294
                         relop_multi_test.In21_1_1
295
                         relop_multi_test.In22_1_1
296
                         relop_multi_test.In22_1_2
297
                         relop_multi_test.In22_1_3
298
                         relop_multi_test.In22_1_4
299
                         relop_multi_test.In22_1_5
300
                         relop_multi_test.In22_1_6
301
                         relop_multi_test.In23_1_1
302
                         relop_multi_test.In23_1_2
303
                         relop_multi_test.In23_1_3
304
                         relop_multi_test.In23_1_4
305
                         relop_multi_test.In23_1_5
306
                         relop_multi_test.In23_1_6
307
                         relop_multi_test.In24_1_1
308
                         relop_multi_test.In24_1_2
309
                         relop_multi_test.In24_1_3
310
                         relop_multi_test.In24_1_4
311
                         relop_multi_test.In24_1_5
312
                         relop_multi_test.In24_1_6
313
                         relop_multi_test.Out1_1_1
314
                         relop_multi_test.Out1_1_2
315
                         relop_multi_test.Out1_1_3
316
                         relop_multi_test.Out2_2_1
317
                         relop_multi_test.Out2_2_2
318
                         relop_multi_test.Out2_2_3
319
                         relop_multi_test.Out3_3_1
320
                         relop_multi_test.Out3_3_2
321
                         relop_multi_test.Out3_3_3
322
                         relop_multi_test.Out10_4_1
323
                         relop_multi_test.Out10_4_2
324
                         relop_multi_test.Out10_4_3
325
                         relop_multi_test.Out10_4_4
326
                         relop_multi_test.Out10_4_5
327
                         relop_multi_test.Out10_4_6
328
                         relop_multi_test.Out11_5_1
329
                         relop_multi_test.Out11_5_2
330
                         relop_multi_test.Out11_5_3
331
                         relop_multi_test.Out11_5_4
332
                         relop_multi_test.Out11_5_5
333
                         relop_multi_test.Out11_5_6
334
                         relop_multi_test.Out12_6_1
335
                         relop_multi_test.Out12_6_2
336
                         relop_multi_test.Out12_6_3
337
                         relop_multi_test.Out12_6_4
338
                         relop_multi_test.Out12_6_5
339
                         relop_multi_test.Out12_6_6
340
                         relop_multi_test.ni_0._arrow._first_c
341
                         relop_multi_test.ni_0._arrow._first_x)
342
))