Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_integrator_ext_reset_vector_test / integrator_ext_reset_vector_test.smt2 @ 6c3ea955

History | View | Annotate | Download (84.1 KB)

1
; integrator_ext_reset_vector_test
2
(declare-var integrator_ext_reset_vector_test.In4_1_1 Real)
3
(declare-var integrator_ext_reset_vector_test.In4_1_2 Real)
4
(declare-var integrator_ext_reset_vector_test.In7_1_1 Real)
5
(declare-var integrator_ext_reset_vector_test.In1_1_1 Real)
6
(declare-var integrator_ext_reset_vector_test.In2_1_1 Real)
7
(declare-var integrator_ext_reset_vector_test.In2_1_2 Real)
8
(declare-var integrator_ext_reset_vector_test.In3_1_1 Real)
9
(declare-var integrator_ext_reset_vector_test.In3_1_2 Real)
10
(declare-var integrator_ext_reset_vector_test.In5_1_1 Real)
11
(declare-var integrator_ext_reset_vector_test.In5_1_2 Real)
12
(declare-var integrator_ext_reset_vector_test.In6_1_1 Real)
13
(declare-var integrator_ext_reset_vector_test.In6_1_2 Real)
14
(declare-var integrator_ext_reset_vector_test.In8_1_1 Real)
15
(declare-var integrator_ext_reset_vector_test.In9_1_1 Real)
16
(declare-var integrator_ext_reset_vector_test.In10_1_1 Real)
17
(declare-var integrator_ext_reset_vector_test.In10_1_2 Real)
18
(declare-var integrator_ext_reset_vector_test.In11_1_1 Real)
19
(declare-var integrator_ext_reset_vector_test.In11_1_2 Real)
20
(declare-var integrator_ext_reset_vector_test.In12_1_1 Real)
21
(declare-var integrator_ext_reset_vector_test.In12_1_2 Real)
22
(declare-var integrator_ext_reset_vector_test.In13_1_1 Real)
23
(declare-var integrator_ext_reset_vector_test.In13_1_2 Real)
24
(declare-var integrator_ext_reset_vector_test.In14_1_1 Real)
25
(declare-var integrator_ext_reset_vector_test.In15_1_1 Real)
26
(declare-var integrator_ext_reset_vector_test.In16_1_1 Real)
27
(declare-var integrator_ext_reset_vector_test.In16_1_2 Real)
28
(declare-var integrator_ext_reset_vector_test.In17_1_1 Real)
29
(declare-var integrator_ext_reset_vector_test.In17_1_2 Real)
30
(declare-var integrator_ext_reset_vector_test.In18_1_1 Real)
31
(declare-var integrator_ext_reset_vector_test.In18_1_2 Real)
32
(declare-var integrator_ext_reset_vector_test.Out4_1_1 Real)
33
(declare-var integrator_ext_reset_vector_test.Out4_1_2 Real)
34
(declare-var integrator_ext_reset_vector_test.Out1_2_1 Real)
35
(declare-var integrator_ext_reset_vector_test.Out1_2_2 Real)
36
(declare-var integrator_ext_reset_vector_test.Out2_3_1 Real)
37
(declare-var integrator_ext_reset_vector_test.Out2_3_2 Real)
38
(declare-var integrator_ext_reset_vector_test.Out3_4_1 Real)
39
(declare-var integrator_ext_reset_vector_test.Out3_4_2 Real)
40
(declare-var integrator_ext_reset_vector_test.Out5_5_1 Real)
41
(declare-var integrator_ext_reset_vector_test.Out5_5_2 Real)
42
(declare-var integrator_ext_reset_vector_test.Out6_6_1 Real)
43
(declare-var integrator_ext_reset_vector_test.Out6_6_2 Real)
44
(declare-var integrator_ext_reset_vector_test.Out7_7_1 Real)
45
(declare-var integrator_ext_reset_vector_test.Out7_7_2 Real)
46
(declare-var integrator_ext_reset_vector_test.Out8_8_1 Real)
47
(declare-var integrator_ext_reset_vector_test.Out8_8_2 Real)
48
(declare-var integrator_ext_reset_vector_test.Out9_9_1 Real)
49
(declare-var integrator_ext_reset_vector_test.Out9_9_2 Real)
50
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_10_c Real)
51
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_11_c Real)
52
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_12_c Real)
53
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_13_c Real)
54
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_14_c Real)
55
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_15_c Real)
56
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_16_c Real)
57
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_17_c Real)
58
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_18_c Real)
59
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_19_c Real)
60
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_2_c Real)
61
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_20_c Real)
62
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_21_c Real)
63
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_22_c Real)
64
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_23_c Real)
65
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_24_c Real)
66
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_25_c Real)
67
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_26_c Real)
68
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_27_c Real)
69
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_28_c Real)
70
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_29_c Real)
71
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_3_c Real)
72
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_30_c Real)
73
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_31_c Real)
74
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_32_c Real)
75
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_33_c Real)
76
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_34_c Real)
77
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_35_c Real)
78
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_36_c Real)
79
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_37_c Real)
80
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_38_c Real)
81
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_39_c Real)
82
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_4_c Real)
83
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_40_c Real)
84
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_41_c Real)
85
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_42_c Real)
86
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_43_c Real)
87
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_44_c Real)
88
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_45_c Real)
89
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_46_c Real)
90
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_47_c Real)
91
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_48_c Real)
92
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_49_c Real)
93
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_5_c Real)
94
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_6_c Real)
95
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_7_c Real)
96
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_8_c Real)
97
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_9_c Real)
98
(declare-var integrator_ext_reset_vector_test.ni_0._arrow._first_c Bool)
99
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_10_m Real)
100
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_11_m Real)
101
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_12_m Real)
102
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_13_m Real)
103
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_14_m Real)
104
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_15_m Real)
105
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_16_m Real)
106
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_17_m Real)
107
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_18_m Real)
108
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_19_m Real)
109
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_2_m Real)
110
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_20_m Real)
111
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_21_m Real)
112
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_22_m Real)
113
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_23_m Real)
114
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_24_m Real)
115
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_25_m Real)
116
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_26_m Real)
117
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_27_m Real)
118
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_28_m Real)
119
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_29_m Real)
120
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_3_m Real)
121
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_30_m Real)
122
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_31_m Real)
123
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_32_m Real)
124
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_33_m Real)
125
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_34_m Real)
126
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_35_m Real)
127
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_36_m Real)
128
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_37_m Real)
129
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_38_m Real)
130
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_39_m Real)
131
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_4_m Real)
132
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_40_m Real)
133
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_41_m Real)
134
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_42_m Real)
135
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_43_m Real)
136
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_44_m Real)
137
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_45_m Real)
138
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_46_m Real)
139
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_47_m Real)
140
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_48_m Real)
141
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_49_m Real)
142
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_5_m Real)
143
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_6_m Real)
144
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_7_m Real)
145
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_8_m Real)
146
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_9_m Real)
147
(declare-var integrator_ext_reset_vector_test.ni_0._arrow._first_m Bool)
148
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_10_x Real)
149
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_11_x Real)
150
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_12_x Real)
151
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_13_x Real)
152
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_14_x Real)
153
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_15_x Real)
154
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_16_x Real)
155
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_17_x Real)
156
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_18_x Real)
157
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_19_x Real)
158
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_2_x Real)
159
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_20_x Real)
160
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_21_x Real)
161
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_22_x Real)
162
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_23_x Real)
163
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_24_x Real)
164
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_25_x Real)
165
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_26_x Real)
166
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_27_x Real)
167
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_28_x Real)
168
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_29_x Real)
169
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_3_x Real)
170
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_30_x Real)
171
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_31_x Real)
172
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_32_x Real)
173
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_33_x Real)
174
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_34_x Real)
175
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_35_x Real)
176
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_36_x Real)
177
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_37_x Real)
178
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_38_x Real)
179
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_39_x Real)
180
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_4_x Real)
181
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_40_x Real)
182
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_41_x Real)
183
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_42_x Real)
184
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_43_x Real)
185
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_44_x Real)
186
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_45_x Real)
187
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_46_x Real)
188
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_47_x Real)
189
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_48_x Real)
190
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_49_x Real)
191
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_5_x Real)
192
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_6_x Real)
193
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_7_x Real)
194
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_8_x Real)
195
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_9_x Real)
196
(declare-var integrator_ext_reset_vector_test.ni_0._arrow._first_x Bool)
197
(declare-var integrator_ext_reset_vector_test.Integrator1_1_1 Real)
198
(declare-var integrator_ext_reset_vector_test.Integrator1_1_2 Real)
199
(declare-var integrator_ext_reset_vector_test.Integrator1_Reset_Trigger1_1 Bool)
200
(declare-var integrator_ext_reset_vector_test.Integrator1_Reset_Trigger2_1 Bool)
201
(declare-var integrator_ext_reset_vector_test.Integrator2_1_1 Real)
202
(declare-var integrator_ext_reset_vector_test.Integrator2_1_2 Real)
203
(declare-var integrator_ext_reset_vector_test.Integrator2_Reset_Trigger1_1 Bool)
204
(declare-var integrator_ext_reset_vector_test.Integrator2_Reset_Trigger2_1 Bool)
205
(declare-var integrator_ext_reset_vector_test.Integrator3_1_1 Real)
206
(declare-var integrator_ext_reset_vector_test.Integrator3_1_2 Real)
207
(declare-var integrator_ext_reset_vector_test.Integrator3_Reset_Trigger1_1 Bool)
208
(declare-var integrator_ext_reset_vector_test.Integrator3_Reset_Trigger2_1 Bool)
209
(declare-var integrator_ext_reset_vector_test.Integrator4_1_1 Real)
210
(declare-var integrator_ext_reset_vector_test.Integrator4_1_2 Real)
211
(declare-var integrator_ext_reset_vector_test.Integrator4_Reset_Trigger1_1 Bool)
212
(declare-var integrator_ext_reset_vector_test.Integrator4_Reset_Trigger2_1 Bool)
213
(declare-var integrator_ext_reset_vector_test.Integrator5_1_1 Real)
214
(declare-var integrator_ext_reset_vector_test.Integrator5_1_2 Real)
215
(declare-var integrator_ext_reset_vector_test.Integrator5_Reset_Trigger1_1 Bool)
216
(declare-var integrator_ext_reset_vector_test.Integrator5_Reset_Trigger2_1 Bool)
217
(declare-var integrator_ext_reset_vector_test.Integrator6_1_1 Real)
218
(declare-var integrator_ext_reset_vector_test.Integrator6_1_2 Real)
219
(declare-var integrator_ext_reset_vector_test.Integrator6_Reset_Trigger1_1 Bool)
220
(declare-var integrator_ext_reset_vector_test.Integrator6_Reset_Trigger2_1 Bool)
221
(declare-var integrator_ext_reset_vector_test.Integrator7_1_1 Real)
222
(declare-var integrator_ext_reset_vector_test.Integrator7_1_2 Real)
223
(declare-var integrator_ext_reset_vector_test.Integrator7_Reset_Trigger1_1 Bool)
224
(declare-var integrator_ext_reset_vector_test.Integrator7_Reset_Trigger2_1 Bool)
225
(declare-var integrator_ext_reset_vector_test.Integrator8_1_1 Real)
226
(declare-var integrator_ext_reset_vector_test.Integrator8_1_2 Real)
227
(declare-var integrator_ext_reset_vector_test.Integrator8_Reset_Trigger1_1 Bool)
228
(declare-var integrator_ext_reset_vector_test.Integrator8_Reset_Trigger2_1 Bool)
229
(declare-var integrator_ext_reset_vector_test.Integrator_1_1 Real)
230
(declare-var integrator_ext_reset_vector_test.Integrator_1_2 Real)
231
(declare-var integrator_ext_reset_vector_test.Integrator_Reset_Trigger1_1 Bool)
232
(declare-var integrator_ext_reset_vector_test.Integrator_Reset_Trigger2_1 Bool)
233
(declare-var integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 Bool)
234
(declare-var integrator_ext_reset_vector_test.i_virtual_local Real)
235
(declare-rel integrator_ext_reset_vector_test_reset (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 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))
236
(declare-rel integrator_ext_reset_vector_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 Real Real Real Real Real Bool 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))
237

    
238
(rule (=> 
239
  (and 
240
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_10_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_10_c)
241
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_11_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_11_c)
242
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_12_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_12_c)
243
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_13_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_13_c)
244
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_14_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_14_c)
245
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_15_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_15_c)
246
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_16_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_16_c)
247
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_17_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_17_c)
248
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_18_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_18_c)
249
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_19_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_19_c)
250
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_2_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_2_c)
251
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_20_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_20_c)
252
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_21_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_21_c)
253
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_22_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_22_c)
254
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_23_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_23_c)
255
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_24_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_24_c)
256
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_25_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_25_c)
257
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_26_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_26_c)
258
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_27_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_27_c)
259
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_28_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_28_c)
260
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_29_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_29_c)
261
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_3_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_3_c)
262
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_30_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_30_c)
263
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_31_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_31_c)
264
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_32_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_32_c)
265
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_33_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_33_c)
266
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_34_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_34_c)
267
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_35_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_35_c)
268
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_36_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_36_c)
269
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_37_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_37_c)
270
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_38_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_38_c)
271
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_39_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_39_c)
272
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_4_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_4_c)
273
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_40_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_40_c)
274
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_41_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_41_c)
275
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_42_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_42_c)
276
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_43_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_43_c)
277
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_44_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_44_c)
278
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_45_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_45_c)
279
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_46_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_46_c)
280
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_47_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_47_c)
281
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_48_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_48_c)
282
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_49_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_49_c)
283
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_5_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_5_c)
284
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_6_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_6_c)
285
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_7_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_7_c)
286
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_8_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_8_c)
287
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_9_m integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_9_c)
288
       (= integrator_ext_reset_vector_test.ni_0._arrow._first_m true)
289
  )
290
  (integrator_ext_reset_vector_test_reset integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_10_c
291
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_11_c
292
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_12_c
293
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_13_c
294
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_14_c
295
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_15_c
296
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_16_c
297
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_17_c
298
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_18_c
299
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_19_c
300
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_2_c
301
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_20_c
302
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_21_c
303
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_22_c
304
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_23_c
305
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_24_c
306
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_25_c
307
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_26_c
308
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_27_c
309
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_28_c
310
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_29_c
311
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_3_c
312
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_30_c
313
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_31_c
314
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_32_c
315
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_33_c
316
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_34_c
317
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_35_c
318
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_36_c
319
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_37_c
320
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_38_c
321
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_39_c
322
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_4_c
323
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_40_c
324
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_41_c
325
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_42_c
326
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_43_c
327
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_44_c
328
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_45_c
329
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_46_c
330
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_47_c
331
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_48_c
332
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_49_c
333
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_5_c
334
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_6_c
335
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_7_c
336
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_8_c
337
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_9_c
338
                                          integrator_ext_reset_vector_test.ni_0._arrow._first_c
339
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_10_m
340
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_11_m
341
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_12_m
342
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_13_m
343
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_14_m
344
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_15_m
345
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_16_m
346
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_17_m
347
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_18_m
348
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_19_m
349
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_2_m
350
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_20_m
351
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_21_m
352
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_22_m
353
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_23_m
354
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_24_m
355
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_25_m
356
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_26_m
357
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_27_m
358
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_28_m
359
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_29_m
360
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_3_m
361
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_30_m
362
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_31_m
363
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_32_m
364
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_33_m
365
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_34_m
366
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_35_m
367
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_36_m
368
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_37_m
369
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_38_m
370
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_39_m
371
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_4_m
372
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_40_m
373
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_41_m
374
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_42_m
375
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_43_m
376
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_44_m
377
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_45_m
378
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_46_m
379
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_47_m
380
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_48_m
381
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_49_m
382
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_5_m
383
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_6_m
384
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_7_m
385
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_8_m
386
                                          integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_9_m
387
                                          integrator_ext_reset_vector_test.ni_0._arrow._first_m)
388
))
389

    
390
(rule (=> 
391
  (and (= integrator_ext_reset_vector_test.ni_0._arrow._first_m integrator_ext_reset_vector_test.ni_0._arrow._first_c)
392
       (and (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 (ite integrator_ext_reset_vector_test.ni_0._arrow._first_m true false))
393
            (= integrator_ext_reset_vector_test.ni_0._arrow._first_x false))
394
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
395
               (and (= integrator_ext_reset_vector_test.i_virtual_local 1.0)
396
                    (= integrator_ext_reset_vector_test.Integrator7_Reset_Trigger2_1 (and (<= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_10_c 0.0) (> integrator_ext_reset_vector_test.In16_1_2 0.0)))
397
                    (= integrator_ext_reset_vector_test.Integrator7_Reset_Trigger1_1 (and (<= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_12_c 0.0) (> integrator_ext_reset_vector_test.In16_1_1 0.0)))
398
                    (and (or (not (= integrator_ext_reset_vector_test.Integrator7_Reset_Trigger2_1 true))
399
                            (= integrator_ext_reset_vector_test.Integrator7_1_2 0.50000000))
400
                         (or (not (= integrator_ext_reset_vector_test.Integrator7_Reset_Trigger2_1 false))
401
                            (= integrator_ext_reset_vector_test.Integrator7_1_2 (+ (* (* 0.58900000 1.00000000) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_9_c) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_8_c)))
402
                    )
403
                    (and (or (not (= integrator_ext_reset_vector_test.Integrator7_Reset_Trigger1_1 true))
404
                            (= integrator_ext_reset_vector_test.Integrator7_1_1 2.00000000))
405
                         (or (not (= integrator_ext_reset_vector_test.Integrator7_Reset_Trigger1_1 false))
406
                            (= integrator_ext_reset_vector_test.Integrator7_1_1 (+ (* (* 0.25000000 1.00000000) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_9_c) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_11_c)))
407
                    )
408
                    ))
409
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
410
               (and (= integrator_ext_reset_vector_test.i_virtual_local 0.0)
411
                    (= integrator_ext_reset_vector_test.Integrator7_Reset_Trigger2_1 false)
412
                    (= integrator_ext_reset_vector_test.Integrator7_Reset_Trigger1_1 false)
413
                    (= integrator_ext_reset_vector_test.Integrator7_1_2 0.50000000)
414
                    (= integrator_ext_reset_vector_test.Integrator7_1_1 2.00000000)
415
                    ))
416
       )
417
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_9_x integrator_ext_reset_vector_test.In15_1_1)
418
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_8_x integrator_ext_reset_vector_test.Integrator7_1_2)
419
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
420
               (= integrator_ext_reset_vector_test.Integrator8_Reset_Trigger1_1 false))
421
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
422
               (= integrator_ext_reset_vector_test.Integrator8_Reset_Trigger1_1 (and (<= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_7_c 0.0) (> integrator_ext_reset_vector_test.In18_1_1 0.0))))
423
       )
424
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_7_x integrator_ext_reset_vector_test.In18_1_1)
425
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
426
               (= integrator_ext_reset_vector_test.Integrator8_1_1 2.00000000))
427
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
428
               (and (or (not (= integrator_ext_reset_vector_test.Integrator8_Reset_Trigger1_1 true))
429
                       (= integrator_ext_reset_vector_test.Integrator8_1_1 2.00000000))
430
                    (or (not (= integrator_ext_reset_vector_test.Integrator8_Reset_Trigger1_1 false))
431
                       (= integrator_ext_reset_vector_test.Integrator8_1_1 (+ (* (* 0.25000000 1.00000000) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_6_c) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_5_c)))
432
               ))
433
       )
434
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_6_x integrator_ext_reset_vector_test.In17_1_1)
435
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_5_x integrator_ext_reset_vector_test.Integrator8_1_1)
436
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
437
               (= integrator_ext_reset_vector_test.Integrator_Reset_Trigger2_1 false))
438
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
439
               (= integrator_ext_reset_vector_test.Integrator_Reset_Trigger2_1 (and (<= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_47_c 0.0) (> integrator_ext_reset_vector_test.In7_1_1 0.0))))
440
       )
441
       (= integrator_ext_reset_vector_test.Integrator_Reset_Trigger1_1 integrator_ext_reset_vector_test.Integrator_Reset_Trigger2_1)
442
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
443
               (= integrator_ext_reset_vector_test.Integrator_1_1 0.00000000))
444
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
445
               (and (or (not (= integrator_ext_reset_vector_test.Integrator_Reset_Trigger1_1 true))
446
                       (= integrator_ext_reset_vector_test.Integrator_1_1 0.00000000))
447
                    (or (not (= integrator_ext_reset_vector_test.Integrator_Reset_Trigger1_1 false))
448
                       (= integrator_ext_reset_vector_test.Integrator_1_1 (+ (* (* 1.00000000 1.00000000) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_49_c) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_48_c)))
449
               ))
450
       )
451
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_49_x integrator_ext_reset_vector_test.In4_1_1)
452
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_48_x integrator_ext_reset_vector_test.Integrator_1_1)
453
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_47_x integrator_ext_reset_vector_test.In7_1_1)
454
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
455
               (= integrator_ext_reset_vector_test.Integrator_1_2 0.00000000))
456
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
457
               (and (or (not (= integrator_ext_reset_vector_test.Integrator_Reset_Trigger2_1 true))
458
                       (= integrator_ext_reset_vector_test.Integrator_1_2 0.00000000))
459
                    (or (not (= integrator_ext_reset_vector_test.Integrator_Reset_Trigger2_1 false))
460
                       (= integrator_ext_reset_vector_test.Integrator_1_2 (+ (* (* 1.00000000 1.00000000) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_46_c) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_45_c)))
461
               ))
462
       )
463
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_46_x integrator_ext_reset_vector_test.In4_1_2)
464
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_45_x integrator_ext_reset_vector_test.Integrator_1_2)
465
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
466
               (= integrator_ext_reset_vector_test.Integrator1_Reset_Trigger1_1 false))
467
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
468
               (= integrator_ext_reset_vector_test.Integrator1_Reset_Trigger1_1 (and (<= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_44_c 0.0) (> integrator_ext_reset_vector_test.In2_1_1 0.0))))
469
       )
470
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_44_x integrator_ext_reset_vector_test.In2_1_1)
471
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
472
               (= integrator_ext_reset_vector_test.Integrator1_1_1 0.00000000))
473
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
474
               (and (or (not (= integrator_ext_reset_vector_test.Integrator1_Reset_Trigger1_1 true))
475
                       (= integrator_ext_reset_vector_test.Integrator1_1_1 0.00000000))
476
                    (or (not (= integrator_ext_reset_vector_test.Integrator1_Reset_Trigger1_1 false))
477
                       (= integrator_ext_reset_vector_test.Integrator1_1_1 (+ (* (* 1.00000000 1.00000000) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_41_c) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_43_c)))
478
               ))
479
       )
480
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_43_x integrator_ext_reset_vector_test.Integrator1_1_1)
481
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
482
               (= integrator_ext_reset_vector_test.Integrator1_Reset_Trigger2_1 false))
483
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
484
               (= integrator_ext_reset_vector_test.Integrator1_Reset_Trigger2_1 (and (<= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_42_c 0.0) (> integrator_ext_reset_vector_test.In2_1_2 0.0))))
485
       )
486
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_42_x integrator_ext_reset_vector_test.In2_1_2)
487
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
488
               (= integrator_ext_reset_vector_test.Integrator1_1_2 0.00000000))
489
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
490
               (and (or (not (= integrator_ext_reset_vector_test.Integrator1_Reset_Trigger2_1 true))
491
                       (= integrator_ext_reset_vector_test.Integrator1_1_2 0.00000000))
492
                    (or (not (= integrator_ext_reset_vector_test.Integrator1_Reset_Trigger2_1 false))
493
                       (= integrator_ext_reset_vector_test.Integrator1_1_2 (+ (* (* 1.00000000 1.00000000) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_41_c) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_40_c)))
494
               ))
495
       )
496
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_41_x integrator_ext_reset_vector_test.In1_1_1)
497
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_40_x integrator_ext_reset_vector_test.Integrator1_1_2)
498
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
499
               (= integrator_ext_reset_vector_test.Integrator8_Reset_Trigger2_1 false))
500
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
501
               (= integrator_ext_reset_vector_test.Integrator8_Reset_Trigger2_1 (and (<= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_4_c 0.0) (> integrator_ext_reset_vector_test.In18_1_2 0.0))))
502
       )
503
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_4_x integrator_ext_reset_vector_test.In18_1_2)
504
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
505
               (= integrator_ext_reset_vector_test.Integrator2_Reset_Trigger1_1 false))
506
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
507
               (= integrator_ext_reset_vector_test.Integrator2_Reset_Trigger1_1 (and (<= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_39_c 0.0) (> integrator_ext_reset_vector_test.In5_1_1 0.0))))
508
       )
509
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_39_x integrator_ext_reset_vector_test.In5_1_1)
510
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
511
               (= integrator_ext_reset_vector_test.Integrator2_1_1 0.00000000))
512
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
513
               (and (or (not (= integrator_ext_reset_vector_test.Integrator2_Reset_Trigger1_1 true))
514
                       (= integrator_ext_reset_vector_test.Integrator2_1_1 0.00000000))
515
                    (or (not (= integrator_ext_reset_vector_test.Integrator2_Reset_Trigger1_1 false))
516
                       (= integrator_ext_reset_vector_test.Integrator2_1_1 (+ (* (* 1.00000000 1.00000000) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_38_c) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_37_c)))
517
               ))
518
       )
519
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_38_x integrator_ext_reset_vector_test.In3_1_1)
520
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_37_x integrator_ext_reset_vector_test.Integrator2_1_1)
521
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
522
               (= integrator_ext_reset_vector_test.Integrator2_Reset_Trigger2_1 false))
523
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
524
               (= integrator_ext_reset_vector_test.Integrator2_Reset_Trigger2_1 (and (<= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_36_c 0.0) (> integrator_ext_reset_vector_test.In5_1_2 0.0))))
525
       )
526
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_36_x integrator_ext_reset_vector_test.In5_1_2)
527
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
528
               (= integrator_ext_reset_vector_test.Integrator2_1_2 0.00000000))
529
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
530
               (and (or (not (= integrator_ext_reset_vector_test.Integrator2_Reset_Trigger2_1 true))
531
                       (= integrator_ext_reset_vector_test.Integrator2_1_2 0.00000000))
532
                    (or (not (= integrator_ext_reset_vector_test.Integrator2_Reset_Trigger2_1 false))
533
                       (= integrator_ext_reset_vector_test.Integrator2_1_2 (+ (* (* 1.00000000 1.00000000) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_35_c) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_34_c)))
534
               ))
535
       )
536
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_35_x integrator_ext_reset_vector_test.In3_1_2)
537
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_34_x integrator_ext_reset_vector_test.Integrator2_1_2)
538
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
539
               (= integrator_ext_reset_vector_test.Integrator3_Reset_Trigger2_1 false))
540
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
541
               (= integrator_ext_reset_vector_test.Integrator3_Reset_Trigger2_1 (and (<= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_31_c 0.0) (> integrator_ext_reset_vector_test.In8_1_1 0.0))))
542
       )
543
       (= integrator_ext_reset_vector_test.Integrator3_Reset_Trigger1_1 integrator_ext_reset_vector_test.Integrator3_Reset_Trigger2_1)
544
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
545
               (= integrator_ext_reset_vector_test.Integrator3_1_1 2.00000000))
546
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
547
               (and (or (not (= integrator_ext_reset_vector_test.Integrator3_Reset_Trigger1_1 true))
548
                       (= integrator_ext_reset_vector_test.Integrator3_1_1 2.00000000))
549
                    (or (not (= integrator_ext_reset_vector_test.Integrator3_Reset_Trigger1_1 false))
550
                       (= integrator_ext_reset_vector_test.Integrator3_1_1 (+ (* (* 1.00000000 1.00000000) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_33_c) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_32_c)))
551
               ))
552
       )
553
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_33_x integrator_ext_reset_vector_test.In6_1_1)
554
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_32_x integrator_ext_reset_vector_test.Integrator3_1_1)
555
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_31_x integrator_ext_reset_vector_test.In8_1_1)
556
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
557
               (= integrator_ext_reset_vector_test.Integrator3_1_2 0.50000000))
558
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
559
               (and (or (not (= integrator_ext_reset_vector_test.Integrator3_Reset_Trigger2_1 true))
560
                       (= integrator_ext_reset_vector_test.Integrator3_1_2 0.50000000))
561
                    (or (not (= integrator_ext_reset_vector_test.Integrator3_Reset_Trigger2_1 false))
562
                       (= integrator_ext_reset_vector_test.Integrator3_1_2 (+ (* (* 1.00000000 1.00000000) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_30_c) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_29_c)))
563
               ))
564
       )
565
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_30_x integrator_ext_reset_vector_test.In6_1_2)
566
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
567
               (= integrator_ext_reset_vector_test.Integrator8_1_2 0.50000000))
568
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
569
               (and (or (not (= integrator_ext_reset_vector_test.Integrator8_Reset_Trigger2_1 true))
570
                       (= integrator_ext_reset_vector_test.Integrator8_1_2 0.50000000))
571
                    (or (not (= integrator_ext_reset_vector_test.Integrator8_Reset_Trigger2_1 false))
572
                       (= integrator_ext_reset_vector_test.Integrator8_1_2 (+ (* (* 0.58900000 1.00000000) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_3_c) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_2_c)))
573
               ))
574
       )
575
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_3_x integrator_ext_reset_vector_test.In17_1_2)
576
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_29_x integrator_ext_reset_vector_test.Integrator3_1_2)
577
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
578
               (= integrator_ext_reset_vector_test.Integrator4_Reset_Trigger1_1 false))
579
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
580
               (= integrator_ext_reset_vector_test.Integrator4_Reset_Trigger1_1 (and (<= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_28_c 0.0) (> integrator_ext_reset_vector_test.In10_1_1 0.0))))
581
       )
582
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_28_x integrator_ext_reset_vector_test.In10_1_1)
583
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
584
               (= integrator_ext_reset_vector_test.Integrator4_1_1 2.00000000))
585
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
586
               (and (or (not (= integrator_ext_reset_vector_test.Integrator4_Reset_Trigger1_1 true))
587
                       (= integrator_ext_reset_vector_test.Integrator4_1_1 2.00000000))
588
                    (or (not (= integrator_ext_reset_vector_test.Integrator4_Reset_Trigger1_1 false))
589
                       (= integrator_ext_reset_vector_test.Integrator4_1_1 (+ (* (* 1.00000000 1.00000000) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_25_c) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_27_c)))
590
               ))
591
       )
592
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_27_x integrator_ext_reset_vector_test.Integrator4_1_1)
593
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
594
               (= integrator_ext_reset_vector_test.Integrator4_Reset_Trigger2_1 false))
595
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
596
               (= integrator_ext_reset_vector_test.Integrator4_Reset_Trigger2_1 (and (<= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_26_c 0.0) (> integrator_ext_reset_vector_test.In10_1_2 0.0))))
597
       )
598
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_26_x integrator_ext_reset_vector_test.In10_1_2)
599
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
600
               (= integrator_ext_reset_vector_test.Integrator4_1_2 0.50000000))
601
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
602
               (and (or (not (= integrator_ext_reset_vector_test.Integrator4_Reset_Trigger2_1 true))
603
                       (= integrator_ext_reset_vector_test.Integrator4_1_2 0.50000000))
604
                    (or (not (= integrator_ext_reset_vector_test.Integrator4_Reset_Trigger2_1 false))
605
                       (= integrator_ext_reset_vector_test.Integrator4_1_2 (+ (* (* 1.00000000 1.00000000) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_25_c) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_24_c)))
606
               ))
607
       )
608
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_25_x integrator_ext_reset_vector_test.In9_1_1)
609
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_24_x integrator_ext_reset_vector_test.Integrator4_1_2)
610
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
611
               (= integrator_ext_reset_vector_test.Integrator5_Reset_Trigger1_1 false))
612
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
613
               (= integrator_ext_reset_vector_test.Integrator5_Reset_Trigger1_1 (and (<= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_23_c 0.0) (> integrator_ext_reset_vector_test.In12_1_1 0.0))))
614
       )
615
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_23_x integrator_ext_reset_vector_test.In12_1_1)
616
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
617
               (= integrator_ext_reset_vector_test.Integrator5_1_1 2.00000000))
618
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
619
               (and (or (not (= integrator_ext_reset_vector_test.Integrator5_Reset_Trigger1_1 true))
620
                       (= integrator_ext_reset_vector_test.Integrator5_1_1 2.00000000))
621
                    (or (not (= integrator_ext_reset_vector_test.Integrator5_Reset_Trigger1_1 false))
622
                       (= integrator_ext_reset_vector_test.Integrator5_1_1 (+ (* (* 1.00000000 1.00000000) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_22_c) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_21_c)))
623
               ))
624
       )
625
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_22_x integrator_ext_reset_vector_test.In11_1_1)
626
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_21_x integrator_ext_reset_vector_test.Integrator5_1_1)
627
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
628
               (= integrator_ext_reset_vector_test.Integrator5_Reset_Trigger2_1 false))
629
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
630
               (= integrator_ext_reset_vector_test.Integrator5_Reset_Trigger2_1 (and (<= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_20_c 0.0) (> integrator_ext_reset_vector_test.In12_1_2 0.0))))
631
       )
632
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_20_x integrator_ext_reset_vector_test.In12_1_2)
633
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_2_x integrator_ext_reset_vector_test.Integrator8_1_2)
634
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
635
               (= integrator_ext_reset_vector_test.Integrator5_1_2 0.50000000))
636
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
637
               (and (or (not (= integrator_ext_reset_vector_test.Integrator5_Reset_Trigger2_1 true))
638
                       (= integrator_ext_reset_vector_test.Integrator5_1_2 0.50000000))
639
                    (or (not (= integrator_ext_reset_vector_test.Integrator5_Reset_Trigger2_1 false))
640
                       (= integrator_ext_reset_vector_test.Integrator5_1_2 (+ (* (* 1.00000000 1.00000000) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_19_c) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_18_c)))
641
               ))
642
       )
643
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_19_x integrator_ext_reset_vector_test.In11_1_2)
644
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_18_x integrator_ext_reset_vector_test.Integrator5_1_2)
645
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
646
               (= integrator_ext_reset_vector_test.Integrator6_Reset_Trigger2_1 false))
647
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
648
               (= integrator_ext_reset_vector_test.Integrator6_Reset_Trigger2_1 (and (<= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_15_c 0.0) (> integrator_ext_reset_vector_test.In14_1_1 0.0))))
649
       )
650
       (= integrator_ext_reset_vector_test.Integrator6_Reset_Trigger1_1 integrator_ext_reset_vector_test.Integrator6_Reset_Trigger2_1)
651
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
652
               (= integrator_ext_reset_vector_test.Integrator6_1_1 2.00000000))
653
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
654
               (and (or (not (= integrator_ext_reset_vector_test.Integrator6_Reset_Trigger1_1 true))
655
                       (= integrator_ext_reset_vector_test.Integrator6_1_1 2.00000000))
656
                    (or (not (= integrator_ext_reset_vector_test.Integrator6_Reset_Trigger1_1 false))
657
                       (= integrator_ext_reset_vector_test.Integrator6_1_1 (+ (* (* 0.25000000 1.00000000) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_17_c) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_16_c)))
658
               ))
659
       )
660
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_17_x integrator_ext_reset_vector_test.In13_1_1)
661
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_16_x integrator_ext_reset_vector_test.Integrator6_1_1)
662
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_15_x integrator_ext_reset_vector_test.In14_1_1)
663
       (and (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 true))
664
               (= integrator_ext_reset_vector_test.Integrator6_1_2 0.50000000))
665
            (or (not (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_1 false))
666
               (and (or (not (= integrator_ext_reset_vector_test.Integrator6_Reset_Trigger2_1 true))
667
                       (= integrator_ext_reset_vector_test.Integrator6_1_2 0.50000000))
668
                    (or (not (= integrator_ext_reset_vector_test.Integrator6_Reset_Trigger2_1 false))
669
                       (= integrator_ext_reset_vector_test.Integrator6_1_2 (+ (* (* 0.58900000 1.00000000) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_14_c) integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_13_c)))
670
               ))
671
       )
672
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_14_x integrator_ext_reset_vector_test.In13_1_2)
673
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_13_x integrator_ext_reset_vector_test.Integrator6_1_2)
674
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_12_x integrator_ext_reset_vector_test.In16_1_1)
675
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_11_x integrator_ext_reset_vector_test.Integrator7_1_1)
676
       (= integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_10_x integrator_ext_reset_vector_test.In16_1_2)
677
       (= integrator_ext_reset_vector_test.Out9_9_2 integrator_ext_reset_vector_test.Integrator8_1_2)
678
       (= integrator_ext_reset_vector_test.Out9_9_1 integrator_ext_reset_vector_test.Integrator8_1_1)
679
       (= integrator_ext_reset_vector_test.Out8_8_2 integrator_ext_reset_vector_test.Integrator7_1_2)
680
       (= integrator_ext_reset_vector_test.Out8_8_1 integrator_ext_reset_vector_test.Integrator7_1_1)
681
       (= integrator_ext_reset_vector_test.Out7_7_2 integrator_ext_reset_vector_test.Integrator6_1_2)
682
       (= integrator_ext_reset_vector_test.Out7_7_1 integrator_ext_reset_vector_test.Integrator6_1_1)
683
       (= integrator_ext_reset_vector_test.Out6_6_2 integrator_ext_reset_vector_test.Integrator5_1_2)
684
       (= integrator_ext_reset_vector_test.Out6_6_1 integrator_ext_reset_vector_test.Integrator5_1_1)
685
       (= integrator_ext_reset_vector_test.Out5_5_2 integrator_ext_reset_vector_test.Integrator4_1_2)
686
       (= integrator_ext_reset_vector_test.Out5_5_1 integrator_ext_reset_vector_test.Integrator4_1_1)
687
       (= integrator_ext_reset_vector_test.Out4_1_2 integrator_ext_reset_vector_test.Integrator_1_2)
688
       (= integrator_ext_reset_vector_test.Out4_1_1 integrator_ext_reset_vector_test.Integrator_1_1)
689
       (= integrator_ext_reset_vector_test.Out3_4_2 integrator_ext_reset_vector_test.Integrator3_1_2)
690
       (= integrator_ext_reset_vector_test.Out3_4_1 integrator_ext_reset_vector_test.Integrator3_1_1)
691
       (= integrator_ext_reset_vector_test.Out2_3_2 integrator_ext_reset_vector_test.Integrator2_1_2)
692
       (= integrator_ext_reset_vector_test.Out2_3_1 integrator_ext_reset_vector_test.Integrator2_1_1)
693
       (= integrator_ext_reset_vector_test.Out1_2_2 integrator_ext_reset_vector_test.Integrator1_1_2)
694
       (= integrator_ext_reset_vector_test.Out1_2_1 integrator_ext_reset_vector_test.Integrator1_1_1)
695
       )
696
  (integrator_ext_reset_vector_test_step integrator_ext_reset_vector_test.In4_1_1
697
                                         integrator_ext_reset_vector_test.In4_1_2
698
                                         integrator_ext_reset_vector_test.In7_1_1
699
                                         integrator_ext_reset_vector_test.In1_1_1
700
                                         integrator_ext_reset_vector_test.In2_1_1
701
                                         integrator_ext_reset_vector_test.In2_1_2
702
                                         integrator_ext_reset_vector_test.In3_1_1
703
                                         integrator_ext_reset_vector_test.In3_1_2
704
                                         integrator_ext_reset_vector_test.In5_1_1
705
                                         integrator_ext_reset_vector_test.In5_1_2
706
                                         integrator_ext_reset_vector_test.In6_1_1
707
                                         integrator_ext_reset_vector_test.In6_1_2
708
                                         integrator_ext_reset_vector_test.In8_1_1
709
                                         integrator_ext_reset_vector_test.In9_1_1
710
                                         integrator_ext_reset_vector_test.In10_1_1
711
                                         integrator_ext_reset_vector_test.In10_1_2
712
                                         integrator_ext_reset_vector_test.In11_1_1
713
                                         integrator_ext_reset_vector_test.In11_1_2
714
                                         integrator_ext_reset_vector_test.In12_1_1
715
                                         integrator_ext_reset_vector_test.In12_1_2
716
                                         integrator_ext_reset_vector_test.In13_1_1
717
                                         integrator_ext_reset_vector_test.In13_1_2
718
                                         integrator_ext_reset_vector_test.In14_1_1
719
                                         integrator_ext_reset_vector_test.In15_1_1
720
                                         integrator_ext_reset_vector_test.In16_1_1
721
                                         integrator_ext_reset_vector_test.In16_1_2
722
                                         integrator_ext_reset_vector_test.In17_1_1
723
                                         integrator_ext_reset_vector_test.In17_1_2
724
                                         integrator_ext_reset_vector_test.In18_1_1
725
                                         integrator_ext_reset_vector_test.In18_1_2
726
                                         integrator_ext_reset_vector_test.Out4_1_1
727
                                         integrator_ext_reset_vector_test.Out4_1_2
728
                                         integrator_ext_reset_vector_test.Out1_2_1
729
                                         integrator_ext_reset_vector_test.Out1_2_2
730
                                         integrator_ext_reset_vector_test.Out2_3_1
731
                                         integrator_ext_reset_vector_test.Out2_3_2
732
                                         integrator_ext_reset_vector_test.Out3_4_1
733
                                         integrator_ext_reset_vector_test.Out3_4_2
734
                                         integrator_ext_reset_vector_test.Out5_5_1
735
                                         integrator_ext_reset_vector_test.Out5_5_2
736
                                         integrator_ext_reset_vector_test.Out6_6_1
737
                                         integrator_ext_reset_vector_test.Out6_6_2
738
                                         integrator_ext_reset_vector_test.Out7_7_1
739
                                         integrator_ext_reset_vector_test.Out7_7_2
740
                                         integrator_ext_reset_vector_test.Out8_8_1
741
                                         integrator_ext_reset_vector_test.Out8_8_2
742
                                         integrator_ext_reset_vector_test.Out9_9_1
743
                                         integrator_ext_reset_vector_test.Out9_9_2
744
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_10_c
745
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_11_c
746
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_12_c
747
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_13_c
748
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_14_c
749
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_15_c
750
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_16_c
751
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_17_c
752
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_18_c
753
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_19_c
754
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_2_c
755
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_20_c
756
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_21_c
757
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_22_c
758
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_23_c
759
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_24_c
760
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_25_c
761
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_26_c
762
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_27_c
763
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_28_c
764
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_29_c
765
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_3_c
766
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_30_c
767
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_31_c
768
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_32_c
769
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_33_c
770
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_34_c
771
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_35_c
772
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_36_c
773
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_37_c
774
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_38_c
775
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_39_c
776
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_4_c
777
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_40_c
778
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_41_c
779
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_42_c
780
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_43_c
781
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_44_c
782
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_45_c
783
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_46_c
784
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_47_c
785
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_48_c
786
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_49_c
787
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_5_c
788
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_6_c
789
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_7_c
790
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_8_c
791
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_9_c
792
                                         integrator_ext_reset_vector_test.ni_0._arrow._first_c
793
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_10_x
794
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_11_x
795
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_12_x
796
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_13_x
797
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_14_x
798
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_15_x
799
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_16_x
800
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_17_x
801
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_18_x
802
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_19_x
803
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_2_x
804
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_20_x
805
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_21_x
806
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_22_x
807
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_23_x
808
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_24_x
809
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_25_x
810
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_26_x
811
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_27_x
812
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_28_x
813
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_29_x
814
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_3_x
815
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_30_x
816
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_31_x
817
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_32_x
818
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_33_x
819
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_34_x
820
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_35_x
821
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_36_x
822
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_37_x
823
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_38_x
824
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_39_x
825
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_4_x
826
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_40_x
827
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_41_x
828
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_42_x
829
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_43_x
830
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_44_x
831
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_45_x
832
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_46_x
833
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_47_x
834
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_48_x
835
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_49_x
836
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_5_x
837
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_6_x
838
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_7_x
839
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_8_x
840
                                         integrator_ext_reset_vector_test.__integrator_ext_reset_vector_test_9_x
841
                                         integrator_ext_reset_vector_test.ni_0._arrow._first_x)
842
))
843