Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_integrator_ext_reset_test / integrator_ext_reset_test.smt2 @ 6c3ea955

History | View | Annotate | Download (40.8 KB)

1
; integrator_ext_reset_test
2
(declare-var integrator_ext_reset_test.In4_1_1 Real)
3
(declare-var integrator_ext_reset_test.In5_1_1 Int)
4
(declare-var integrator_ext_reset_test.In6_1_1 Bool)
5
(declare-var integrator_ext_reset_test.In7_1_1 Real)
6
(declare-var integrator_ext_reset_test.In8_1_1 Real)
7
(declare-var integrator_ext_reset_test.In9_1_1 Real)
8
(declare-var integrator_ext_reset_test.In10_1_1 Real)
9
(declare-var integrator_ext_reset_test.In11_1_1 Int)
10
(declare-var integrator_ext_reset_test.In12_1_1 Bool)
11
(declare-var integrator_ext_reset_test.In13_1_1 Int)
12
(declare-var integrator_ext_reset_test.In14_1_1 Int)
13
(declare-var integrator_ext_reset_test.In15_1_1 Int)
14
(declare-var integrator_ext_reset_test.In16_1_1 Real)
15
(declare-var integrator_ext_reset_test.In17_1_1 Int)
16
(declare-var integrator_ext_reset_test.In18_1_1 Bool)
17
(declare-var integrator_ext_reset_test.In19_1_1 Bool)
18
(declare-var integrator_ext_reset_test.In20_1_1 Bool)
19
(declare-var integrator_ext_reset_test.In21_1_1 Bool)
20
(declare-var integrator_ext_reset_test.Out4_1_1 Real)
21
(declare-var integrator_ext_reset_test.Out5_2_1 Int)
22
(declare-var integrator_ext_reset_test.Out6_3_1 Int)
23
(declare-var integrator_ext_reset_test.Out7_4_1 Real)
24
(declare-var integrator_ext_reset_test.Out8_5_1 Int)
25
(declare-var integrator_ext_reset_test.Out9_6_1 Int)
26
(declare-var integrator_ext_reset_test.Out10_7_1 Real)
27
(declare-var integrator_ext_reset_test.Out11_8_1 Int)
28
(declare-var integrator_ext_reset_test.Out12_9_1 Int)
29
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_10_c Int)
30
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_11_c Int)
31
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_12_c Real)
32
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_13_c Real)
33
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_14_c Int)
34
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_15_c Int)
35
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_17_c Int)
36
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_18_c Real)
37
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_19_c Int)
38
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_2_c Real)
39
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_20_c Int)
40
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_21_c Real)
41
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_22_c Real)
42
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_23_c Real)
43
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_24_c Real)
44
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_25_c Int)
45
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_27_c Int)
46
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_28_c Bool)
47
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_29_c Int)
48
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_3_c Real)
49
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_30_c Int)
50
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_31_c Bool)
51
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_4_c Bool)
52
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_5_c Int)
53
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_7_c Int)
54
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_8_c Int)
55
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_9_c Int)
56
(declare-var integrator_ext_reset_test.ni_0._arrow._first_c Bool)
57
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_10_m Int)
58
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_11_m Int)
59
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_12_m Real)
60
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_13_m Real)
61
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_14_m Int)
62
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_15_m Int)
63
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_17_m Int)
64
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_18_m Real)
65
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_19_m Int)
66
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_2_m Real)
67
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_20_m Int)
68
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_21_m Real)
69
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_22_m Real)
70
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_23_m Real)
71
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_24_m Real)
72
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_25_m Int)
73
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_27_m Int)
74
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_28_m Bool)
75
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_29_m Int)
76
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_3_m Real)
77
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_30_m Int)
78
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_31_m Bool)
79
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_4_m Bool)
80
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_5_m Int)
81
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_7_m Int)
82
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_8_m Int)
83
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_9_m Int)
84
(declare-var integrator_ext_reset_test.ni_0._arrow._first_m Bool)
85
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_10_x Int)
86
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_11_x Int)
87
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_12_x Real)
88
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_13_x Real)
89
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_14_x Int)
90
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_15_x Int)
91
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_17_x Int)
92
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_18_x Real)
93
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_19_x Int)
94
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_2_x Real)
95
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_20_x Int)
96
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_21_x Real)
97
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_22_x Real)
98
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_23_x Real)
99
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_24_x Real)
100
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_25_x Int)
101
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_27_x Int)
102
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_28_x Bool)
103
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_29_x Int)
104
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_3_x Real)
105
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_30_x Int)
106
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_31_x Bool)
107
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_4_x Bool)
108
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_5_x Int)
109
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_7_x Int)
110
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_8_x Int)
111
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_9_x Int)
112
(declare-var integrator_ext_reset_test.ni_0._arrow._first_x Bool)
113
(declare-var integrator_ext_reset_test.Integrator10_1_1 Int)
114
(declare-var integrator_ext_reset_test.Integrator10_Reset_Trigger1_1 Bool)
115
(declare-var integrator_ext_reset_test.Integrator11_1_1 Int)
116
(declare-var integrator_ext_reset_test.Integrator11_Reset_Trigger1_1 Bool)
117
(declare-var integrator_ext_reset_test.Integrator3_1_1 Real)
118
(declare-var integrator_ext_reset_test.Integrator3_Reset_Trigger1_1 Bool)
119
(declare-var integrator_ext_reset_test.Integrator4_1_1 Int)
120
(declare-var integrator_ext_reset_test.Integrator4_Reset_Trigger1_1 Bool)
121
(declare-var integrator_ext_reset_test.Integrator5_1_1 Int)
122
(declare-var integrator_ext_reset_test.Integrator5_Reset_Trigger1_1 Bool)
123
(declare-var integrator_ext_reset_test.Integrator6_1_1 Real)
124
(declare-var integrator_ext_reset_test.Integrator6_Reset_Trigger1_1 Bool)
125
(declare-var integrator_ext_reset_test.Integrator7_1_1 Int)
126
(declare-var integrator_ext_reset_test.Integrator7_Reset_Trigger1_1 Bool)
127
(declare-var integrator_ext_reset_test.Integrator8_1_1 Int)
128
(declare-var integrator_ext_reset_test.Integrator8_Reset_Trigger1_1 Bool)
129
(declare-var integrator_ext_reset_test.Integrator9_1_1 Real)
130
(declare-var integrator_ext_reset_test.Integrator9_Reset_Trigger1_1 Bool)
131
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_1 Bool)
132
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_16 Int)
133
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_26 Int)
134
(declare-var integrator_ext_reset_test.__integrator_ext_reset_test_6 Int)
135
(declare-var integrator_ext_reset_test.i_virtual_local Real)
136
(declare-rel integrator_ext_reset_test_reset (Int Int Real Real Int Int Int Real Int Real Int Real Real Real Real Int Int Bool Int Real Int Bool Bool Int Int Int Int Bool Int Int Real Real Int Int Int Real Int Real Int Real Real Real Real Int Int Bool Int Real Int Bool Bool Int Int Int Int Bool))
137
(declare-rel integrator_ext_reset_test_step (Real Int Bool Real Real Real Real Int Bool Int Int Int Real Int Bool Bool Bool Bool Real Int Int Real Int Int Real Int Int Int Int Real Real Int Int Int Real Int Real Int Real Real Real Real Int Int Bool Int Real Int Bool Bool Int Int Int Int Bool Int Int Real Real Int Int Int Real Int Real Int Real Real Real Real Int Int Bool Int Real Int Bool Bool Int Int Int Int Bool))
138

    
139
(rule (=> 
140
  (and 
141
       (= integrator_ext_reset_test.__integrator_ext_reset_test_10_m integrator_ext_reset_test.__integrator_ext_reset_test_10_c)
142
       (= integrator_ext_reset_test.__integrator_ext_reset_test_11_m integrator_ext_reset_test.__integrator_ext_reset_test_11_c)
143
       (= integrator_ext_reset_test.__integrator_ext_reset_test_12_m integrator_ext_reset_test.__integrator_ext_reset_test_12_c)
144
       (= integrator_ext_reset_test.__integrator_ext_reset_test_13_m integrator_ext_reset_test.__integrator_ext_reset_test_13_c)
145
       (= integrator_ext_reset_test.__integrator_ext_reset_test_14_m integrator_ext_reset_test.__integrator_ext_reset_test_14_c)
146
       (= integrator_ext_reset_test.__integrator_ext_reset_test_15_m integrator_ext_reset_test.__integrator_ext_reset_test_15_c)
147
       (= integrator_ext_reset_test.__integrator_ext_reset_test_17_m integrator_ext_reset_test.__integrator_ext_reset_test_17_c)
148
       (= integrator_ext_reset_test.__integrator_ext_reset_test_18_m integrator_ext_reset_test.__integrator_ext_reset_test_18_c)
149
       (= integrator_ext_reset_test.__integrator_ext_reset_test_19_m integrator_ext_reset_test.__integrator_ext_reset_test_19_c)
150
       (= integrator_ext_reset_test.__integrator_ext_reset_test_2_m integrator_ext_reset_test.__integrator_ext_reset_test_2_c)
151
       (= integrator_ext_reset_test.__integrator_ext_reset_test_20_m integrator_ext_reset_test.__integrator_ext_reset_test_20_c)
152
       (= integrator_ext_reset_test.__integrator_ext_reset_test_21_m integrator_ext_reset_test.__integrator_ext_reset_test_21_c)
153
       (= integrator_ext_reset_test.__integrator_ext_reset_test_22_m integrator_ext_reset_test.__integrator_ext_reset_test_22_c)
154
       (= integrator_ext_reset_test.__integrator_ext_reset_test_23_m integrator_ext_reset_test.__integrator_ext_reset_test_23_c)
155
       (= integrator_ext_reset_test.__integrator_ext_reset_test_24_m integrator_ext_reset_test.__integrator_ext_reset_test_24_c)
156
       (= integrator_ext_reset_test.__integrator_ext_reset_test_25_m integrator_ext_reset_test.__integrator_ext_reset_test_25_c)
157
       (= integrator_ext_reset_test.__integrator_ext_reset_test_27_m integrator_ext_reset_test.__integrator_ext_reset_test_27_c)
158
       (= integrator_ext_reset_test.__integrator_ext_reset_test_28_m integrator_ext_reset_test.__integrator_ext_reset_test_28_c)
159
       (= integrator_ext_reset_test.__integrator_ext_reset_test_29_m integrator_ext_reset_test.__integrator_ext_reset_test_29_c)
160
       (= integrator_ext_reset_test.__integrator_ext_reset_test_3_m integrator_ext_reset_test.__integrator_ext_reset_test_3_c)
161
       (= integrator_ext_reset_test.__integrator_ext_reset_test_30_m integrator_ext_reset_test.__integrator_ext_reset_test_30_c)
162
       (= integrator_ext_reset_test.__integrator_ext_reset_test_31_m integrator_ext_reset_test.__integrator_ext_reset_test_31_c)
163
       (= integrator_ext_reset_test.__integrator_ext_reset_test_4_m integrator_ext_reset_test.__integrator_ext_reset_test_4_c)
164
       (= integrator_ext_reset_test.__integrator_ext_reset_test_5_m integrator_ext_reset_test.__integrator_ext_reset_test_5_c)
165
       (= integrator_ext_reset_test.__integrator_ext_reset_test_7_m integrator_ext_reset_test.__integrator_ext_reset_test_7_c)
166
       (= integrator_ext_reset_test.__integrator_ext_reset_test_8_m integrator_ext_reset_test.__integrator_ext_reset_test_8_c)
167
       (= integrator_ext_reset_test.__integrator_ext_reset_test_9_m integrator_ext_reset_test.__integrator_ext_reset_test_9_c)
168
       (= integrator_ext_reset_test.ni_0._arrow._first_m true)
169
  )
170
  (integrator_ext_reset_test_reset integrator_ext_reset_test.__integrator_ext_reset_test_10_c
171
                                   integrator_ext_reset_test.__integrator_ext_reset_test_11_c
172
                                   integrator_ext_reset_test.__integrator_ext_reset_test_12_c
173
                                   integrator_ext_reset_test.__integrator_ext_reset_test_13_c
174
                                   integrator_ext_reset_test.__integrator_ext_reset_test_14_c
175
                                   integrator_ext_reset_test.__integrator_ext_reset_test_15_c
176
                                   integrator_ext_reset_test.__integrator_ext_reset_test_17_c
177
                                   integrator_ext_reset_test.__integrator_ext_reset_test_18_c
178
                                   integrator_ext_reset_test.__integrator_ext_reset_test_19_c
179
                                   integrator_ext_reset_test.__integrator_ext_reset_test_2_c
180
                                   integrator_ext_reset_test.__integrator_ext_reset_test_20_c
181
                                   integrator_ext_reset_test.__integrator_ext_reset_test_21_c
182
                                   integrator_ext_reset_test.__integrator_ext_reset_test_22_c
183
                                   integrator_ext_reset_test.__integrator_ext_reset_test_23_c
184
                                   integrator_ext_reset_test.__integrator_ext_reset_test_24_c
185
                                   integrator_ext_reset_test.__integrator_ext_reset_test_25_c
186
                                   integrator_ext_reset_test.__integrator_ext_reset_test_27_c
187
                                   integrator_ext_reset_test.__integrator_ext_reset_test_28_c
188
                                   integrator_ext_reset_test.__integrator_ext_reset_test_29_c
189
                                   integrator_ext_reset_test.__integrator_ext_reset_test_3_c
190
                                   integrator_ext_reset_test.__integrator_ext_reset_test_30_c
191
                                   integrator_ext_reset_test.__integrator_ext_reset_test_31_c
192
                                   integrator_ext_reset_test.__integrator_ext_reset_test_4_c
193
                                   integrator_ext_reset_test.__integrator_ext_reset_test_5_c
194
                                   integrator_ext_reset_test.__integrator_ext_reset_test_7_c
195
                                   integrator_ext_reset_test.__integrator_ext_reset_test_8_c
196
                                   integrator_ext_reset_test.__integrator_ext_reset_test_9_c
197
                                   integrator_ext_reset_test.ni_0._arrow._first_c
198
                                   integrator_ext_reset_test.__integrator_ext_reset_test_10_m
199
                                   integrator_ext_reset_test.__integrator_ext_reset_test_11_m
200
                                   integrator_ext_reset_test.__integrator_ext_reset_test_12_m
201
                                   integrator_ext_reset_test.__integrator_ext_reset_test_13_m
202
                                   integrator_ext_reset_test.__integrator_ext_reset_test_14_m
203
                                   integrator_ext_reset_test.__integrator_ext_reset_test_15_m
204
                                   integrator_ext_reset_test.__integrator_ext_reset_test_17_m
205
                                   integrator_ext_reset_test.__integrator_ext_reset_test_18_m
206
                                   integrator_ext_reset_test.__integrator_ext_reset_test_19_m
207
                                   integrator_ext_reset_test.__integrator_ext_reset_test_2_m
208
                                   integrator_ext_reset_test.__integrator_ext_reset_test_20_m
209
                                   integrator_ext_reset_test.__integrator_ext_reset_test_21_m
210
                                   integrator_ext_reset_test.__integrator_ext_reset_test_22_m
211
                                   integrator_ext_reset_test.__integrator_ext_reset_test_23_m
212
                                   integrator_ext_reset_test.__integrator_ext_reset_test_24_m
213
                                   integrator_ext_reset_test.__integrator_ext_reset_test_25_m
214
                                   integrator_ext_reset_test.__integrator_ext_reset_test_27_m
215
                                   integrator_ext_reset_test.__integrator_ext_reset_test_28_m
216
                                   integrator_ext_reset_test.__integrator_ext_reset_test_29_m
217
                                   integrator_ext_reset_test.__integrator_ext_reset_test_3_m
218
                                   integrator_ext_reset_test.__integrator_ext_reset_test_30_m
219
                                   integrator_ext_reset_test.__integrator_ext_reset_test_31_m
220
                                   integrator_ext_reset_test.__integrator_ext_reset_test_4_m
221
                                   integrator_ext_reset_test.__integrator_ext_reset_test_5_m
222
                                   integrator_ext_reset_test.__integrator_ext_reset_test_7_m
223
                                   integrator_ext_reset_test.__integrator_ext_reset_test_8_m
224
                                   integrator_ext_reset_test.__integrator_ext_reset_test_9_m
225
                                   integrator_ext_reset_test.ni_0._arrow._first_m)
226
))
227

    
228
(rule (=> 
229
  (and (= integrator_ext_reset_test.ni_0._arrow._first_m integrator_ext_reset_test.ni_0._arrow._first_c)
230
       (and (= integrator_ext_reset_test.__integrator_ext_reset_test_1 (ite integrator_ext_reset_test.ni_0._arrow._first_m true false))
231
            (= integrator_ext_reset_test.ni_0._arrow._first_x false))
232
       (and (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 false))
233
               (and (= integrator_ext_reset_test.i_virtual_local 1.0)
234
                    (= integrator_ext_reset_test.Integrator7_Reset_Trigger1_1 (and (<= integrator_ext_reset_test.__integrator_ext_reset_test_11_c 0) (> integrator_ext_reset_test.In14_1_1 0)))
235
                    (and (or (not (= integrator_ext_reset_test.Integrator7_Reset_Trigger1_1 true))
236
                            (= integrator_ext_reset_test.Integrator7_1_1 0))
237
                         (or (not (= integrator_ext_reset_test.Integrator7_Reset_Trigger1_1 false))
238
                            (= integrator_ext_reset_test.Integrator7_1_1 (+ (* (* 1 1) integrator_ext_reset_test.__integrator_ext_reset_test_10_c) integrator_ext_reset_test.__integrator_ext_reset_test_9_c)))
239
                    )
240
                    ))
241
            (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 true))
242
               (and (= integrator_ext_reset_test.i_virtual_local 0.0)
243
                    (= integrator_ext_reset_test.Integrator7_Reset_Trigger1_1 false)
244
                    (= integrator_ext_reset_test.Integrator7_1_1 0)
245
                    ))
246
       )
247
       (= integrator_ext_reset_test.__integrator_ext_reset_test_9_x integrator_ext_reset_test.Integrator7_1_1)
248
       (and (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 true))
249
               (= integrator_ext_reset_test.Integrator8_Reset_Trigger1_1 false))
250
            (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 false))
251
               (= integrator_ext_reset_test.Integrator8_Reset_Trigger1_1 (and (<= integrator_ext_reset_test.__integrator_ext_reset_test_8_c 0) (> integrator_ext_reset_test.In15_1_1 0))))
252
       )
253
       (= integrator_ext_reset_test.__integrator_ext_reset_test_8_x integrator_ext_reset_test.In15_1_1)
254
       (and (or (not (= integrator_ext_reset_test.In12_1_1 true))
255
               (= integrator_ext_reset_test.__integrator_ext_reset_test_6 1))
256
            (or (not (= integrator_ext_reset_test.In12_1_1 false))
257
               (= integrator_ext_reset_test.__integrator_ext_reset_test_6 0))
258
       )
259
       (and (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 true))
260
               (= integrator_ext_reset_test.Integrator8_1_1 0))
261
            (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 false))
262
               (and (or (not (= integrator_ext_reset_test.Integrator8_Reset_Trigger1_1 true))
263
                       (= integrator_ext_reset_test.Integrator8_1_1 0))
264
                    (or (not (= integrator_ext_reset_test.Integrator8_Reset_Trigger1_1 false))
265
                       (= integrator_ext_reset_test.Integrator8_1_1 (+ (* (* 1 1) integrator_ext_reset_test.__integrator_ext_reset_test_7_c) integrator_ext_reset_test.__integrator_ext_reset_test_5_c)))
266
               ))
267
       )
268
       (= integrator_ext_reset_test.__integrator_ext_reset_test_7_x integrator_ext_reset_test.__integrator_ext_reset_test_6)
269
       (= integrator_ext_reset_test.__integrator_ext_reset_test_5_x integrator_ext_reset_test.Integrator8_1_1)
270
       (and (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 true))
271
               (= integrator_ext_reset_test.Integrator9_Reset_Trigger1_1 false))
272
            (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 false))
273
               (= integrator_ext_reset_test.Integrator9_Reset_Trigger1_1 (and (not integrator_ext_reset_test.__integrator_ext_reset_test_4_c) integrator_ext_reset_test.In19_1_1)))
274
       )
275
       (= integrator_ext_reset_test.__integrator_ext_reset_test_4_x integrator_ext_reset_test.In19_1_1)
276
       (and (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 true))
277
               (= integrator_ext_reset_test.Integrator10_Reset_Trigger1_1 false))
278
            (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 false))
279
               (= integrator_ext_reset_test.Integrator10_Reset_Trigger1_1 (and (not integrator_ext_reset_test.__integrator_ext_reset_test_31_c) integrator_ext_reset_test.In20_1_1)))
280
       )
281
       (= integrator_ext_reset_test.__integrator_ext_reset_test_31_x integrator_ext_reset_test.In20_1_1)
282
       (and (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 true))
283
               (= integrator_ext_reset_test.Integrator10_1_1 0))
284
            (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 false))
285
               (and (or (not (= integrator_ext_reset_test.Integrator10_Reset_Trigger1_1 true))
286
                       (= integrator_ext_reset_test.Integrator10_1_1 0))
287
                    (or (not (= integrator_ext_reset_test.Integrator10_Reset_Trigger1_1 false))
288
                       (= integrator_ext_reset_test.Integrator10_1_1 (+ (* (* 1 1) integrator_ext_reset_test.__integrator_ext_reset_test_30_c) integrator_ext_reset_test.__integrator_ext_reset_test_29_c)))
289
               ))
290
       )
291
       (= integrator_ext_reset_test.__integrator_ext_reset_test_30_x integrator_ext_reset_test.In17_1_1)
292
       (and (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 true))
293
               (= integrator_ext_reset_test.Integrator9_1_1 0.00000000))
294
            (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 false))
295
               (and (or (not (= integrator_ext_reset_test.Integrator9_Reset_Trigger1_1 true))
296
                       (= integrator_ext_reset_test.Integrator9_1_1 0.00000000))
297
                    (or (not (= integrator_ext_reset_test.Integrator9_Reset_Trigger1_1 false))
298
                       (= integrator_ext_reset_test.Integrator9_1_1 (+ (* (* 1.00000000 1.00000000) integrator_ext_reset_test.__integrator_ext_reset_test_3_c) integrator_ext_reset_test.__integrator_ext_reset_test_2_c)))
299
               ))
300
       )
301
       (= integrator_ext_reset_test.__integrator_ext_reset_test_3_x integrator_ext_reset_test.In16_1_1)
302
       (= integrator_ext_reset_test.__integrator_ext_reset_test_29_x integrator_ext_reset_test.Integrator10_1_1)
303
       (and (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 true))
304
               (= integrator_ext_reset_test.Integrator11_Reset_Trigger1_1 false))
305
            (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 false))
306
               (= integrator_ext_reset_test.Integrator11_Reset_Trigger1_1 (and (not integrator_ext_reset_test.__integrator_ext_reset_test_28_c) integrator_ext_reset_test.In21_1_1)))
307
       )
308
       (= integrator_ext_reset_test.__integrator_ext_reset_test_28_x integrator_ext_reset_test.In21_1_1)
309
       (and (or (not (= integrator_ext_reset_test.In18_1_1 true))
310
               (= integrator_ext_reset_test.__integrator_ext_reset_test_26 1))
311
            (or (not (= integrator_ext_reset_test.In18_1_1 false))
312
               (= integrator_ext_reset_test.__integrator_ext_reset_test_26 0))
313
       )
314
       (and (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 true))
315
               (= integrator_ext_reset_test.Integrator11_1_1 0))
316
            (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 false))
317
               (and (or (not (= integrator_ext_reset_test.Integrator11_Reset_Trigger1_1 true))
318
                       (= integrator_ext_reset_test.Integrator11_1_1 0))
319
                    (or (not (= integrator_ext_reset_test.Integrator11_Reset_Trigger1_1 false))
320
                       (= integrator_ext_reset_test.Integrator11_1_1 (+ (* (* 1 1) integrator_ext_reset_test.__integrator_ext_reset_test_27_c) integrator_ext_reset_test.__integrator_ext_reset_test_25_c)))
321
               ))
322
       )
323
       (= integrator_ext_reset_test.__integrator_ext_reset_test_27_x integrator_ext_reset_test.__integrator_ext_reset_test_26)
324
       (= integrator_ext_reset_test.__integrator_ext_reset_test_25_x integrator_ext_reset_test.Integrator11_1_1)
325
       (and (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 true))
326
               (= integrator_ext_reset_test.Integrator3_Reset_Trigger1_1 false))
327
            (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 false))
328
               (= integrator_ext_reset_test.Integrator3_Reset_Trigger1_1 (and (<= integrator_ext_reset_test.__integrator_ext_reset_test_24_c 0.0) (> integrator_ext_reset_test.In7_1_1 0.0))))
329
       )
330
       (= integrator_ext_reset_test.__integrator_ext_reset_test_24_x integrator_ext_reset_test.In7_1_1)
331
       (and (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 true))
332
               (= integrator_ext_reset_test.Integrator3_1_1 0.00000000))
333
            (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 false))
334
               (and (or (not (= integrator_ext_reset_test.Integrator3_Reset_Trigger1_1 true))
335
                       (= integrator_ext_reset_test.Integrator3_1_1 0.00000000))
336
                    (or (not (= integrator_ext_reset_test.Integrator3_Reset_Trigger1_1 false))
337
                       (= integrator_ext_reset_test.Integrator3_1_1 (+ (* (* 1.00000000 1.00000000) integrator_ext_reset_test.__integrator_ext_reset_test_23_c) integrator_ext_reset_test.__integrator_ext_reset_test_22_c)))
338
               ))
339
       )
340
       (= integrator_ext_reset_test.__integrator_ext_reset_test_23_x integrator_ext_reset_test.In4_1_1)
341
       (= integrator_ext_reset_test.__integrator_ext_reset_test_22_x integrator_ext_reset_test.Integrator3_1_1)
342
       (and (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 true))
343
               (= integrator_ext_reset_test.Integrator4_Reset_Trigger1_1 false))
344
            (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 false))
345
               (= integrator_ext_reset_test.Integrator4_Reset_Trigger1_1 (and (<= integrator_ext_reset_test.__integrator_ext_reset_test_21_c 0.0) (> integrator_ext_reset_test.In8_1_1 0.0))))
346
       )
347
       (= integrator_ext_reset_test.__integrator_ext_reset_test_21_x integrator_ext_reset_test.In8_1_1)
348
       (and (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 true))
349
               (= integrator_ext_reset_test.Integrator4_1_1 0))
350
            (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 false))
351
               (and (or (not (= integrator_ext_reset_test.Integrator4_Reset_Trigger1_1 true))
352
                       (= integrator_ext_reset_test.Integrator4_1_1 0))
353
                    (or (not (= integrator_ext_reset_test.Integrator4_Reset_Trigger1_1 false))
354
                       (= integrator_ext_reset_test.Integrator4_1_1 (+ (* (* 1 1) integrator_ext_reset_test.__integrator_ext_reset_test_20_c) integrator_ext_reset_test.__integrator_ext_reset_test_19_c)))
355
               ))
356
       )
357
       (= integrator_ext_reset_test.__integrator_ext_reset_test_20_x integrator_ext_reset_test.In5_1_1)
358
       (= integrator_ext_reset_test.__integrator_ext_reset_test_2_x integrator_ext_reset_test.Integrator9_1_1)
359
       (= integrator_ext_reset_test.__integrator_ext_reset_test_19_x integrator_ext_reset_test.Integrator4_1_1)
360
       (and (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 true))
361
               (= integrator_ext_reset_test.Integrator5_Reset_Trigger1_1 false))
362
            (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 false))
363
               (= integrator_ext_reset_test.Integrator5_Reset_Trigger1_1 (and (<= integrator_ext_reset_test.__integrator_ext_reset_test_18_c 0.0) (> integrator_ext_reset_test.In9_1_1 0.0))))
364
       )
365
       (= integrator_ext_reset_test.__integrator_ext_reset_test_18_x integrator_ext_reset_test.In9_1_1)
366
       (and (or (not (= integrator_ext_reset_test.In6_1_1 true))
367
               (= integrator_ext_reset_test.__integrator_ext_reset_test_16 1))
368
            (or (not (= integrator_ext_reset_test.In6_1_1 false))
369
               (= integrator_ext_reset_test.__integrator_ext_reset_test_16 0))
370
       )
371
       (and (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 true))
372
               (= integrator_ext_reset_test.Integrator5_1_1 0))
373
            (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 false))
374
               (and (or (not (= integrator_ext_reset_test.Integrator5_Reset_Trigger1_1 true))
375
                       (= integrator_ext_reset_test.Integrator5_1_1 0))
376
                    (or (not (= integrator_ext_reset_test.Integrator5_Reset_Trigger1_1 false))
377
                       (= integrator_ext_reset_test.Integrator5_1_1 (+ (* (* 1 1) integrator_ext_reset_test.__integrator_ext_reset_test_17_c) integrator_ext_reset_test.__integrator_ext_reset_test_15_c)))
378
               ))
379
       )
380
       (= integrator_ext_reset_test.__integrator_ext_reset_test_17_x integrator_ext_reset_test.__integrator_ext_reset_test_16)
381
       (= integrator_ext_reset_test.__integrator_ext_reset_test_15_x integrator_ext_reset_test.Integrator5_1_1)
382
       (and (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 true))
383
               (= integrator_ext_reset_test.Integrator6_Reset_Trigger1_1 false))
384
            (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 false))
385
               (= integrator_ext_reset_test.Integrator6_Reset_Trigger1_1 (and (<= integrator_ext_reset_test.__integrator_ext_reset_test_14_c 0) (> integrator_ext_reset_test.In13_1_1 0))))
386
       )
387
       (= integrator_ext_reset_test.__integrator_ext_reset_test_14_x integrator_ext_reset_test.In13_1_1)
388
       (and (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 true))
389
               (= integrator_ext_reset_test.Integrator6_1_1 0.00000000))
390
            (or (not (= integrator_ext_reset_test.__integrator_ext_reset_test_1 false))
391
               (and (or (not (= integrator_ext_reset_test.Integrator6_Reset_Trigger1_1 true))
392
                       (= integrator_ext_reset_test.Integrator6_1_1 0.00000000))
393
                    (or (not (= integrator_ext_reset_test.Integrator6_Reset_Trigger1_1 false))
394
                       (= integrator_ext_reset_test.Integrator6_1_1 (+ (* (* 1.00000000 1.00000000) integrator_ext_reset_test.__integrator_ext_reset_test_13_c) integrator_ext_reset_test.__integrator_ext_reset_test_12_c)))
395
               ))
396
       )
397
       (= integrator_ext_reset_test.__integrator_ext_reset_test_13_x integrator_ext_reset_test.In10_1_1)
398
       (= integrator_ext_reset_test.__integrator_ext_reset_test_12_x integrator_ext_reset_test.Integrator6_1_1)
399
       (= integrator_ext_reset_test.__integrator_ext_reset_test_11_x integrator_ext_reset_test.In14_1_1)
400
       (= integrator_ext_reset_test.__integrator_ext_reset_test_10_x integrator_ext_reset_test.In11_1_1)
401
       (= integrator_ext_reset_test.Out9_6_1 integrator_ext_reset_test.Integrator8_1_1)
402
       (= integrator_ext_reset_test.Out8_5_1 integrator_ext_reset_test.Integrator7_1_1)
403
       (= integrator_ext_reset_test.Out7_4_1 integrator_ext_reset_test.Integrator6_1_1)
404
       (= integrator_ext_reset_test.Out6_3_1 integrator_ext_reset_test.Integrator5_1_1)
405
       (= integrator_ext_reset_test.Out5_2_1 integrator_ext_reset_test.Integrator4_1_1)
406
       (= integrator_ext_reset_test.Out4_1_1 integrator_ext_reset_test.Integrator3_1_1)
407
       (= integrator_ext_reset_test.Out12_9_1 integrator_ext_reset_test.Integrator11_1_1)
408
       (= integrator_ext_reset_test.Out11_8_1 integrator_ext_reset_test.Integrator10_1_1)
409
       (= integrator_ext_reset_test.Out10_7_1 integrator_ext_reset_test.Integrator9_1_1)
410
       )
411
  (integrator_ext_reset_test_step integrator_ext_reset_test.In4_1_1
412
                                  integrator_ext_reset_test.In5_1_1
413
                                  integrator_ext_reset_test.In6_1_1
414
                                  integrator_ext_reset_test.In7_1_1
415
                                  integrator_ext_reset_test.In8_1_1
416
                                  integrator_ext_reset_test.In9_1_1
417
                                  integrator_ext_reset_test.In10_1_1
418
                                  integrator_ext_reset_test.In11_1_1
419
                                  integrator_ext_reset_test.In12_1_1
420
                                  integrator_ext_reset_test.In13_1_1
421
                                  integrator_ext_reset_test.In14_1_1
422
                                  integrator_ext_reset_test.In15_1_1
423
                                  integrator_ext_reset_test.In16_1_1
424
                                  integrator_ext_reset_test.In17_1_1
425
                                  integrator_ext_reset_test.In18_1_1
426
                                  integrator_ext_reset_test.In19_1_1
427
                                  integrator_ext_reset_test.In20_1_1
428
                                  integrator_ext_reset_test.In21_1_1
429
                                  integrator_ext_reset_test.Out4_1_1
430
                                  integrator_ext_reset_test.Out5_2_1
431
                                  integrator_ext_reset_test.Out6_3_1
432
                                  integrator_ext_reset_test.Out7_4_1
433
                                  integrator_ext_reset_test.Out8_5_1
434
                                  integrator_ext_reset_test.Out9_6_1
435
                                  integrator_ext_reset_test.Out10_7_1
436
                                  integrator_ext_reset_test.Out11_8_1
437
                                  integrator_ext_reset_test.Out12_9_1
438
                                  integrator_ext_reset_test.__integrator_ext_reset_test_10_c
439
                                  integrator_ext_reset_test.__integrator_ext_reset_test_11_c
440
                                  integrator_ext_reset_test.__integrator_ext_reset_test_12_c
441
                                  integrator_ext_reset_test.__integrator_ext_reset_test_13_c
442
                                  integrator_ext_reset_test.__integrator_ext_reset_test_14_c
443
                                  integrator_ext_reset_test.__integrator_ext_reset_test_15_c
444
                                  integrator_ext_reset_test.__integrator_ext_reset_test_17_c
445
                                  integrator_ext_reset_test.__integrator_ext_reset_test_18_c
446
                                  integrator_ext_reset_test.__integrator_ext_reset_test_19_c
447
                                  integrator_ext_reset_test.__integrator_ext_reset_test_2_c
448
                                  integrator_ext_reset_test.__integrator_ext_reset_test_20_c
449
                                  integrator_ext_reset_test.__integrator_ext_reset_test_21_c
450
                                  integrator_ext_reset_test.__integrator_ext_reset_test_22_c
451
                                  integrator_ext_reset_test.__integrator_ext_reset_test_23_c
452
                                  integrator_ext_reset_test.__integrator_ext_reset_test_24_c
453
                                  integrator_ext_reset_test.__integrator_ext_reset_test_25_c
454
                                  integrator_ext_reset_test.__integrator_ext_reset_test_27_c
455
                                  integrator_ext_reset_test.__integrator_ext_reset_test_28_c
456
                                  integrator_ext_reset_test.__integrator_ext_reset_test_29_c
457
                                  integrator_ext_reset_test.__integrator_ext_reset_test_3_c
458
                                  integrator_ext_reset_test.__integrator_ext_reset_test_30_c
459
                                  integrator_ext_reset_test.__integrator_ext_reset_test_31_c
460
                                  integrator_ext_reset_test.__integrator_ext_reset_test_4_c
461
                                  integrator_ext_reset_test.__integrator_ext_reset_test_5_c
462
                                  integrator_ext_reset_test.__integrator_ext_reset_test_7_c
463
                                  integrator_ext_reset_test.__integrator_ext_reset_test_8_c
464
                                  integrator_ext_reset_test.__integrator_ext_reset_test_9_c
465
                                  integrator_ext_reset_test.ni_0._arrow._first_c
466
                                  integrator_ext_reset_test.__integrator_ext_reset_test_10_x
467
                                  integrator_ext_reset_test.__integrator_ext_reset_test_11_x
468
                                  integrator_ext_reset_test.__integrator_ext_reset_test_12_x
469
                                  integrator_ext_reset_test.__integrator_ext_reset_test_13_x
470
                                  integrator_ext_reset_test.__integrator_ext_reset_test_14_x
471
                                  integrator_ext_reset_test.__integrator_ext_reset_test_15_x
472
                                  integrator_ext_reset_test.__integrator_ext_reset_test_17_x
473
                                  integrator_ext_reset_test.__integrator_ext_reset_test_18_x
474
                                  integrator_ext_reset_test.__integrator_ext_reset_test_19_x
475
                                  integrator_ext_reset_test.__integrator_ext_reset_test_2_x
476
                                  integrator_ext_reset_test.__integrator_ext_reset_test_20_x
477
                                  integrator_ext_reset_test.__integrator_ext_reset_test_21_x
478
                                  integrator_ext_reset_test.__integrator_ext_reset_test_22_x
479
                                  integrator_ext_reset_test.__integrator_ext_reset_test_23_x
480
                                  integrator_ext_reset_test.__integrator_ext_reset_test_24_x
481
                                  integrator_ext_reset_test.__integrator_ext_reset_test_25_x
482
                                  integrator_ext_reset_test.__integrator_ext_reset_test_27_x
483
                                  integrator_ext_reset_test.__integrator_ext_reset_test_28_x
484
                                  integrator_ext_reset_test.__integrator_ext_reset_test_29_x
485
                                  integrator_ext_reset_test.__integrator_ext_reset_test_3_x
486
                                  integrator_ext_reset_test.__integrator_ext_reset_test_30_x
487
                                  integrator_ext_reset_test.__integrator_ext_reset_test_31_x
488
                                  integrator_ext_reset_test.__integrator_ext_reset_test_4_x
489
                                  integrator_ext_reset_test.__integrator_ext_reset_test_5_x
490
                                  integrator_ext_reset_test.__integrator_ext_reset_test_7_x
491
                                  integrator_ext_reset_test.__integrator_ext_reset_test_8_x
492
                                  integrator_ext_reset_test.__integrator_ext_reset_test_9_x
493
                                  integrator_ext_reset_test.ni_0._arrow._first_x)
494
))
495