Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_assignment_test / assignment_test.smt2 @ 6c3ea955

History | View | Annotate | Download (16 KB)

1
; assignment_test
2
(declare-var assignment_test.In1_1_1 Real)
3
(declare-var assignment_test.In1_1_2 Real)
4
(declare-var assignment_test.In1_1_3 Real)
5
(declare-var assignment_test.In1_1_4 Real)
6
(declare-var assignment_test.In1_1_5 Real)
7
(declare-var assignment_test.In1_1_6 Real)
8
(declare-var assignment_test.In2_1_1 Bool)
9
(declare-var assignment_test.In2_1_2 Bool)
10
(declare-var assignment_test.In2_1_3 Bool)
11
(declare-var assignment_test.In2_1_4 Bool)
12
(declare-var assignment_test.In2_1_5 Bool)
13
(declare-var assignment_test.In2_1_6 Bool)
14
(declare-var assignment_test.In3_1_1 Int)
15
(declare-var assignment_test.In3_1_2 Int)
16
(declare-var assignment_test.In3_1_3 Int)
17
(declare-var assignment_test.In3_1_4 Int)
18
(declare-var assignment_test.In3_1_5 Int)
19
(declare-var assignment_test.In3_1_6 Int)
20
(declare-var assignment_test.In4_1_1 Real)
21
(declare-var assignment_test.In4_1_2 Real)
22
(declare-var assignment_test.In4_1_3 Real)
23
(declare-var assignment_test.In5_1_1 Bool)
24
(declare-var assignment_test.In5_1_2 Bool)
25
(declare-var assignment_test.In5_1_3 Bool)
26
(declare-var assignment_test.In6_1_1 Int)
27
(declare-var assignment_test.In6_1_2 Int)
28
(declare-var assignment_test.In6_1_3 Int)
29
(declare-var assignment_test.In7_1_1 Int)
30
(declare-var assignment_test.In7_1_2 Int)
31
(declare-var assignment_test.In7_1_3 Int)
32
(declare-var assignment_test.In8_1_1 Int)
33
(declare-var assignment_test.In8_1_2 Int)
34
(declare-var assignment_test.In8_1_3 Int)
35
(declare-var assignment_test.In8_1_4 Int)
36
(declare-var assignment_test.In8_1_5 Int)
37
(declare-var assignment_test.In8_1_6 Int)
38
(declare-var assignment_test.Out1_1_1 Real)
39
(declare-var assignment_test.Out1_1_2 Real)
40
(declare-var assignment_test.Out1_1_3 Real)
41
(declare-var assignment_test.Out1_1_4 Real)
42
(declare-var assignment_test.Out1_1_5 Real)
43
(declare-var assignment_test.Out1_1_6 Real)
44
(declare-var assignment_test.Out2_2_1 Bool)
45
(declare-var assignment_test.Out2_2_2 Bool)
46
(declare-var assignment_test.Out2_2_3 Bool)
47
(declare-var assignment_test.Out2_2_4 Bool)
48
(declare-var assignment_test.Out2_2_5 Bool)
49
(declare-var assignment_test.Out2_2_6 Bool)
50
(declare-var assignment_test.Out3_3_1 Int)
51
(declare-var assignment_test.Out3_3_2 Int)
52
(declare-var assignment_test.Out3_3_3 Int)
53
(declare-var assignment_test.Out3_3_4 Int)
54
(declare-var assignment_test.Out3_3_5 Int)
55
(declare-var assignment_test.Out3_3_6 Int)
56
(declare-var assignment_test.Out4_4_1 Real)
57
(declare-var assignment_test.Out4_4_2 Real)
58
(declare-var assignment_test.Out4_4_3 Real)
59
(declare-var assignment_test.Out5_5_1 Bool)
60
(declare-var assignment_test.Out5_5_2 Bool)
61
(declare-var assignment_test.Out5_5_3 Bool)
62
(declare-var assignment_test.Out6_6_1 Int)
63
(declare-var assignment_test.Out6_6_2 Int)
64
(declare-var assignment_test.Out6_6_3 Int)
65
(declare-var assignment_test.Out7_7_1 Int)
66
(declare-var assignment_test.Out7_7_2 Int)
67
(declare-var assignment_test.Out7_7_3 Int)
68
(declare-var assignment_test.Out8_8_1 Int)
69
(declare-var assignment_test.Out8_8_2 Int)
70
(declare-var assignment_test.Out8_8_3 Int)
71
(declare-var assignment_test.Out8_8_4 Int)
72
(declare-var assignment_test.Out8_8_5 Int)
73
(declare-var assignment_test.Out8_8_6 Int)
74
(declare-var assignment_test.ni_0._arrow._first_c Bool)
75
(declare-var assignment_test.ni_0._arrow._first_m Bool)
76
(declare-var assignment_test.ni_0._arrow._first_x Bool)
77
(declare-var assignment_test.Assignment1_1_1 Bool)
78
(declare-var assignment_test.Assignment1_1_2 Bool)
79
(declare-var assignment_test.Assignment1_1_3 Bool)
80
(declare-var assignment_test.Assignment1_1_4 Bool)
81
(declare-var assignment_test.Assignment1_1_5 Bool)
82
(declare-var assignment_test.Assignment1_1_6 Bool)
83
(declare-var assignment_test.Assignment2_1_1 Int)
84
(declare-var assignment_test.Assignment2_1_2 Int)
85
(declare-var assignment_test.Assignment2_1_3 Int)
86
(declare-var assignment_test.Assignment2_1_4 Int)
87
(declare-var assignment_test.Assignment2_1_5 Int)
88
(declare-var assignment_test.Assignment2_1_6 Int)
89
(declare-var assignment_test.Assignment3_1_1 Real)
90
(declare-var assignment_test.Assignment3_1_2 Real)
91
(declare-var assignment_test.Assignment3_1_3 Real)
92
(declare-var assignment_test.Assignment4_1_1 Bool)
93
(declare-var assignment_test.Assignment4_1_2 Bool)
94
(declare-var assignment_test.Assignment4_1_3 Bool)
95
(declare-var assignment_test.Assignment5_1_1 Int)
96
(declare-var assignment_test.Assignment5_1_2 Int)
97
(declare-var assignment_test.Assignment5_1_3 Int)
98
(declare-var assignment_test.Assignment6_1_1 Int)
99
(declare-var assignment_test.Assignment6_1_2 Int)
100
(declare-var assignment_test.Assignment6_1_3 Int)
101
(declare-var assignment_test.Assignment7_1_1 Int)
102
(declare-var assignment_test.Assignment7_1_2 Int)
103
(declare-var assignment_test.Assignment7_1_3 Int)
104
(declare-var assignment_test.Assignment7_1_4 Int)
105
(declare-var assignment_test.Assignment7_1_5 Int)
106
(declare-var assignment_test.Assignment7_1_6 Int)
107
(declare-var assignment_test.Assignment_1_1 Real)
108
(declare-var assignment_test.Assignment_1_2 Real)
109
(declare-var assignment_test.Assignment_1_3 Real)
110
(declare-var assignment_test.Assignment_1_4 Real)
111
(declare-var assignment_test.Assignment_1_5 Real)
112
(declare-var assignment_test.Assignment_1_6 Real)
113
(declare-var assignment_test.Constant1_1_1 Real)
114
(declare-var assignment_test.Constant2_1_1 Real)
115
(declare-var assignment_test.Constant3_1_1 Bool)
116
(declare-var assignment_test.Constant4_1_1 Bool)
117
(declare-var assignment_test.Constant5_1_1 Int)
118
(declare-var assignment_test.Constant6_1_1 Int)
119
(declare-var assignment_test.Constant7_1_1 Int)
120
(declare-var assignment_test.Constant7_1_2 Int)
121
(declare-var assignment_test.Constant7_1_3 Int)
122
(declare-var assignment_test.Constant8_1_1 Int)
123
(declare-var assignment_test.Constant8_1_2 Int)
124
(declare-var assignment_test.Constant8_1_3 Int)
125
(declare-var assignment_test.Constant8_1_4 Int)
126
(declare-var assignment_test.Constant8_1_5 Int)
127
(declare-var assignment_test.Constant8_1_6 Int)
128
(declare-var assignment_test.__assignment_test_1 Bool)
129
(declare-var assignment_test.i_virtual_local Real)
130
(declare-rel assignment_test_reset (Bool Bool))
131
(declare-rel assignment_test_step (Real Real Real Real Real Real Bool Bool Bool Bool Bool Bool Int Int Int Int Int Int Real Real Real Bool Bool Bool Int Int Int Int Int Int Int Int Int Int Int Int Real Real Real Real Real Real Bool Bool Bool Bool Bool Bool Int Int Int Int Int Int Real Real Real Bool Bool Bool Int Int Int Int Int Int Int Int Int Int Int Int Bool Bool))
132

    
133
(rule (=> 
134
  (and 
135
       
136
       (= assignment_test.ni_0._arrow._first_m true)
137
  )
138
  (assignment_test_reset assignment_test.ni_0._arrow._first_c
139
                         assignment_test.ni_0._arrow._first_m)
140
))
141

    
142
(rule (=> 
143
  (and (= assignment_test.ni_0._arrow._first_m assignment_test.ni_0._arrow._first_c)
144
       (and (= assignment_test.__assignment_test_1 (ite assignment_test.ni_0._arrow._first_m true false))
145
            (= assignment_test.ni_0._arrow._first_x false))
146
       (and (or (not (= assignment_test.__assignment_test_1 true))
147
               (= assignment_test.i_virtual_local 0.0))
148
            (or (not (= assignment_test.__assignment_test_1 false))
149
               (= assignment_test.i_virtual_local 1.0))
150
       )
151
       (= assignment_test.Constant8_1_6 7)
152
       (= assignment_test.Assignment7_1_6 assignment_test.Constant8_1_6)
153
       (= assignment_test.Out8_8_6 assignment_test.Assignment7_1_6)
154
       (= assignment_test.Constant8_1_5 6)
155
       (= assignment_test.Assignment7_1_5 assignment_test.Constant8_1_5)
156
       (= assignment_test.Out8_8_5 assignment_test.Assignment7_1_5)
157
       (= assignment_test.Constant8_1_4 5)
158
       (= assignment_test.Assignment7_1_4 assignment_test.Constant8_1_4)
159
       (= assignment_test.Out8_8_4 assignment_test.Assignment7_1_4)
160
       (= assignment_test.Constant8_1_3 4)
161
       (= assignment_test.Assignment7_1_3 assignment_test.Constant8_1_3)
162
       (= assignment_test.Out8_8_3 assignment_test.Assignment7_1_3)
163
       (= assignment_test.Constant8_1_2 3)
164
       (= assignment_test.Assignment7_1_2 assignment_test.Constant8_1_2)
165
       (= assignment_test.Out8_8_2 assignment_test.Assignment7_1_2)
166
       (= assignment_test.Constant8_1_1 2)
167
       (= assignment_test.Assignment7_1_1 assignment_test.Constant8_1_1)
168
       (= assignment_test.Out8_8_1 assignment_test.Assignment7_1_1)
169
       (= assignment_test.Constant7_1_3 4)
170
       (= assignment_test.Assignment6_1_3 assignment_test.Constant7_1_3)
171
       (= assignment_test.Out7_7_3 assignment_test.Assignment6_1_3)
172
       (= assignment_test.Constant7_1_2 3)
173
       (= assignment_test.Assignment6_1_2 assignment_test.Constant7_1_2)
174
       (= assignment_test.Out7_7_2 assignment_test.Assignment6_1_2)
175
       (= assignment_test.Constant7_1_1 2)
176
       (= assignment_test.Assignment6_1_1 assignment_test.Constant7_1_1)
177
       (= assignment_test.Out7_7_1 assignment_test.Assignment6_1_1)
178
       (= assignment_test.Assignment5_1_3 assignment_test.In6_1_3)
179
       (= assignment_test.Out6_6_3 assignment_test.Assignment5_1_3)
180
       (= assignment_test.Assignment5_1_2 assignment_test.In6_1_2)
181
       (= assignment_test.Out6_6_2 assignment_test.Assignment5_1_2)
182
       (= assignment_test.Constant6_1_1 12)
183
       (= assignment_test.Assignment5_1_1 assignment_test.Constant6_1_1)
184
       (= assignment_test.Out6_6_1 assignment_test.Assignment5_1_1)
185
       (= assignment_test.Constant4_1_1 true)
186
       (= assignment_test.Assignment4_1_3 assignment_test.Constant4_1_1)
187
       (= assignment_test.Out5_5_3 assignment_test.Assignment4_1_3)
188
       (= assignment_test.Assignment4_1_2 assignment_test.In5_1_2)
189
       (= assignment_test.Out5_5_2 assignment_test.Assignment4_1_2)
190
       (= assignment_test.Assignment4_1_1 assignment_test.In5_1_1)
191
       (= assignment_test.Out5_5_1 assignment_test.Assignment4_1_1)
192
       (= assignment_test.Assignment3_1_3 assignment_test.In4_1_3)
193
       (= assignment_test.Out4_4_3 assignment_test.Assignment3_1_3)
194
       (= assignment_test.Constant2_1_1 12.00000000)
195
       (= assignment_test.Assignment3_1_2 assignment_test.Constant2_1_1)
196
       (= assignment_test.Out4_4_2 assignment_test.Assignment3_1_2)
197
       (= assignment_test.Assignment3_1_1 assignment_test.Constant2_1_1)
198
       (= assignment_test.Out4_4_1 assignment_test.Assignment3_1_1)
199
       (= assignment_test.Assignment2_1_6 assignment_test.In3_1_6)
200
       (= assignment_test.Out3_3_6 assignment_test.Assignment2_1_6)
201
       (= assignment_test.Constant5_1_1 12)
202
       (= assignment_test.Assignment2_1_5 assignment_test.Constant5_1_1)
203
       (= assignment_test.Out3_3_5 assignment_test.Assignment2_1_5)
204
       (= assignment_test.Assignment2_1_4 assignment_test.In3_1_4)
205
       (= assignment_test.Out3_3_4 assignment_test.Assignment2_1_4)
206
       (= assignment_test.Assignment2_1_3 assignment_test.In3_1_3)
207
       (= assignment_test.Out3_3_3 assignment_test.Assignment2_1_3)
208
       (= assignment_test.Assignment2_1_2 assignment_test.Constant5_1_1)
209
       (= assignment_test.Out3_3_2 assignment_test.Assignment2_1_2)
210
       (= assignment_test.Assignment2_1_1 assignment_test.In3_1_1)
211
       (= assignment_test.Out3_3_1 assignment_test.Assignment2_1_1)
212
       (= assignment_test.Assignment1_1_6 assignment_test.In2_1_6)
213
       (= assignment_test.Out2_2_6 assignment_test.Assignment1_1_6)
214
       (= assignment_test.Constant3_1_1 true)
215
       (= assignment_test.Assignment1_1_5 assignment_test.Constant3_1_1)
216
       (= assignment_test.Out2_2_5 assignment_test.Assignment1_1_5)
217
       (= assignment_test.Assignment1_1_4 assignment_test.In2_1_4)
218
       (= assignment_test.Out2_2_4 assignment_test.Assignment1_1_4)
219
       (= assignment_test.Assignment1_1_3 assignment_test.In2_1_3)
220
       (= assignment_test.Out2_2_3 assignment_test.Assignment1_1_3)
221
       (= assignment_test.Assignment1_1_2 assignment_test.Constant3_1_1)
222
       (= assignment_test.Out2_2_2 assignment_test.Assignment1_1_2)
223
       (= assignment_test.Assignment1_1_1 assignment_test.In2_1_1)
224
       (= assignment_test.Out2_2_1 assignment_test.Assignment1_1_1)
225
       (= assignment_test.Assignment_1_6 assignment_test.In1_1_6)
226
       (= assignment_test.Out1_1_6 assignment_test.Assignment_1_6)
227
       (= assignment_test.Constant1_1_1 12.00000000)
228
       (= assignment_test.Assignment_1_5 assignment_test.Constant1_1_1)
229
       (= assignment_test.Out1_1_5 assignment_test.Assignment_1_5)
230
       (= assignment_test.Assignment_1_4 assignment_test.In1_1_4)
231
       (= assignment_test.Out1_1_4 assignment_test.Assignment_1_4)
232
       (= assignment_test.Assignment_1_3 assignment_test.In1_1_3)
233
       (= assignment_test.Out1_1_3 assignment_test.Assignment_1_3)
234
       (= assignment_test.Assignment_1_2 assignment_test.Constant1_1_1)
235
       (= assignment_test.Out1_1_2 assignment_test.Assignment_1_2)
236
       (= assignment_test.Assignment_1_1 assignment_test.In1_1_1)
237
       (= assignment_test.Out1_1_1 assignment_test.Assignment_1_1)
238
       )
239
  (assignment_test_step assignment_test.In1_1_1
240
                        assignment_test.In1_1_2
241
                        assignment_test.In1_1_3
242
                        assignment_test.In1_1_4
243
                        assignment_test.In1_1_5
244
                        assignment_test.In1_1_6
245
                        assignment_test.In2_1_1
246
                        assignment_test.In2_1_2
247
                        assignment_test.In2_1_3
248
                        assignment_test.In2_1_4
249
                        assignment_test.In2_1_5
250
                        assignment_test.In2_1_6
251
                        assignment_test.In3_1_1
252
                        assignment_test.In3_1_2
253
                        assignment_test.In3_1_3
254
                        assignment_test.In3_1_4
255
                        assignment_test.In3_1_5
256
                        assignment_test.In3_1_6
257
                        assignment_test.In4_1_1
258
                        assignment_test.In4_1_2
259
                        assignment_test.In4_1_3
260
                        assignment_test.In5_1_1
261
                        assignment_test.In5_1_2
262
                        assignment_test.In5_1_3
263
                        assignment_test.In6_1_1
264
                        assignment_test.In6_1_2
265
                        assignment_test.In6_1_3
266
                        assignment_test.In7_1_1
267
                        assignment_test.In7_1_2
268
                        assignment_test.In7_1_3
269
                        assignment_test.In8_1_1
270
                        assignment_test.In8_1_2
271
                        assignment_test.In8_1_3
272
                        assignment_test.In8_1_4
273
                        assignment_test.In8_1_5
274
                        assignment_test.In8_1_6
275
                        assignment_test.Out1_1_1
276
                        assignment_test.Out1_1_2
277
                        assignment_test.Out1_1_3
278
                        assignment_test.Out1_1_4
279
                        assignment_test.Out1_1_5
280
                        assignment_test.Out1_1_6
281
                        assignment_test.Out2_2_1
282
                        assignment_test.Out2_2_2
283
                        assignment_test.Out2_2_3
284
                        assignment_test.Out2_2_4
285
                        assignment_test.Out2_2_5
286
                        assignment_test.Out2_2_6
287
                        assignment_test.Out3_3_1
288
                        assignment_test.Out3_3_2
289
                        assignment_test.Out3_3_3
290
                        assignment_test.Out3_3_4
291
                        assignment_test.Out3_3_5
292
                        assignment_test.Out3_3_6
293
                        assignment_test.Out4_4_1
294
                        assignment_test.Out4_4_2
295
                        assignment_test.Out4_4_3
296
                        assignment_test.Out5_5_1
297
                        assignment_test.Out5_5_2
298
                        assignment_test.Out5_5_3
299
                        assignment_test.Out6_6_1
300
                        assignment_test.Out6_6_2
301
                        assignment_test.Out6_6_3
302
                        assignment_test.Out7_7_1
303
                        assignment_test.Out7_7_2
304
                        assignment_test.Out7_7_3
305
                        assignment_test.Out8_8_1
306
                        assignment_test.Out8_8_2
307
                        assignment_test.Out8_8_3
308
                        assignment_test.Out8_8_4
309
                        assignment_test.Out8_8_5
310
                        assignment_test.Out8_8_6
311
                        assignment_test.ni_0._arrow._first_c
312
                        assignment_test.ni_0._arrow._first_x)
313
))
314