Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_saturate_test / saturate_test.smt2 @ 6c3ea955

History | View | Annotate | Download (37.6 KB)

1
; saturate_test
2
(declare-var saturate_test.In1_1_1 Real)
3
(declare-var saturate_test.In2_1_1 Real)
4
(declare-var saturate_test.In2_1_2 Real)
5
(declare-var saturate_test.In2_1_3 Real)
6
(declare-var saturate_test.In3_1_1 Real)
7
(declare-var saturate_test.In3_1_2 Real)
8
(declare-var saturate_test.In3_1_3 Real)
9
(declare-var saturate_test.In3_1_4 Real)
10
(declare-var saturate_test.In3_1_5 Real)
11
(declare-var saturate_test.In3_1_6 Real)
12
(declare-var saturate_test.In4_1_1 Real)
13
(declare-var saturate_test.In4_1_2 Real)
14
(declare-var saturate_test.In4_1_3 Real)
15
(declare-var saturate_test.In5_1_1 Real)
16
(declare-var saturate_test.In5_1_2 Real)
17
(declare-var saturate_test.In5_1_3 Real)
18
(declare-var saturate_test.In5_1_4 Real)
19
(declare-var saturate_test.In5_1_5 Real)
20
(declare-var saturate_test.In5_1_6 Real)
21
(declare-var saturate_test.In6_1_1 Real)
22
(declare-var saturate_test.In7_1_1 Real)
23
(declare-var saturate_test.In8_1_1 Real)
24
(declare-var saturate_test.In9_1_1 Real)
25
(declare-var saturate_test.Out1_1_1 Real)
26
(declare-var saturate_test.Out2_2_1 Real)
27
(declare-var saturate_test.Out2_2_2 Real)
28
(declare-var saturate_test.Out2_2_3 Real)
29
(declare-var saturate_test.Out3_3_1 Real)
30
(declare-var saturate_test.Out3_3_2 Real)
31
(declare-var saturate_test.Out3_3_3 Real)
32
(declare-var saturate_test.Out3_3_4 Real)
33
(declare-var saturate_test.Out3_3_5 Real)
34
(declare-var saturate_test.Out3_3_6 Real)
35
(declare-var saturate_test.Out4_4_1 Real)
36
(declare-var saturate_test.Out4_4_2 Real)
37
(declare-var saturate_test.Out4_4_3 Real)
38
(declare-var saturate_test.Out5_5_1 Real)
39
(declare-var saturate_test.Out5_5_2 Real)
40
(declare-var saturate_test.Out5_5_3 Real)
41
(declare-var saturate_test.Out5_5_4 Real)
42
(declare-var saturate_test.Out5_5_5 Real)
43
(declare-var saturate_test.Out5_5_6 Real)
44
(declare-var saturate_test.Out6_6_1 Real)
45
(declare-var saturate_test.Out6_6_2 Real)
46
(declare-var saturate_test.Out6_6_3 Real)
47
(declare-var saturate_test.Out7_7_1 Real)
48
(declare-var saturate_test.Out7_7_2 Real)
49
(declare-var saturate_test.Out7_7_3 Real)
50
(declare-var saturate_test.Out7_7_4 Real)
51
(declare-var saturate_test.Out7_7_5 Real)
52
(declare-var saturate_test.Out7_7_6 Real)
53
(declare-var saturate_test.Out8_8_1 Real)
54
(declare-var saturate_test.Out8_8_2 Real)
55
(declare-var saturate_test.Out8_8_3 Real)
56
(declare-var saturate_test.Out9_9_1 Real)
57
(declare-var saturate_test.Out9_9_2 Real)
58
(declare-var saturate_test.Out9_9_3 Real)
59
(declare-var saturate_test.Out9_9_4 Real)
60
(declare-var saturate_test.Out9_9_5 Real)
61
(declare-var saturate_test.Out9_9_6 Real)
62
(declare-var saturate_test.ni_0._arrow._first_c Bool)
63
(declare-var saturate_test.ni_0._arrow._first_m Bool)
64
(declare-var saturate_test.ni_0._arrow._first_x Bool)
65
(declare-var saturate_test.Saturation1_1_1 Real)
66
(declare-var saturate_test.Saturation1_1_2 Real)
67
(declare-var saturate_test.Saturation1_1_3 Real)
68
(declare-var saturate_test.Saturation2_1_1 Real)
69
(declare-var saturate_test.Saturation2_1_2 Real)
70
(declare-var saturate_test.Saturation2_1_3 Real)
71
(declare-var saturate_test.Saturation2_1_4 Real)
72
(declare-var saturate_test.Saturation2_1_5 Real)
73
(declare-var saturate_test.Saturation2_1_6 Real)
74
(declare-var saturate_test.Saturation3_1_1 Real)
75
(declare-var saturate_test.Saturation3_1_2 Real)
76
(declare-var saturate_test.Saturation3_1_3 Real)
77
(declare-var saturate_test.Saturation4_1_1 Real)
78
(declare-var saturate_test.Saturation4_1_2 Real)
79
(declare-var saturate_test.Saturation4_1_3 Real)
80
(declare-var saturate_test.Saturation4_1_4 Real)
81
(declare-var saturate_test.Saturation4_1_5 Real)
82
(declare-var saturate_test.Saturation4_1_6 Real)
83
(declare-var saturate_test.Saturation5_1_1 Real)
84
(declare-var saturate_test.Saturation5_1_2 Real)
85
(declare-var saturate_test.Saturation5_1_3 Real)
86
(declare-var saturate_test.Saturation6_1_1 Real)
87
(declare-var saturate_test.Saturation6_1_2 Real)
88
(declare-var saturate_test.Saturation6_1_3 Real)
89
(declare-var saturate_test.Saturation6_1_4 Real)
90
(declare-var saturate_test.Saturation6_1_5 Real)
91
(declare-var saturate_test.Saturation6_1_6 Real)
92
(declare-var saturate_test.Saturation7_1_1 Real)
93
(declare-var saturate_test.Saturation7_1_2 Real)
94
(declare-var saturate_test.Saturation7_1_3 Real)
95
(declare-var saturate_test.Saturation8_1_1 Real)
96
(declare-var saturate_test.Saturation8_1_2 Real)
97
(declare-var saturate_test.Saturation8_1_3 Real)
98
(declare-var saturate_test.Saturation8_1_4 Real)
99
(declare-var saturate_test.Saturation8_1_5 Real)
100
(declare-var saturate_test.Saturation8_1_6 Real)
101
(declare-var saturate_test.Saturation_1_1 Real)
102
(declare-var saturate_test.__saturate_test_1 Bool)
103
(declare-var saturate_test.__saturate_test_10 Bool)
104
(declare-var saturate_test.__saturate_test_11 Bool)
105
(declare-var saturate_test.__saturate_test_12 Bool)
106
(declare-var saturate_test.__saturate_test_13 Bool)
107
(declare-var saturate_test.__saturate_test_14 Bool)
108
(declare-var saturate_test.__saturate_test_15 Bool)
109
(declare-var saturate_test.__saturate_test_16 Bool)
110
(declare-var saturate_test.__saturate_test_17 Bool)
111
(declare-var saturate_test.__saturate_test_18 Bool)
112
(declare-var saturate_test.__saturate_test_19 Bool)
113
(declare-var saturate_test.__saturate_test_2 Bool)
114
(declare-var saturate_test.__saturate_test_20 Bool)
115
(declare-var saturate_test.__saturate_test_21 Bool)
116
(declare-var saturate_test.__saturate_test_22 Bool)
117
(declare-var saturate_test.__saturate_test_23 Bool)
118
(declare-var saturate_test.__saturate_test_24 Bool)
119
(declare-var saturate_test.__saturate_test_25 Bool)
120
(declare-var saturate_test.__saturate_test_26 Bool)
121
(declare-var saturate_test.__saturate_test_27 Bool)
122
(declare-var saturate_test.__saturate_test_28 Bool)
123
(declare-var saturate_test.__saturate_test_29 Bool)
124
(declare-var saturate_test.__saturate_test_3 Bool)
125
(declare-var saturate_test.__saturate_test_30 Bool)
126
(declare-var saturate_test.__saturate_test_31 Bool)
127
(declare-var saturate_test.__saturate_test_32 Bool)
128
(declare-var saturate_test.__saturate_test_33 Bool)
129
(declare-var saturate_test.__saturate_test_34 Bool)
130
(declare-var saturate_test.__saturate_test_35 Bool)
131
(declare-var saturate_test.__saturate_test_36 Bool)
132
(declare-var saturate_test.__saturate_test_37 Bool)
133
(declare-var saturate_test.__saturate_test_38 Bool)
134
(declare-var saturate_test.__saturate_test_39 Bool)
135
(declare-var saturate_test.__saturate_test_4 Bool)
136
(declare-var saturate_test.__saturate_test_40 Bool)
137
(declare-var saturate_test.__saturate_test_41 Bool)
138
(declare-var saturate_test.__saturate_test_42 Bool)
139
(declare-var saturate_test.__saturate_test_43 Bool)
140
(declare-var saturate_test.__saturate_test_44 Bool)
141
(declare-var saturate_test.__saturate_test_45 Bool)
142
(declare-var saturate_test.__saturate_test_46 Bool)
143
(declare-var saturate_test.__saturate_test_47 Bool)
144
(declare-var saturate_test.__saturate_test_48 Bool)
145
(declare-var saturate_test.__saturate_test_49 Bool)
146
(declare-var saturate_test.__saturate_test_5 Bool)
147
(declare-var saturate_test.__saturate_test_50 Bool)
148
(declare-var saturate_test.__saturate_test_51 Bool)
149
(declare-var saturate_test.__saturate_test_52 Bool)
150
(declare-var saturate_test.__saturate_test_53 Bool)
151
(declare-var saturate_test.__saturate_test_54 Bool)
152
(declare-var saturate_test.__saturate_test_55 Bool)
153
(declare-var saturate_test.__saturate_test_56 Bool)
154
(declare-var saturate_test.__saturate_test_57 Bool)
155
(declare-var saturate_test.__saturate_test_58 Bool)
156
(declare-var saturate_test.__saturate_test_59 Bool)
157
(declare-var saturate_test.__saturate_test_6 Bool)
158
(declare-var saturate_test.__saturate_test_60 Bool)
159
(declare-var saturate_test.__saturate_test_61 Bool)
160
(declare-var saturate_test.__saturate_test_62 Bool)
161
(declare-var saturate_test.__saturate_test_63 Bool)
162
(declare-var saturate_test.__saturate_test_64 Bool)
163
(declare-var saturate_test.__saturate_test_65 Bool)
164
(declare-var saturate_test.__saturate_test_66 Bool)
165
(declare-var saturate_test.__saturate_test_67 Bool)
166
(declare-var saturate_test.__saturate_test_68 Bool)
167
(declare-var saturate_test.__saturate_test_7 Bool)
168
(declare-var saturate_test.__saturate_test_8 Bool)
169
(declare-var saturate_test.__saturate_test_9 Bool)
170
(declare-var saturate_test.i_virtual_local Real)
171
(declare-rel saturate_test_reset (Bool Bool))
172
(declare-rel saturate_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 Bool Bool))
173

    
174
(rule (=> 
175
  (and 
176
       
177
       (= saturate_test.ni_0._arrow._first_m true)
178
  )
179
  (saturate_test_reset saturate_test.ni_0._arrow._first_c
180
                       saturate_test.ni_0._arrow._first_m)
181
))
182

    
183
(rule (=> 
184
  (and (= saturate_test.ni_0._arrow._first_m saturate_test.ni_0._arrow._first_c)
185
       (and (= saturate_test.__saturate_test_1 (ite saturate_test.ni_0._arrow._first_m true false))
186
            (= saturate_test.ni_0._arrow._first_x false))
187
       (and (or (not (= saturate_test.__saturate_test_1 true))
188
               (= saturate_test.i_virtual_local 0.0))
189
            (or (not (= saturate_test.__saturate_test_1 false))
190
               (= saturate_test.i_virtual_local 1.0))
191
       )
192
       (= saturate_test.__saturate_test_9 (>= saturate_test.In8_1_1 2.000000))
193
       (= saturate_test.__saturate_test_8 (>= saturate_test.In9_1_1 2.000000))
194
       (= saturate_test.__saturate_test_7 (>= saturate_test.In9_1_1 3.000000))
195
       (= saturate_test.__saturate_test_68 (<= saturate_test.In1_1_1 (- 0.500000)))
196
       (= saturate_test.__saturate_test_67 (>= saturate_test.In1_1_1 0.600000))
197
       (= saturate_test.__saturate_test_66 (<= saturate_test.In2_1_1 (- 0.500000)))
198
       (= saturate_test.__saturate_test_65 (>= saturate_test.In2_1_1 0.600000))
199
       (= saturate_test.__saturate_test_64 (<= saturate_test.In2_1_2 (- 0.500000)))
200
       (= saturate_test.__saturate_test_63 (>= saturate_test.In2_1_2 0.600000))
201
       (= saturate_test.__saturate_test_62 (<= saturate_test.In2_1_3 (- 0.500000)))
202
       (= saturate_test.__saturate_test_61 (>= saturate_test.In2_1_3 0.600000))
203
       (= saturate_test.__saturate_test_60 (<= saturate_test.In3_1_1 (- 0.500000)))
204
       (= saturate_test.__saturate_test_6 (>= saturate_test.In9_1_1 4.000000))
205
       (= saturate_test.__saturate_test_59 (>= saturate_test.In3_1_1 0.600000))
206
       (= saturate_test.__saturate_test_58 (<= saturate_test.In3_1_2 (- 0.500000)))
207
       (= saturate_test.__saturate_test_57 (>= saturate_test.In3_1_2 0.600000))
208
       (= saturate_test.__saturate_test_56 (<= saturate_test.In3_1_3 (- 0.500000)))
209
       (= saturate_test.__saturate_test_55 (>= saturate_test.In3_1_3 0.600000))
210
       (= saturate_test.__saturate_test_54 (<= saturate_test.In3_1_4 (- 0.500000)))
211
       (= saturate_test.__saturate_test_53 (>= saturate_test.In3_1_4 0.600000))
212
       (= saturate_test.__saturate_test_52 (<= saturate_test.In3_1_5 (- 0.500000)))
213
       (= saturate_test.__saturate_test_51 (>= saturate_test.In3_1_5 0.600000))
214
       (= saturate_test.__saturate_test_50 (<= saturate_test.In3_1_6 (- 0.500000)))
215
       (= saturate_test.__saturate_test_5 (>= saturate_test.In9_1_1 5.000000))
216
       (= saturate_test.__saturate_test_49 (>= saturate_test.In3_1_6 0.600000))
217
       (= saturate_test.__saturate_test_48 (<= saturate_test.In4_1_1 (- 0.500000)))
218
       (= saturate_test.__saturate_test_47 (>= saturate_test.In4_1_1 0.500000))
219
       (= saturate_test.__saturate_test_46 (<= saturate_test.In4_1_2 (- 0.600000)))
220
       (= saturate_test.__saturate_test_45 (>= saturate_test.In4_1_2 0.600000))
221
       (= saturate_test.__saturate_test_44 (<= saturate_test.In4_1_3 (- 0.700000)))
222
       (= saturate_test.__saturate_test_43 (>= saturate_test.In4_1_3 0.700000))
223
       (= saturate_test.__saturate_test_42 (<= saturate_test.In5_1_1 (- 0.500000)))
224
       (= saturate_test.__saturate_test_41 (>= saturate_test.In5_1_1 0.500000))
225
       (= saturate_test.__saturate_test_40 (<= saturate_test.In5_1_2 (- 0.600000)))
226
       (= saturate_test.__saturate_test_4 (>= saturate_test.In9_1_1 6.000000))
227
       (= saturate_test.__saturate_test_39 (>= saturate_test.In5_1_2 0.600000))
228
       (= saturate_test.__saturate_test_38 (<= saturate_test.In5_1_3 (- 0.700000)))
229
       (= saturate_test.__saturate_test_37 (>= saturate_test.In5_1_3 0.700000))
230
       (= saturate_test.__saturate_test_36 (<= saturate_test.In5_1_4 (- 1.500000)))
231
       (= saturate_test.__saturate_test_35 (>= saturate_test.In5_1_4 1.500000))
232
       (= saturate_test.__saturate_test_34 (<= saturate_test.In5_1_5 (- 1.600000)))
233
       (= saturate_test.__saturate_test_33 (>= saturate_test.In5_1_5 1.600000))
234
       (= saturate_test.__saturate_test_32 (<= saturate_test.In5_1_6 (- 1.700000)))
235
       (= saturate_test.__saturate_test_31 (>= saturate_test.In5_1_6 1.700000))
236
       (= saturate_test.__saturate_test_30 (<= saturate_test.In6_1_1 (- 2.000000)))
237
       (= saturate_test.__saturate_test_3 (<= saturate_test.In9_1_1 (- 2.000000)))
238
       (= saturate_test.__saturate_test_29 (>= saturate_test.In6_1_1 2.000000))
239
       (= saturate_test.__saturate_test_28 (<= saturate_test.In6_1_1 (- 3.000000)))
240
       (= saturate_test.__saturate_test_27 (>= saturate_test.In6_1_1 3.000000))
241
       (= saturate_test.__saturate_test_26 (<= saturate_test.In6_1_1 (- 4.000000)))
242
       (= saturate_test.__saturate_test_25 (>= saturate_test.In6_1_1 4.000000))
243
       (= saturate_test.__saturate_test_24 (<= saturate_test.In7_1_1 (- 2.000000)))
244
       (= saturate_test.__saturate_test_23 (>= saturate_test.In7_1_1 2.000000))
245
       (= saturate_test.__saturate_test_22 (<= saturate_test.In7_1_1 (- 3.000000)))
246
       (= saturate_test.__saturate_test_21 (>= saturate_test.In7_1_1 3.000000))
247
       (= saturate_test.__saturate_test_20 (<= saturate_test.In7_1_1 (- 4.000000)))
248
       (= saturate_test.__saturate_test_2 (>= saturate_test.In9_1_1 7.000000))
249
       (= saturate_test.__saturate_test_19 (>= saturate_test.In7_1_1 4.000000))
250
       (= saturate_test.__saturate_test_18 (<= saturate_test.In7_1_1 (- 5.000000)))
251
       (= saturate_test.__saturate_test_17 (>= saturate_test.In7_1_1 5.000000))
252
       (= saturate_test.__saturate_test_16 (<= saturate_test.In7_1_1 (- 6.000000)))
253
       (= saturate_test.__saturate_test_15 (>= saturate_test.In7_1_1 6.000000))
254
       (= saturate_test.__saturate_test_14 (<= saturate_test.In7_1_1 (- 7.000000)))
255
       (= saturate_test.__saturate_test_13 (>= saturate_test.In7_1_1 7.000000))
256
       (= saturate_test.__saturate_test_12 (<= saturate_test.In8_1_1 (- 2.000000)))
257
       (= saturate_test.__saturate_test_11 (<= saturate_test.In8_1_1 (- 3.000000)))
258
       (= saturate_test.__saturate_test_10 (<= saturate_test.In8_1_1 (- 4.000000)))
259
       (and (or (not (= saturate_test.__saturate_test_67 true))
260
               (= saturate_test.Saturation_1_1 0.600000))
261
            (or (not (= saturate_test.__saturate_test_67 false))
262
               (and (or (not (= saturate_test.__saturate_test_68 true))
263
                       (= saturate_test.Saturation_1_1 (- 0.500000)))
264
                    (or (not (= saturate_test.__saturate_test_68 false))
265
                       (= saturate_test.Saturation_1_1 saturate_test.In1_1_1))
266
               ))
267
       )
268
       (and (or (not (= saturate_test.__saturate_test_2 true))
269
               (= saturate_test.Saturation8_1_6 7.000000))
270
            (or (not (= saturate_test.__saturate_test_2 false))
271
               (and (or (not (= saturate_test.__saturate_test_3 true))
272
                       (= saturate_test.Saturation8_1_6 (- 2.000000)))
273
                    (or (not (= saturate_test.__saturate_test_3 false))
274
                       (= saturate_test.Saturation8_1_6 saturate_test.In9_1_1))
275
               ))
276
       )
277
       (and (or (not (= saturate_test.__saturate_test_4 true))
278
               (= saturate_test.Saturation8_1_5 6.000000))
279
            (or (not (= saturate_test.__saturate_test_4 false))
280
               (and (or (not (= saturate_test.__saturate_test_3 true))
281
                       (= saturate_test.Saturation8_1_5 (- 2.000000)))
282
                    (or (not (= saturate_test.__saturate_test_3 false))
283
                       (= saturate_test.Saturation8_1_5 saturate_test.In9_1_1))
284
               ))
285
       )
286
       (and (or (not (= saturate_test.__saturate_test_5 true))
287
               (= saturate_test.Saturation8_1_4 5.000000))
288
            (or (not (= saturate_test.__saturate_test_5 false))
289
               (and (or (not (= saturate_test.__saturate_test_3 true))
290
                       (= saturate_test.Saturation8_1_4 (- 2.000000)))
291
                    (or (not (= saturate_test.__saturate_test_3 false))
292
                       (= saturate_test.Saturation8_1_4 saturate_test.In9_1_1))
293
               ))
294
       )
295
       (and (or (not (= saturate_test.__saturate_test_6 true))
296
               (= saturate_test.Saturation8_1_3 4.000000))
297
            (or (not (= saturate_test.__saturate_test_6 false))
298
               (and (or (not (= saturate_test.__saturate_test_3 true))
299
                       (= saturate_test.Saturation8_1_3 (- 2.000000)))
300
                    (or (not (= saturate_test.__saturate_test_3 false))
301
                       (= saturate_test.Saturation8_1_3 saturate_test.In9_1_1))
302
               ))
303
       )
304
       (and (or (not (= saturate_test.__saturate_test_7 true))
305
               (= saturate_test.Saturation8_1_2 3.000000))
306
            (or (not (= saturate_test.__saturate_test_7 false))
307
               (and (or (not (= saturate_test.__saturate_test_3 true))
308
                       (= saturate_test.Saturation8_1_2 (- 2.000000)))
309
                    (or (not (= saturate_test.__saturate_test_3 false))
310
                       (= saturate_test.Saturation8_1_2 saturate_test.In9_1_1))
311
               ))
312
       )
313
       (and (or (not (= saturate_test.__saturate_test_8 true))
314
               (= saturate_test.Saturation8_1_1 2.000000))
315
            (or (not (= saturate_test.__saturate_test_8 false))
316
               (and (or (not (= saturate_test.__saturate_test_3 true))
317
                       (= saturate_test.Saturation8_1_1 (- 2.000000)))
318
                    (or (not (= saturate_test.__saturate_test_3 false))
319
                       (= saturate_test.Saturation8_1_1 saturate_test.In9_1_1))
320
               ))
321
       )
322
       (and (or (not (= saturate_test.__saturate_test_9 false))
323
               (and (and (or (not (= saturate_test.__saturate_test_10 true))
324
                            (= saturate_test.Saturation7_1_3 (- 4.000000)))
325
                         (or (not (= saturate_test.__saturate_test_10 false))
326
                            (= saturate_test.Saturation7_1_3 saturate_test.In8_1_1))
327
                    )
328
                    (and (or (not (= saturate_test.__saturate_test_11 true))
329
                            (= saturate_test.Saturation7_1_2 (- 3.000000)))
330
                         (or (not (= saturate_test.__saturate_test_11 false))
331
                            (= saturate_test.Saturation7_1_2 saturate_test.In8_1_1))
332
                    )
333
                    (and (or (not (= saturate_test.__saturate_test_12 true))
334
                            (= saturate_test.Saturation7_1_1 (- 2.000000)))
335
                         (or (not (= saturate_test.__saturate_test_12 false))
336
                            (= saturate_test.Saturation7_1_1 saturate_test.In8_1_1))
337
                    )
338
                    ))
339
            (or (not (= saturate_test.__saturate_test_9 true))
340
               (and (= saturate_test.Saturation7_1_3 2.000000)
341
                    (= saturate_test.Saturation7_1_2 2.000000)
342
                    (= saturate_test.Saturation7_1_1 2.000000)
343
                    ))
344
       )
345
       (and (or (not (= saturate_test.__saturate_test_13 true))
346
               (= saturate_test.Saturation6_1_6 7.000000))
347
            (or (not (= saturate_test.__saturate_test_13 false))
348
               (and (or (not (= saturate_test.__saturate_test_14 true))
349
                       (= saturate_test.Saturation6_1_6 (- 7.000000)))
350
                    (or (not (= saturate_test.__saturate_test_14 false))
351
                       (= saturate_test.Saturation6_1_6 saturate_test.In7_1_1))
352
               ))
353
       )
354
       (and (or (not (= saturate_test.__saturate_test_15 true))
355
               (= saturate_test.Saturation6_1_5 6.000000))
356
            (or (not (= saturate_test.__saturate_test_15 false))
357
               (and (or (not (= saturate_test.__saturate_test_16 true))
358
                       (= saturate_test.Saturation6_1_5 (- 6.000000)))
359
                    (or (not (= saturate_test.__saturate_test_16 false))
360
                       (= saturate_test.Saturation6_1_5 saturate_test.In7_1_1))
361
               ))
362
       )
363
       (and (or (not (= saturate_test.__saturate_test_17 true))
364
               (= saturate_test.Saturation6_1_4 5.000000))
365
            (or (not (= saturate_test.__saturate_test_17 false))
366
               (and (or (not (= saturate_test.__saturate_test_18 true))
367
                       (= saturate_test.Saturation6_1_4 (- 5.000000)))
368
                    (or (not (= saturate_test.__saturate_test_18 false))
369
                       (= saturate_test.Saturation6_1_4 saturate_test.In7_1_1))
370
               ))
371
       )
372
       (and (or (not (= saturate_test.__saturate_test_19 true))
373
               (= saturate_test.Saturation6_1_3 4.000000))
374
            (or (not (= saturate_test.__saturate_test_19 false))
375
               (and (or (not (= saturate_test.__saturate_test_20 true))
376
                       (= saturate_test.Saturation6_1_3 (- 4.000000)))
377
                    (or (not (= saturate_test.__saturate_test_20 false))
378
                       (= saturate_test.Saturation6_1_3 saturate_test.In7_1_1))
379
               ))
380
       )
381
       (and (or (not (= saturate_test.__saturate_test_21 true))
382
               (= saturate_test.Saturation6_1_2 3.000000))
383
            (or (not (= saturate_test.__saturate_test_21 false))
384
               (and (or (not (= saturate_test.__saturate_test_22 true))
385
                       (= saturate_test.Saturation6_1_2 (- 3.000000)))
386
                    (or (not (= saturate_test.__saturate_test_22 false))
387
                       (= saturate_test.Saturation6_1_2 saturate_test.In7_1_1))
388
               ))
389
       )
390
       (and (or (not (= saturate_test.__saturate_test_23 true))
391
               (= saturate_test.Saturation6_1_1 2.000000))
392
            (or (not (= saturate_test.__saturate_test_23 false))
393
               (and (or (not (= saturate_test.__saturate_test_24 true))
394
                       (= saturate_test.Saturation6_1_1 (- 2.000000)))
395
                    (or (not (= saturate_test.__saturate_test_24 false))
396
                       (= saturate_test.Saturation6_1_1 saturate_test.In7_1_1))
397
               ))
398
       )
399
       (and (or (not (= saturate_test.__saturate_test_25 true))
400
               (= saturate_test.Saturation5_1_3 4.000000))
401
            (or (not (= saturate_test.__saturate_test_25 false))
402
               (and (or (not (= saturate_test.__saturate_test_26 true))
403
                       (= saturate_test.Saturation5_1_3 (- 4.000000)))
404
                    (or (not (= saturate_test.__saturate_test_26 false))
405
                       (= saturate_test.Saturation5_1_3 saturate_test.In6_1_1))
406
               ))
407
       )
408
       (and (or (not (= saturate_test.__saturate_test_27 true))
409
               (= saturate_test.Saturation5_1_2 3.000000))
410
            (or (not (= saturate_test.__saturate_test_27 false))
411
               (and (or (not (= saturate_test.__saturate_test_28 true))
412
                       (= saturate_test.Saturation5_1_2 (- 3.000000)))
413
                    (or (not (= saturate_test.__saturate_test_28 false))
414
                       (= saturate_test.Saturation5_1_2 saturate_test.In6_1_1))
415
               ))
416
       )
417
       (and (or (not (= saturate_test.__saturate_test_29 true))
418
               (= saturate_test.Saturation5_1_1 2.000000))
419
            (or (not (= saturate_test.__saturate_test_29 false))
420
               (and (or (not (= saturate_test.__saturate_test_30 true))
421
                       (= saturate_test.Saturation5_1_1 (- 2.000000)))
422
                    (or (not (= saturate_test.__saturate_test_30 false))
423
                       (= saturate_test.Saturation5_1_1 saturate_test.In6_1_1))
424
               ))
425
       )
426
       (and (or (not (= saturate_test.__saturate_test_31 true))
427
               (= saturate_test.Saturation4_1_6 1.700000))
428
            (or (not (= saturate_test.__saturate_test_31 false))
429
               (and (or (not (= saturate_test.__saturate_test_32 true))
430
                       (= saturate_test.Saturation4_1_6 (- 1.700000)))
431
                    (or (not (= saturate_test.__saturate_test_32 false))
432
                       (= saturate_test.Saturation4_1_6 saturate_test.In5_1_6))
433
               ))
434
       )
435
       (and (or (not (= saturate_test.__saturate_test_33 true))
436
               (= saturate_test.Saturation4_1_5 1.600000))
437
            (or (not (= saturate_test.__saturate_test_33 false))
438
               (and (or (not (= saturate_test.__saturate_test_34 true))
439
                       (= saturate_test.Saturation4_1_5 (- 1.600000)))
440
                    (or (not (= saturate_test.__saturate_test_34 false))
441
                       (= saturate_test.Saturation4_1_5 saturate_test.In5_1_5))
442
               ))
443
       )
444
       (and (or (not (= saturate_test.__saturate_test_35 true))
445
               (= saturate_test.Saturation4_1_4 1.500000))
446
            (or (not (= saturate_test.__saturate_test_35 false))
447
               (and (or (not (= saturate_test.__saturate_test_36 true))
448
                       (= saturate_test.Saturation4_1_4 (- 1.500000)))
449
                    (or (not (= saturate_test.__saturate_test_36 false))
450
                       (= saturate_test.Saturation4_1_4 saturate_test.In5_1_4))
451
               ))
452
       )
453
       (and (or (not (= saturate_test.__saturate_test_37 true))
454
               (= saturate_test.Saturation4_1_3 0.700000))
455
            (or (not (= saturate_test.__saturate_test_37 false))
456
               (and (or (not (= saturate_test.__saturate_test_38 true))
457
                       (= saturate_test.Saturation4_1_3 (- 0.700000)))
458
                    (or (not (= saturate_test.__saturate_test_38 false))
459
                       (= saturate_test.Saturation4_1_3 saturate_test.In5_1_3))
460
               ))
461
       )
462
       (and (or (not (= saturate_test.__saturate_test_39 true))
463
               (= saturate_test.Saturation4_1_2 0.600000))
464
            (or (not (= saturate_test.__saturate_test_39 false))
465
               (and (or (not (= saturate_test.__saturate_test_40 true))
466
                       (= saturate_test.Saturation4_1_2 (- 0.600000)))
467
                    (or (not (= saturate_test.__saturate_test_40 false))
468
                       (= saturate_test.Saturation4_1_2 saturate_test.In5_1_2))
469
               ))
470
       )
471
       (and (or (not (= saturate_test.__saturate_test_41 true))
472
               (= saturate_test.Saturation4_1_1 0.500000))
473
            (or (not (= saturate_test.__saturate_test_41 false))
474
               (and (or (not (= saturate_test.__saturate_test_42 true))
475
                       (= saturate_test.Saturation4_1_1 (- 0.500000)))
476
                    (or (not (= saturate_test.__saturate_test_42 false))
477
                       (= saturate_test.Saturation4_1_1 saturate_test.In5_1_1))
478
               ))
479
       )
480
       (and (or (not (= saturate_test.__saturate_test_43 true))
481
               (= saturate_test.Saturation3_1_3 0.700000))
482
            (or (not (= saturate_test.__saturate_test_43 false))
483
               (and (or (not (= saturate_test.__saturate_test_44 true))
484
                       (= saturate_test.Saturation3_1_3 (- 0.700000)))
485
                    (or (not (= saturate_test.__saturate_test_44 false))
486
                       (= saturate_test.Saturation3_1_3 saturate_test.In4_1_3))
487
               ))
488
       )
489
       (and (or (not (= saturate_test.__saturate_test_45 true))
490
               (= saturate_test.Saturation3_1_2 0.600000))
491
            (or (not (= saturate_test.__saturate_test_45 false))
492
               (and (or (not (= saturate_test.__saturate_test_46 true))
493
                       (= saturate_test.Saturation3_1_2 (- 0.600000)))
494
                    (or (not (= saturate_test.__saturate_test_46 false))
495
                       (= saturate_test.Saturation3_1_2 saturate_test.In4_1_2))
496
               ))
497
       )
498
       (and (or (not (= saturate_test.__saturate_test_47 true))
499
               (= saturate_test.Saturation3_1_1 0.500000))
500
            (or (not (= saturate_test.__saturate_test_47 false))
501
               (and (or (not (= saturate_test.__saturate_test_48 true))
502
                       (= saturate_test.Saturation3_1_1 (- 0.500000)))
503
                    (or (not (= saturate_test.__saturate_test_48 false))
504
                       (= saturate_test.Saturation3_1_1 saturate_test.In4_1_1))
505
               ))
506
       )
507
       (and (or (not (= saturate_test.__saturate_test_49 true))
508
               (= saturate_test.Saturation2_1_6 0.600000))
509
            (or (not (= saturate_test.__saturate_test_49 false))
510
               (and (or (not (= saturate_test.__saturate_test_50 true))
511
                       (= saturate_test.Saturation2_1_6 (- 0.500000)))
512
                    (or (not (= saturate_test.__saturate_test_50 false))
513
                       (= saturate_test.Saturation2_1_6 saturate_test.In3_1_6))
514
               ))
515
       )
516
       (and (or (not (= saturate_test.__saturate_test_51 true))
517
               (= saturate_test.Saturation2_1_5 0.600000))
518
            (or (not (= saturate_test.__saturate_test_51 false))
519
               (and (or (not (= saturate_test.__saturate_test_52 true))
520
                       (= saturate_test.Saturation2_1_5 (- 0.500000)))
521
                    (or (not (= saturate_test.__saturate_test_52 false))
522
                       (= saturate_test.Saturation2_1_5 saturate_test.In3_1_5))
523
               ))
524
       )
525
       (and (or (not (= saturate_test.__saturate_test_53 true))
526
               (= saturate_test.Saturation2_1_4 0.600000))
527
            (or (not (= saturate_test.__saturate_test_53 false))
528
               (and (or (not (= saturate_test.__saturate_test_54 true))
529
                       (= saturate_test.Saturation2_1_4 (- 0.500000)))
530
                    (or (not (= saturate_test.__saturate_test_54 false))
531
                       (= saturate_test.Saturation2_1_4 saturate_test.In3_1_4))
532
               ))
533
       )
534
       (and (or (not (= saturate_test.__saturate_test_55 true))
535
               (= saturate_test.Saturation2_1_3 0.600000))
536
            (or (not (= saturate_test.__saturate_test_55 false))
537
               (and (or (not (= saturate_test.__saturate_test_56 true))
538
                       (= saturate_test.Saturation2_1_3 (- 0.500000)))
539
                    (or (not (= saturate_test.__saturate_test_56 false))
540
                       (= saturate_test.Saturation2_1_3 saturate_test.In3_1_3))
541
               ))
542
       )
543
       (and (or (not (= saturate_test.__saturate_test_57 true))
544
               (= saturate_test.Saturation2_1_2 0.600000))
545
            (or (not (= saturate_test.__saturate_test_57 false))
546
               (and (or (not (= saturate_test.__saturate_test_58 true))
547
                       (= saturate_test.Saturation2_1_2 (- 0.500000)))
548
                    (or (not (= saturate_test.__saturate_test_58 false))
549
                       (= saturate_test.Saturation2_1_2 saturate_test.In3_1_2))
550
               ))
551
       )
552
       (and (or (not (= saturate_test.__saturate_test_59 true))
553
               (= saturate_test.Saturation2_1_1 0.600000))
554
            (or (not (= saturate_test.__saturate_test_59 false))
555
               (and (or (not (= saturate_test.__saturate_test_60 true))
556
                       (= saturate_test.Saturation2_1_1 (- 0.500000)))
557
                    (or (not (= saturate_test.__saturate_test_60 false))
558
                       (= saturate_test.Saturation2_1_1 saturate_test.In3_1_1))
559
               ))
560
       )
561
       (and (or (not (= saturate_test.__saturate_test_61 true))
562
               (= saturate_test.Saturation1_1_3 0.600000))
563
            (or (not (= saturate_test.__saturate_test_61 false))
564
               (and (or (not (= saturate_test.__saturate_test_62 true))
565
                       (= saturate_test.Saturation1_1_3 (- 0.500000)))
566
                    (or (not (= saturate_test.__saturate_test_62 false))
567
                       (= saturate_test.Saturation1_1_3 saturate_test.In2_1_3))
568
               ))
569
       )
570
       (and (or (not (= saturate_test.__saturate_test_63 true))
571
               (= saturate_test.Saturation1_1_2 0.600000))
572
            (or (not (= saturate_test.__saturate_test_63 false))
573
               (and (or (not (= saturate_test.__saturate_test_64 true))
574
                       (= saturate_test.Saturation1_1_2 (- 0.500000)))
575
                    (or (not (= saturate_test.__saturate_test_64 false))
576
                       (= saturate_test.Saturation1_1_2 saturate_test.In2_1_2))
577
               ))
578
       )
579
       (and (or (not (= saturate_test.__saturate_test_65 true))
580
               (= saturate_test.Saturation1_1_1 0.600000))
581
            (or (not (= saturate_test.__saturate_test_65 false))
582
               (and (or (not (= saturate_test.__saturate_test_66 true))
583
                       (= saturate_test.Saturation1_1_1 (- 0.500000)))
584
                    (or (not (= saturate_test.__saturate_test_66 false))
585
                       (= saturate_test.Saturation1_1_1 saturate_test.In2_1_1))
586
               ))
587
       )
588
       (= saturate_test.Out9_9_6 saturate_test.Saturation8_1_6)
589
       (= saturate_test.Out9_9_5 saturate_test.Saturation8_1_5)
590
       (= saturate_test.Out9_9_4 saturate_test.Saturation8_1_4)
591
       (= saturate_test.Out9_9_3 saturate_test.Saturation8_1_3)
592
       (= saturate_test.Out9_9_2 saturate_test.Saturation8_1_2)
593
       (= saturate_test.Out9_9_1 saturate_test.Saturation8_1_1)
594
       (= saturate_test.Out8_8_3 saturate_test.Saturation7_1_3)
595
       (= saturate_test.Out8_8_2 saturate_test.Saturation7_1_2)
596
       (= saturate_test.Out8_8_1 saturate_test.Saturation7_1_1)
597
       (= saturate_test.Out7_7_6 saturate_test.Saturation6_1_6)
598
       (= saturate_test.Out7_7_5 saturate_test.Saturation6_1_5)
599
       (= saturate_test.Out7_7_4 saturate_test.Saturation6_1_4)
600
       (= saturate_test.Out7_7_3 saturate_test.Saturation6_1_3)
601
       (= saturate_test.Out7_7_2 saturate_test.Saturation6_1_2)
602
       (= saturate_test.Out7_7_1 saturate_test.Saturation6_1_1)
603
       (= saturate_test.Out6_6_3 saturate_test.Saturation5_1_3)
604
       (= saturate_test.Out6_6_2 saturate_test.Saturation5_1_2)
605
       (= saturate_test.Out6_6_1 saturate_test.Saturation5_1_1)
606
       (= saturate_test.Out5_5_6 saturate_test.Saturation4_1_6)
607
       (= saturate_test.Out5_5_5 saturate_test.Saturation4_1_5)
608
       (= saturate_test.Out5_5_4 saturate_test.Saturation4_1_4)
609
       (= saturate_test.Out5_5_3 saturate_test.Saturation4_1_3)
610
       (= saturate_test.Out5_5_2 saturate_test.Saturation4_1_2)
611
       (= saturate_test.Out5_5_1 saturate_test.Saturation4_1_1)
612
       (= saturate_test.Out4_4_3 saturate_test.Saturation3_1_3)
613
       (= saturate_test.Out4_4_2 saturate_test.Saturation3_1_2)
614
       (= saturate_test.Out4_4_1 saturate_test.Saturation3_1_1)
615
       (= saturate_test.Out3_3_6 saturate_test.Saturation2_1_6)
616
       (= saturate_test.Out3_3_5 saturate_test.Saturation2_1_5)
617
       (= saturate_test.Out3_3_4 saturate_test.Saturation2_1_4)
618
       (= saturate_test.Out3_3_3 saturate_test.Saturation2_1_3)
619
       (= saturate_test.Out3_3_2 saturate_test.Saturation2_1_2)
620
       (= saturate_test.Out3_3_1 saturate_test.Saturation2_1_1)
621
       (= saturate_test.Out2_2_3 saturate_test.Saturation1_1_3)
622
       (= saturate_test.Out2_2_2 saturate_test.Saturation1_1_2)
623
       (= saturate_test.Out2_2_1 saturate_test.Saturation1_1_1)
624
       (= saturate_test.Out1_1_1 saturate_test.Saturation_1_1)
625
       )
626
  (saturate_test_step saturate_test.In1_1_1
627
                      saturate_test.In2_1_1
628
                      saturate_test.In2_1_2
629
                      saturate_test.In2_1_3
630
                      saturate_test.In3_1_1
631
                      saturate_test.In3_1_2
632
                      saturate_test.In3_1_3
633
                      saturate_test.In3_1_4
634
                      saturate_test.In3_1_5
635
                      saturate_test.In3_1_6
636
                      saturate_test.In4_1_1
637
                      saturate_test.In4_1_2
638
                      saturate_test.In4_1_3
639
                      saturate_test.In5_1_1
640
                      saturate_test.In5_1_2
641
                      saturate_test.In5_1_3
642
                      saturate_test.In5_1_4
643
                      saturate_test.In5_1_5
644
                      saturate_test.In5_1_6
645
                      saturate_test.In6_1_1
646
                      saturate_test.In7_1_1
647
                      saturate_test.In8_1_1
648
                      saturate_test.In9_1_1
649
                      saturate_test.Out1_1_1
650
                      saturate_test.Out2_2_1
651
                      saturate_test.Out2_2_2
652
                      saturate_test.Out2_2_3
653
                      saturate_test.Out3_3_1
654
                      saturate_test.Out3_3_2
655
                      saturate_test.Out3_3_3
656
                      saturate_test.Out3_3_4
657
                      saturate_test.Out3_3_5
658
                      saturate_test.Out3_3_6
659
                      saturate_test.Out4_4_1
660
                      saturate_test.Out4_4_2
661
                      saturate_test.Out4_4_3
662
                      saturate_test.Out5_5_1
663
                      saturate_test.Out5_5_2
664
                      saturate_test.Out5_5_3
665
                      saturate_test.Out5_5_4
666
                      saturate_test.Out5_5_5
667
                      saturate_test.Out5_5_6
668
                      saturate_test.Out6_6_1
669
                      saturate_test.Out6_6_2
670
                      saturate_test.Out6_6_3
671
                      saturate_test.Out7_7_1
672
                      saturate_test.Out7_7_2
673
                      saturate_test.Out7_7_3
674
                      saturate_test.Out7_7_4
675
                      saturate_test.Out7_7_5
676
                      saturate_test.Out7_7_6
677
                      saturate_test.Out8_8_1
678
                      saturate_test.Out8_8_2
679
                      saturate_test.Out8_8_3
680
                      saturate_test.Out9_9_1
681
                      saturate_test.Out9_9_2
682
                      saturate_test.Out9_9_3
683
                      saturate_test.Out9_9_4
684
                      saturate_test.Out9_9_5
685
                      saturate_test.Out9_9_6
686
                      saturate_test.ni_0._arrow._first_c
687
                      saturate_test.ni_0._arrow._first_x)
688
))
689