Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_sum_test / sum_test.smt2 @ 6c3ea955

History | View | Annotate | Download (10 KB)

1
; sum_test
2
(declare-var sum_test.In1_1_1 Real)
3
(declare-var sum_test.In2_1_1 Real)
4
(declare-var sum_test.In3_1_1 Real)
5
(declare-var sum_test.In3_1_2 Real)
6
(declare-var sum_test.In3_1_3 Real)
7
(declare-var sum_test.In4_1_1 Real)
8
(declare-var sum_test.In4_1_2 Real)
9
(declare-var sum_test.In4_1_3 Real)
10
(declare-var sum_test.In5_1_1 Real)
11
(declare-var sum_test.In5_1_2 Real)
12
(declare-var sum_test.In5_1_3 Real)
13
(declare-var sum_test.In5_1_4 Real)
14
(declare-var sum_test.In5_1_5 Real)
15
(declare-var sum_test.In5_1_6 Real)
16
(declare-var sum_test.In6_1_1 Real)
17
(declare-var sum_test.In6_1_2 Real)
18
(declare-var sum_test.In6_1_3 Real)
19
(declare-var sum_test.In6_1_4 Real)
20
(declare-var sum_test.In6_1_5 Real)
21
(declare-var sum_test.In6_1_6 Real)
22
(declare-var sum_test.In7_1_1 Int)
23
(declare-var sum_test.In8_1_1 Int)
24
(declare-var sum_test.In9_1_1 Int)
25
(declare-var sum_test.In9_1_2 Int)
26
(declare-var sum_test.In9_1_3 Int)
27
(declare-var sum_test.In10_1_1 Int)
28
(declare-var sum_test.In10_1_2 Int)
29
(declare-var sum_test.In10_1_3 Int)
30
(declare-var sum_test.In11_1_1 Int)
31
(declare-var sum_test.In11_1_2 Int)
32
(declare-var sum_test.In11_1_3 Int)
33
(declare-var sum_test.In11_1_4 Int)
34
(declare-var sum_test.In11_1_5 Int)
35
(declare-var sum_test.In11_1_6 Int)
36
(declare-var sum_test.In12_1_1 Int)
37
(declare-var sum_test.In12_1_2 Int)
38
(declare-var sum_test.In12_1_3 Int)
39
(declare-var sum_test.In12_1_4 Int)
40
(declare-var sum_test.In12_1_5 Int)
41
(declare-var sum_test.In12_1_6 Int)
42
(declare-var sum_test.In13_1_1 Int)
43
(declare-var sum_test.In14_1_1 Int)
44
(declare-var sum_test.In15_1_1 Int)
45
(declare-var sum_test.In15_1_2 Int)
46
(declare-var sum_test.In15_1_3 Int)
47
(declare-var sum_test.In16_1_1 Int)
48
(declare-var sum_test.In16_1_2 Int)
49
(declare-var sum_test.In16_1_3 Int)
50
(declare-var sum_test.In17_1_1 Int)
51
(declare-var sum_test.In17_1_2 Int)
52
(declare-var sum_test.In17_1_3 Int)
53
(declare-var sum_test.In17_1_4 Int)
54
(declare-var sum_test.In17_1_5 Int)
55
(declare-var sum_test.In17_1_6 Int)
56
(declare-var sum_test.In18_1_1 Int)
57
(declare-var sum_test.In18_1_2 Int)
58
(declare-var sum_test.In18_1_3 Int)
59
(declare-var sum_test.In18_1_4 Int)
60
(declare-var sum_test.In18_1_5 Int)
61
(declare-var sum_test.In18_1_6 Int)
62
(declare-var sum_test.Out1_1_1 Real)
63
(declare-var sum_test.Out2_2_1 Real)
64
(declare-var sum_test.Out3_3_1 Real)
65
(declare-var sum_test.Out4_4_1 Real)
66
(declare-var sum_test.Out5_5_1 Real)
67
(declare-var sum_test.Out6_6_1 Real)
68
(declare-var sum_test.Out7_7_1 Int)
69
(declare-var sum_test.Out8_8_1 Int)
70
(declare-var sum_test.Out9_9_1 Int)
71
(declare-var sum_test.Out10_10_1 Int)
72
(declare-var sum_test.Out11_11_1 Int)
73
(declare-var sum_test.Out12_12_1 Int)
74
(declare-var sum_test.Out13_13_1 Int)
75
(declare-var sum_test.Out14_14_1 Int)
76
(declare-var sum_test.Out15_15_1 Int)
77
(declare-var sum_test.Out16_16_1 Int)
78
(declare-var sum_test.Out17_17_1 Int)
79
(declare-var sum_test.Out18_18_1 Int)
80
(declare-var sum_test.ni_0._arrow._first_c Bool)
81
(declare-var sum_test.ni_0._arrow._first_m Bool)
82
(declare-var sum_test.ni_0._arrow._first_x Bool)
83
(declare-var sum_test.Sum10_1_1 Int)
84
(declare-var sum_test.Sum11_1_1 Int)
85
(declare-var sum_test.Sum12_1_1 Int)
86
(declare-var sum_test.Sum13_1_1 Int)
87
(declare-var sum_test.Sum14_1_1 Int)
88
(declare-var sum_test.Sum15_1_1 Int)
89
(declare-var sum_test.Sum16_1_1 Int)
90
(declare-var sum_test.Sum17_1_1 Int)
91
(declare-var sum_test.Sum1_1_1 Real)
92
(declare-var sum_test.Sum2_1_1 Real)
93
(declare-var sum_test.Sum3_1_1 Real)
94
(declare-var sum_test.Sum4_1_1 Real)
95
(declare-var sum_test.Sum5_1_1 Real)
96
(declare-var sum_test.Sum6_1_1 Int)
97
(declare-var sum_test.Sum7_1_1 Int)
98
(declare-var sum_test.Sum8_1_1 Int)
99
(declare-var sum_test.Sum9_1_1 Int)
100
(declare-var sum_test.Sum_1_1 Real)
101
(declare-var sum_test.__sum_test_1 Bool)
102
(declare-var sum_test.i_virtual_local Real)
103
(declare-rel sum_test_reset (Bool Bool))
104
(declare-rel sum_test_step (Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Real Real Real Real Real Real Int Int Int Int Int Int Int Int Int Int Int Int Bool Bool))
105

    
106
(rule (=> 
107
  (and 
108
       
109
       (= sum_test.ni_0._arrow._first_m true)
110
  )
111
  (sum_test_reset sum_test.ni_0._arrow._first_c
112
                  sum_test.ni_0._arrow._first_m)
113
))
114

    
115
(rule (=> 
116
  (and (= sum_test.ni_0._arrow._first_m sum_test.ni_0._arrow._first_c)
117
       (and (= sum_test.__sum_test_1 (ite sum_test.ni_0._arrow._first_m true false))
118
            (= sum_test.ni_0._arrow._first_x false))
119
       (and (or (not (= sum_test.__sum_test_1 true))
120
               (= sum_test.i_virtual_local 0.0))
121
            (or (not (= sum_test.__sum_test_1 false))
122
               (= sum_test.i_virtual_local 1.0))
123
       )
124
       (= sum_test.Sum_1_1 sum_test.In1_1_1)
125
       (= sum_test.Sum9_1_1 (- (- (- sum_test.In10_1_1) sum_test.In10_1_2) sum_test.In10_1_3))
126
       (= sum_test.Sum8_1_1 (+ (+ sum_test.In9_1_1 sum_test.In9_1_2) sum_test.In9_1_3))
127
       (= sum_test.Sum7_1_1 (- sum_test.In8_1_1))
128
       (= sum_test.Sum6_1_1 sum_test.In7_1_1)
129
       (= sum_test.Sum5_1_1 (- (- (- (- (- (- sum_test.In6_1_1) sum_test.In6_1_2) sum_test.In6_1_3) sum_test.In6_1_4) sum_test.In6_1_5) sum_test.In6_1_6))
130
       (= sum_test.Sum4_1_1 (+ (+ (+ (+ (+ sum_test.In5_1_1 sum_test.In5_1_2) sum_test.In5_1_3) sum_test.In5_1_4) sum_test.In5_1_5) sum_test.In5_1_6))
131
       (= sum_test.Sum3_1_1 (- (- (- sum_test.In4_1_1) sum_test.In4_1_2) sum_test.In4_1_3))
132
       (= sum_test.Sum2_1_1 (+ (+ sum_test.In3_1_1 sum_test.In3_1_2) sum_test.In3_1_3))
133
       (= sum_test.Sum1_1_1 (- sum_test.In2_1_1))
134
       (= sum_test.Sum17_1_1 (- (- (- sum_test.In16_1_1) sum_test.In16_1_2) sum_test.In16_1_3))
135
       (= sum_test.Sum16_1_1 (+ (+ sum_test.In15_1_1 sum_test.In15_1_2) sum_test.In15_1_3))
136
       (= sum_test.Sum15_1_1 (- sum_test.In14_1_1))
137
       (= sum_test.Sum14_1_1 sum_test.In13_1_1)
138
       (= sum_test.Sum13_1_1 (- (- (- (- (- (- sum_test.In18_1_1) sum_test.In18_1_2) sum_test.In18_1_3) sum_test.In18_1_4) sum_test.In18_1_5) sum_test.In18_1_6))
139
       (= sum_test.Sum12_1_1 (+ (+ (+ (+ (+ sum_test.In17_1_1 sum_test.In17_1_2) sum_test.In17_1_3) sum_test.In17_1_4) sum_test.In17_1_5) sum_test.In17_1_6))
140
       (= sum_test.Sum11_1_1 (- (- (- (- (- (- sum_test.In12_1_1) sum_test.In12_1_2) sum_test.In12_1_3) sum_test.In12_1_4) sum_test.In12_1_5) sum_test.In12_1_6))
141
       (= sum_test.Sum10_1_1 (+ (+ (+ (+ (+ sum_test.In11_1_1 sum_test.In11_1_2) sum_test.In11_1_3) sum_test.In11_1_4) sum_test.In11_1_5) sum_test.In11_1_6))
142
       (= sum_test.Out9_9_1 sum_test.Sum8_1_1)
143
       (= sum_test.Out8_8_1 sum_test.Sum7_1_1)
144
       (= sum_test.Out7_7_1 sum_test.Sum6_1_1)
145
       (= sum_test.Out6_6_1 sum_test.Sum5_1_1)
146
       (= sum_test.Out5_5_1 sum_test.Sum4_1_1)
147
       (= sum_test.Out4_4_1 sum_test.Sum3_1_1)
148
       (= sum_test.Out3_3_1 sum_test.Sum2_1_1)
149
       (= sum_test.Out2_2_1 sum_test.Sum1_1_1)
150
       (= sum_test.Out1_1_1 sum_test.Sum_1_1)
151
       (= sum_test.Out18_18_1 sum_test.Sum13_1_1)
152
       (= sum_test.Out17_17_1 sum_test.Sum12_1_1)
153
       (= sum_test.Out16_16_1 sum_test.Sum17_1_1)
154
       (= sum_test.Out15_15_1 sum_test.Sum16_1_1)
155
       (= sum_test.Out14_14_1 sum_test.Sum15_1_1)
156
       (= sum_test.Out13_13_1 sum_test.Sum14_1_1)
157
       (= sum_test.Out12_12_1 sum_test.Sum11_1_1)
158
       (= sum_test.Out11_11_1 sum_test.Sum10_1_1)
159
       (= sum_test.Out10_10_1 sum_test.Sum9_1_1)
160
       )
161
  (sum_test_step sum_test.In1_1_1
162
                 sum_test.In2_1_1
163
                 sum_test.In3_1_1
164
                 sum_test.In3_1_2
165
                 sum_test.In3_1_3
166
                 sum_test.In4_1_1
167
                 sum_test.In4_1_2
168
                 sum_test.In4_1_3
169
                 sum_test.In5_1_1
170
                 sum_test.In5_1_2
171
                 sum_test.In5_1_3
172
                 sum_test.In5_1_4
173
                 sum_test.In5_1_5
174
                 sum_test.In5_1_6
175
                 sum_test.In6_1_1
176
                 sum_test.In6_1_2
177
                 sum_test.In6_1_3
178
                 sum_test.In6_1_4
179
                 sum_test.In6_1_5
180
                 sum_test.In6_1_6
181
                 sum_test.In7_1_1
182
                 sum_test.In8_1_1
183
                 sum_test.In9_1_1
184
                 sum_test.In9_1_2
185
                 sum_test.In9_1_3
186
                 sum_test.In10_1_1
187
                 sum_test.In10_1_2
188
                 sum_test.In10_1_3
189
                 sum_test.In11_1_1
190
                 sum_test.In11_1_2
191
                 sum_test.In11_1_3
192
                 sum_test.In11_1_4
193
                 sum_test.In11_1_5
194
                 sum_test.In11_1_6
195
                 sum_test.In12_1_1
196
                 sum_test.In12_1_2
197
                 sum_test.In12_1_3
198
                 sum_test.In12_1_4
199
                 sum_test.In12_1_5
200
                 sum_test.In12_1_6
201
                 sum_test.In13_1_1
202
                 sum_test.In14_1_1
203
                 sum_test.In15_1_1
204
                 sum_test.In15_1_2
205
                 sum_test.In15_1_3
206
                 sum_test.In16_1_1
207
                 sum_test.In16_1_2
208
                 sum_test.In16_1_3
209
                 sum_test.In17_1_1
210
                 sum_test.In17_1_2
211
                 sum_test.In17_1_3
212
                 sum_test.In17_1_4
213
                 sum_test.In17_1_5
214
                 sum_test.In17_1_6
215
                 sum_test.In18_1_1
216
                 sum_test.In18_1_2
217
                 sum_test.In18_1_3
218
                 sum_test.In18_1_4
219
                 sum_test.In18_1_5
220
                 sum_test.In18_1_6
221
                 sum_test.Out1_1_1
222
                 sum_test.Out2_2_1
223
                 sum_test.Out3_3_1
224
                 sum_test.Out4_4_1
225
                 sum_test.Out5_5_1
226
                 sum_test.Out6_6_1
227
                 sum_test.Out7_7_1
228
                 sum_test.Out8_8_1
229
                 sum_test.Out9_9_1
230
                 sum_test.Out10_10_1
231
                 sum_test.Out11_11_1
232
                 sum_test.Out12_12_1
233
                 sum_test.Out13_13_1
234
                 sum_test.Out14_14_1
235
                 sum_test.Out15_15_1
236
                 sum_test.Out16_16_1
237
                 sum_test.Out17_17_1
238
                 sum_test.Out18_18_1
239
                 sum_test.ni_0._arrow._first_c
240
                 sum_test.ni_0._arrow._first_x)
241
))
242