Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_sum_multi_test / sum_multi_test.smt2 @ 6c3ea955

History | View | Annotate | Download (15.5 KB)

1
; sum_multi_test
2
(declare-var sum_multi_test.In1_1_1 Real)
3
(declare-var sum_multi_test.In2_1_1 Real)
4
(declare-var sum_multi_test.In3_1_1 Real)
5
(declare-var sum_multi_test.In4_1_1 Real)
6
(declare-var sum_multi_test.In4_1_2 Real)
7
(declare-var sum_multi_test.In4_1_3 Real)
8
(declare-var sum_multi_test.In5_1_1 Real)
9
(declare-var sum_multi_test.In5_1_2 Real)
10
(declare-var sum_multi_test.In5_1_3 Real)
11
(declare-var sum_multi_test.In6_1_1 Real)
12
(declare-var sum_multi_test.In6_1_2 Real)
13
(declare-var sum_multi_test.In6_1_3 Real)
14
(declare-var sum_multi_test.In7_1_1 Real)
15
(declare-var sum_multi_test.In7_1_2 Real)
16
(declare-var sum_multi_test.In7_1_3 Real)
17
(declare-var sum_multi_test.In7_1_4 Real)
18
(declare-var sum_multi_test.In7_1_5 Real)
19
(declare-var sum_multi_test.In7_1_6 Real)
20
(declare-var sum_multi_test.In8_1_1 Real)
21
(declare-var sum_multi_test.In8_1_2 Real)
22
(declare-var sum_multi_test.In8_1_3 Real)
23
(declare-var sum_multi_test.In8_1_4 Real)
24
(declare-var sum_multi_test.In8_1_5 Real)
25
(declare-var sum_multi_test.In8_1_6 Real)
26
(declare-var sum_multi_test.In9_1_1 Real)
27
(declare-var sum_multi_test.In9_1_2 Real)
28
(declare-var sum_multi_test.In9_1_3 Real)
29
(declare-var sum_multi_test.In9_1_4 Real)
30
(declare-var sum_multi_test.In9_1_5 Real)
31
(declare-var sum_multi_test.In9_1_6 Real)
32
(declare-var sum_multi_test.In10_1_1 Real)
33
(declare-var sum_multi_test.In11_1_1 Real)
34
(declare-var sum_multi_test.In11_1_2 Real)
35
(declare-var sum_multi_test.In11_1_3 Real)
36
(declare-var sum_multi_test.In12_1_1 Real)
37
(declare-var sum_multi_test.In13_1_1 Real)
38
(declare-var sum_multi_test.In13_1_2 Real)
39
(declare-var sum_multi_test.In13_1_3 Real)
40
(declare-var sum_multi_test.In14_1_1 Real)
41
(declare-var sum_multi_test.In15_1_1 Real)
42
(declare-var sum_multi_test.In15_1_2 Real)
43
(declare-var sum_multi_test.In15_1_3 Real)
44
(declare-var sum_multi_test.In16_1_1 Real)
45
(declare-var sum_multi_test.In17_1_1 Real)
46
(declare-var sum_multi_test.In17_1_2 Real)
47
(declare-var sum_multi_test.In17_1_3 Real)
48
(declare-var sum_multi_test.In17_1_4 Real)
49
(declare-var sum_multi_test.In17_1_5 Real)
50
(declare-var sum_multi_test.In17_1_6 Real)
51
(declare-var sum_multi_test.In18_1_1 Real)
52
(declare-var sum_multi_test.In19_1_1 Real)
53
(declare-var sum_multi_test.In19_1_2 Real)
54
(declare-var sum_multi_test.In19_1_3 Real)
55
(declare-var sum_multi_test.In19_1_4 Real)
56
(declare-var sum_multi_test.In19_1_5 Real)
57
(declare-var sum_multi_test.In19_1_6 Real)
58
(declare-var sum_multi_test.In20_1_1 Real)
59
(declare-var sum_multi_test.In21_1_1 Real)
60
(declare-var sum_multi_test.In21_1_2 Real)
61
(declare-var sum_multi_test.In21_1_3 Real)
62
(declare-var sum_multi_test.In21_1_4 Real)
63
(declare-var sum_multi_test.In21_1_5 Real)
64
(declare-var sum_multi_test.In21_1_6 Real)
65
(declare-var sum_multi_test.Out1_1_1 Real)
66
(declare-var sum_multi_test.Out2_2_1 Real)
67
(declare-var sum_multi_test.Out2_2_2 Real)
68
(declare-var sum_multi_test.Out2_2_3 Real)
69
(declare-var sum_multi_test.Out3_3_1 Real)
70
(declare-var sum_multi_test.Out3_3_2 Real)
71
(declare-var sum_multi_test.Out3_3_3 Real)
72
(declare-var sum_multi_test.Out3_3_4 Real)
73
(declare-var sum_multi_test.Out3_3_5 Real)
74
(declare-var sum_multi_test.Out3_3_6 Real)
75
(declare-var sum_multi_test.Out4_4_1 Real)
76
(declare-var sum_multi_test.Out4_4_2 Real)
77
(declare-var sum_multi_test.Out4_4_3 Real)
78
(declare-var sum_multi_test.Out5_5_1 Real)
79
(declare-var sum_multi_test.Out5_5_2 Real)
80
(declare-var sum_multi_test.Out5_5_3 Real)
81
(declare-var sum_multi_test.Out6_6_1 Real)
82
(declare-var sum_multi_test.Out6_6_2 Real)
83
(declare-var sum_multi_test.Out6_6_3 Real)
84
(declare-var sum_multi_test.Out6_6_4 Real)
85
(declare-var sum_multi_test.Out6_6_5 Real)
86
(declare-var sum_multi_test.Out6_6_6 Real)
87
(declare-var sum_multi_test.Out7_7_1 Real)
88
(declare-var sum_multi_test.Out7_7_2 Real)
89
(declare-var sum_multi_test.Out7_7_3 Real)
90
(declare-var sum_multi_test.Out7_7_4 Real)
91
(declare-var sum_multi_test.Out7_7_5 Real)
92
(declare-var sum_multi_test.Out7_7_6 Real)
93
(declare-var sum_multi_test.ni_0._arrow._first_c Bool)
94
(declare-var sum_multi_test.ni_0._arrow._first_m Bool)
95
(declare-var sum_multi_test.ni_0._arrow._first_x Bool)
96
(declare-var sum_multi_test.Sum1_1_1 Real)
97
(declare-var sum_multi_test.Sum1_1_2 Real)
98
(declare-var sum_multi_test.Sum1_1_3 Real)
99
(declare-var sum_multi_test.Sum2_1_1 Real)
100
(declare-var sum_multi_test.Sum2_1_2 Real)
101
(declare-var sum_multi_test.Sum2_1_3 Real)
102
(declare-var sum_multi_test.Sum2_1_4 Real)
103
(declare-var sum_multi_test.Sum2_1_5 Real)
104
(declare-var sum_multi_test.Sum2_1_6 Real)
105
(declare-var sum_multi_test.Sum3_1_1 Real)
106
(declare-var sum_multi_test.Sum3_1_2 Real)
107
(declare-var sum_multi_test.Sum3_1_3 Real)
108
(declare-var sum_multi_test.Sum4_1_1 Real)
109
(declare-var sum_multi_test.Sum4_1_2 Real)
110
(declare-var sum_multi_test.Sum4_1_3 Real)
111
(declare-var sum_multi_test.Sum5_1_1 Real)
112
(declare-var sum_multi_test.Sum5_1_2 Real)
113
(declare-var sum_multi_test.Sum5_1_3 Real)
114
(declare-var sum_multi_test.Sum5_1_4 Real)
115
(declare-var sum_multi_test.Sum5_1_5 Real)
116
(declare-var sum_multi_test.Sum5_1_6 Real)
117
(declare-var sum_multi_test.Sum6_1_1 Real)
118
(declare-var sum_multi_test.Sum6_1_2 Real)
119
(declare-var sum_multi_test.Sum6_1_3 Real)
120
(declare-var sum_multi_test.Sum6_1_4 Real)
121
(declare-var sum_multi_test.Sum6_1_5 Real)
122
(declare-var sum_multi_test.Sum6_1_6 Real)
123
(declare-var sum_multi_test.Sum_1_1 Real)
124
(declare-var sum_multi_test.__sum_multi_test_1 Bool)
125
(declare-var sum_multi_test.i_virtual_local Real)
126
(declare-rel sum_multi_test_reset (Bool Bool))
127
(declare-rel sum_multi_test_step (Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Bool Bool))
128

    
129
(rule (=> 
130
  (and 
131
       
132
       (= sum_multi_test.ni_0._arrow._first_m true)
133
  )
134
  (sum_multi_test_reset sum_multi_test.ni_0._arrow._first_c
135
                        sum_multi_test.ni_0._arrow._first_m)
136
))
137

    
138
(rule (=> 
139
  (and (= sum_multi_test.ni_0._arrow._first_m sum_multi_test.ni_0._arrow._first_c)
140
       (and (= sum_multi_test.__sum_multi_test_1 (ite sum_multi_test.ni_0._arrow._first_m true false))
141
            (= sum_multi_test.ni_0._arrow._first_x false))
142
       (and (or (not (= sum_multi_test.__sum_multi_test_1 true))
143
               (= sum_multi_test.i_virtual_local 0.0))
144
            (or (not (= sum_multi_test.__sum_multi_test_1 false))
145
               (= sum_multi_test.i_virtual_local 1.0))
146
       )
147
       (= sum_multi_test.Sum_1_1 (+ (- sum_multi_test.In1_1_1 sum_multi_test.In2_1_1) sum_multi_test.In3_1_1))
148
       (= sum_multi_test.Sum6_1_6 (- (- (- sum_multi_test.In19_1_6) sum_multi_test.In20_1_1) sum_multi_test.In21_1_6))
149
       (= sum_multi_test.Sum6_1_5 (- (- (- sum_multi_test.In19_1_5) sum_multi_test.In20_1_1) sum_multi_test.In21_1_5))
150
       (= sum_multi_test.Sum6_1_4 (- (- (- sum_multi_test.In19_1_4) sum_multi_test.In20_1_1) sum_multi_test.In21_1_4))
151
       (= sum_multi_test.Sum6_1_3 (- (- (- sum_multi_test.In19_1_3) sum_multi_test.In20_1_1) sum_multi_test.In21_1_3))
152
       (= sum_multi_test.Sum6_1_2 (- (- (- sum_multi_test.In19_1_2) sum_multi_test.In20_1_1) sum_multi_test.In21_1_2))
153
       (= sum_multi_test.Sum6_1_1 (- (- (- sum_multi_test.In19_1_1) sum_multi_test.In20_1_1) sum_multi_test.In21_1_1))
154
       (= sum_multi_test.Sum5_1_6 (+ (+ (- sum_multi_test.In16_1_1) sum_multi_test.In17_1_6) sum_multi_test.In18_1_1))
155
       (= sum_multi_test.Sum5_1_5 (+ (+ (- sum_multi_test.In16_1_1) sum_multi_test.In17_1_5) sum_multi_test.In18_1_1))
156
       (= sum_multi_test.Sum5_1_4 (+ (+ (- sum_multi_test.In16_1_1) sum_multi_test.In17_1_4) sum_multi_test.In18_1_1))
157
       (= sum_multi_test.Sum5_1_3 (+ (+ (- sum_multi_test.In16_1_1) sum_multi_test.In17_1_3) sum_multi_test.In18_1_1))
158
       (= sum_multi_test.Sum5_1_2 (+ (+ (- sum_multi_test.In16_1_1) sum_multi_test.In17_1_2) sum_multi_test.In18_1_1))
159
       (= sum_multi_test.Sum5_1_1 (+ (+ (- sum_multi_test.In16_1_1) sum_multi_test.In17_1_1) sum_multi_test.In18_1_1))
160
       (= sum_multi_test.Sum4_1_3 (- (+ sum_multi_test.In13_1_3 sum_multi_test.In14_1_1) sum_multi_test.In15_1_3))
161
       (= sum_multi_test.Sum4_1_2 (- (+ sum_multi_test.In13_1_2 sum_multi_test.In14_1_1) sum_multi_test.In15_1_2))
162
       (= sum_multi_test.Sum4_1_1 (- (+ sum_multi_test.In13_1_1 sum_multi_test.In14_1_1) sum_multi_test.In15_1_1))
163
       (= sum_multi_test.Sum3_1_3 (+ (+ (- sum_multi_test.In10_1_1) sum_multi_test.In11_1_3) sum_multi_test.In12_1_1))
164
       (= sum_multi_test.Sum3_1_2 (+ (+ (- sum_multi_test.In10_1_1) sum_multi_test.In11_1_2) sum_multi_test.In12_1_1))
165
       (= sum_multi_test.Sum3_1_1 (+ (+ (- sum_multi_test.In10_1_1) sum_multi_test.In11_1_1) sum_multi_test.In12_1_1))
166
       (= sum_multi_test.Sum2_1_6 (+ (- sum_multi_test.In7_1_6 sum_multi_test.In8_1_6) sum_multi_test.In9_1_6))
167
       (= sum_multi_test.Sum2_1_5 (+ (- sum_multi_test.In7_1_5 sum_multi_test.In8_1_5) sum_multi_test.In9_1_5))
168
       (= sum_multi_test.Sum2_1_4 (+ (- sum_multi_test.In7_1_4 sum_multi_test.In8_1_4) sum_multi_test.In9_1_4))
169
       (= sum_multi_test.Sum2_1_3 (+ (- sum_multi_test.In7_1_3 sum_multi_test.In8_1_3) sum_multi_test.In9_1_3))
170
       (= sum_multi_test.Sum2_1_2 (+ (- sum_multi_test.In7_1_2 sum_multi_test.In8_1_2) sum_multi_test.In9_1_2))
171
       (= sum_multi_test.Sum2_1_1 (+ (- sum_multi_test.In7_1_1 sum_multi_test.In8_1_1) sum_multi_test.In9_1_1))
172
       (= sum_multi_test.Sum1_1_3 (+ (- sum_multi_test.In4_1_3 sum_multi_test.In5_1_3) sum_multi_test.In6_1_3))
173
       (= sum_multi_test.Sum1_1_2 (+ (- sum_multi_test.In4_1_2 sum_multi_test.In5_1_2) sum_multi_test.In6_1_2))
174
       (= sum_multi_test.Sum1_1_1 (+ (- sum_multi_test.In4_1_1 sum_multi_test.In5_1_1) sum_multi_test.In6_1_1))
175
       (= sum_multi_test.Out7_7_6 sum_multi_test.Sum6_1_6)
176
       (= sum_multi_test.Out7_7_5 sum_multi_test.Sum6_1_5)
177
       (= sum_multi_test.Out7_7_4 sum_multi_test.Sum6_1_4)
178
       (= sum_multi_test.Out7_7_3 sum_multi_test.Sum6_1_3)
179
       (= sum_multi_test.Out7_7_2 sum_multi_test.Sum6_1_2)
180
       (= sum_multi_test.Out7_7_1 sum_multi_test.Sum6_1_1)
181
       (= sum_multi_test.Out6_6_6 sum_multi_test.Sum5_1_6)
182
       (= sum_multi_test.Out6_6_5 sum_multi_test.Sum5_1_5)
183
       (= sum_multi_test.Out6_6_4 sum_multi_test.Sum5_1_4)
184
       (= sum_multi_test.Out6_6_3 sum_multi_test.Sum5_1_3)
185
       (= sum_multi_test.Out6_6_2 sum_multi_test.Sum5_1_2)
186
       (= sum_multi_test.Out6_6_1 sum_multi_test.Sum5_1_1)
187
       (= sum_multi_test.Out5_5_3 sum_multi_test.Sum4_1_3)
188
       (= sum_multi_test.Out5_5_2 sum_multi_test.Sum4_1_2)
189
       (= sum_multi_test.Out5_5_1 sum_multi_test.Sum4_1_1)
190
       (= sum_multi_test.Out4_4_3 sum_multi_test.Sum3_1_3)
191
       (= sum_multi_test.Out4_4_2 sum_multi_test.Sum3_1_2)
192
       (= sum_multi_test.Out4_4_1 sum_multi_test.Sum3_1_1)
193
       (= sum_multi_test.Out3_3_6 sum_multi_test.Sum2_1_6)
194
       (= sum_multi_test.Out3_3_5 sum_multi_test.Sum2_1_5)
195
       (= sum_multi_test.Out3_3_4 sum_multi_test.Sum2_1_4)
196
       (= sum_multi_test.Out3_3_3 sum_multi_test.Sum2_1_3)
197
       (= sum_multi_test.Out3_3_2 sum_multi_test.Sum2_1_2)
198
       (= sum_multi_test.Out3_3_1 sum_multi_test.Sum2_1_1)
199
       (= sum_multi_test.Out2_2_3 sum_multi_test.Sum1_1_3)
200
       (= sum_multi_test.Out2_2_2 sum_multi_test.Sum1_1_2)
201
       (= sum_multi_test.Out2_2_1 sum_multi_test.Sum1_1_1)
202
       (= sum_multi_test.Out1_1_1 sum_multi_test.Sum_1_1)
203
       )
204
  (sum_multi_test_step sum_multi_test.In1_1_1
205
                       sum_multi_test.In2_1_1
206
                       sum_multi_test.In3_1_1
207
                       sum_multi_test.In4_1_1
208
                       sum_multi_test.In4_1_2
209
                       sum_multi_test.In4_1_3
210
                       sum_multi_test.In5_1_1
211
                       sum_multi_test.In5_1_2
212
                       sum_multi_test.In5_1_3
213
                       sum_multi_test.In6_1_1
214
                       sum_multi_test.In6_1_2
215
                       sum_multi_test.In6_1_3
216
                       sum_multi_test.In7_1_1
217
                       sum_multi_test.In7_1_2
218
                       sum_multi_test.In7_1_3
219
                       sum_multi_test.In7_1_4
220
                       sum_multi_test.In7_1_5
221
                       sum_multi_test.In7_1_6
222
                       sum_multi_test.In8_1_1
223
                       sum_multi_test.In8_1_2
224
                       sum_multi_test.In8_1_3
225
                       sum_multi_test.In8_1_4
226
                       sum_multi_test.In8_1_5
227
                       sum_multi_test.In8_1_6
228
                       sum_multi_test.In9_1_1
229
                       sum_multi_test.In9_1_2
230
                       sum_multi_test.In9_1_3
231
                       sum_multi_test.In9_1_4
232
                       sum_multi_test.In9_1_5
233
                       sum_multi_test.In9_1_6
234
                       sum_multi_test.In10_1_1
235
                       sum_multi_test.In11_1_1
236
                       sum_multi_test.In11_1_2
237
                       sum_multi_test.In11_1_3
238
                       sum_multi_test.In12_1_1
239
                       sum_multi_test.In13_1_1
240
                       sum_multi_test.In13_1_2
241
                       sum_multi_test.In13_1_3
242
                       sum_multi_test.In14_1_1
243
                       sum_multi_test.In15_1_1
244
                       sum_multi_test.In15_1_2
245
                       sum_multi_test.In15_1_3
246
                       sum_multi_test.In16_1_1
247
                       sum_multi_test.In17_1_1
248
                       sum_multi_test.In17_1_2
249
                       sum_multi_test.In17_1_3
250
                       sum_multi_test.In17_1_4
251
                       sum_multi_test.In17_1_5
252
                       sum_multi_test.In17_1_6
253
                       sum_multi_test.In18_1_1
254
                       sum_multi_test.In19_1_1
255
                       sum_multi_test.In19_1_2
256
                       sum_multi_test.In19_1_3
257
                       sum_multi_test.In19_1_4
258
                       sum_multi_test.In19_1_5
259
                       sum_multi_test.In19_1_6
260
                       sum_multi_test.In20_1_1
261
                       sum_multi_test.In21_1_1
262
                       sum_multi_test.In21_1_2
263
                       sum_multi_test.In21_1_3
264
                       sum_multi_test.In21_1_4
265
                       sum_multi_test.In21_1_5
266
                       sum_multi_test.In21_1_6
267
                       sum_multi_test.Out1_1_1
268
                       sum_multi_test.Out2_2_1
269
                       sum_multi_test.Out2_2_2
270
                       sum_multi_test.Out2_2_3
271
                       sum_multi_test.Out3_3_1
272
                       sum_multi_test.Out3_3_2
273
                       sum_multi_test.Out3_3_3
274
                       sum_multi_test.Out3_3_4
275
                       sum_multi_test.Out3_3_5
276
                       sum_multi_test.Out3_3_6
277
                       sum_multi_test.Out4_4_1
278
                       sum_multi_test.Out4_4_2
279
                       sum_multi_test.Out4_4_3
280
                       sum_multi_test.Out5_5_1
281
                       sum_multi_test.Out5_5_2
282
                       sum_multi_test.Out5_5_3
283
                       sum_multi_test.Out6_6_1
284
                       sum_multi_test.Out6_6_2
285
                       sum_multi_test.Out6_6_3
286
                       sum_multi_test.Out6_6_4
287
                       sum_multi_test.Out6_6_5
288
                       sum_multi_test.Out6_6_6
289
                       sum_multi_test.Out7_7_1
290
                       sum_multi_test.Out7_7_2
291
                       sum_multi_test.Out7_7_3
292
                       sum_multi_test.Out7_7_4
293
                       sum_multi_test.Out7_7_5
294
                       sum_multi_test.Out7_7_6
295
                       sum_multi_test.ni_0._arrow._first_c
296
                       sum_multi_test.ni_0._arrow._first_x)
297
))
298