Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_saturate_int_test / saturate_int_test.smt2 @ 6c3ea955

History | View | Annotate | Download (41.9 KB)

1
; saturate_int_test
2
(declare-var saturate_int_test.In1_1_1 Real)
3
(declare-var saturate_int_test.In2_1_1 Real)
4
(declare-var saturate_int_test.In2_1_2 Real)
5
(declare-var saturate_int_test.In2_1_3 Real)
6
(declare-var saturate_int_test.In3_1_1 Real)
7
(declare-var saturate_int_test.In3_1_2 Real)
8
(declare-var saturate_int_test.In3_1_3 Real)
9
(declare-var saturate_int_test.In3_1_4 Real)
10
(declare-var saturate_int_test.In3_1_5 Real)
11
(declare-var saturate_int_test.In3_1_6 Real)
12
(declare-var saturate_int_test.In4_1_1 Real)
13
(declare-var saturate_int_test.In4_1_2 Real)
14
(declare-var saturate_int_test.In4_1_3 Real)
15
(declare-var saturate_int_test.In5_1_1 Real)
16
(declare-var saturate_int_test.In5_1_2 Real)
17
(declare-var saturate_int_test.In5_1_3 Real)
18
(declare-var saturate_int_test.In5_1_4 Real)
19
(declare-var saturate_int_test.In5_1_5 Real)
20
(declare-var saturate_int_test.In5_1_6 Real)
21
(declare-var saturate_int_test.In6_1_1 Real)
22
(declare-var saturate_int_test.In7_1_1 Real)
23
(declare-var saturate_int_test.In8_1_1 Real)
24
(declare-var saturate_int_test.In9_1_1 Real)
25
(declare-var saturate_int_test.Out1_1_1 Real)
26
(declare-var saturate_int_test.Out2_2_1 Real)
27
(declare-var saturate_int_test.Out2_2_2 Real)
28
(declare-var saturate_int_test.Out2_2_3 Real)
29
(declare-var saturate_int_test.Out3_3_1 Real)
30
(declare-var saturate_int_test.Out3_3_2 Real)
31
(declare-var saturate_int_test.Out3_3_3 Real)
32
(declare-var saturate_int_test.Out3_3_4 Real)
33
(declare-var saturate_int_test.Out3_3_5 Real)
34
(declare-var saturate_int_test.Out3_3_6 Real)
35
(declare-var saturate_int_test.Out4_4_1 Real)
36
(declare-var saturate_int_test.Out4_4_2 Real)
37
(declare-var saturate_int_test.Out4_4_3 Real)
38
(declare-var saturate_int_test.Out5_5_1 Real)
39
(declare-var saturate_int_test.Out5_5_2 Real)
40
(declare-var saturate_int_test.Out5_5_3 Real)
41
(declare-var saturate_int_test.Out5_5_4 Real)
42
(declare-var saturate_int_test.Out5_5_5 Real)
43
(declare-var saturate_int_test.Out5_5_6 Real)
44
(declare-var saturate_int_test.Out6_6_1 Real)
45
(declare-var saturate_int_test.Out6_6_2 Real)
46
(declare-var saturate_int_test.Out6_6_3 Real)
47
(declare-var saturate_int_test.Out7_7_1 Real)
48
(declare-var saturate_int_test.Out7_7_2 Real)
49
(declare-var saturate_int_test.Out7_7_3 Real)
50
(declare-var saturate_int_test.Out7_7_4 Real)
51
(declare-var saturate_int_test.Out7_7_5 Real)
52
(declare-var saturate_int_test.Out7_7_6 Real)
53
(declare-var saturate_int_test.Out8_8_1 Real)
54
(declare-var saturate_int_test.Out8_8_2 Real)
55
(declare-var saturate_int_test.Out8_8_3 Real)
56
(declare-var saturate_int_test.Out9_9_1 Real)
57
(declare-var saturate_int_test.Out9_9_2 Real)
58
(declare-var saturate_int_test.Out9_9_3 Real)
59
(declare-var saturate_int_test.Out9_9_4 Real)
60
(declare-var saturate_int_test.Out9_9_5 Real)
61
(declare-var saturate_int_test.Out9_9_6 Real)
62
(declare-var saturate_int_test.ni_0._arrow._first_c Bool)
63
(declare-var saturate_int_test.ni_0._arrow._first_m Bool)
64
(declare-var saturate_int_test.ni_0._arrow._first_x Bool)
65
(declare-var saturate_int_test.Saturation1_1_1 Real)
66
(declare-var saturate_int_test.Saturation1_1_2 Real)
67
(declare-var saturate_int_test.Saturation1_1_3 Real)
68
(declare-var saturate_int_test.Saturation2_1_1 Real)
69
(declare-var saturate_int_test.Saturation2_1_2 Real)
70
(declare-var saturate_int_test.Saturation2_1_3 Real)
71
(declare-var saturate_int_test.Saturation2_1_4 Real)
72
(declare-var saturate_int_test.Saturation2_1_5 Real)
73
(declare-var saturate_int_test.Saturation2_1_6 Real)
74
(declare-var saturate_int_test.Saturation3_1_1 Real)
75
(declare-var saturate_int_test.Saturation3_1_2 Real)
76
(declare-var saturate_int_test.Saturation3_1_3 Real)
77
(declare-var saturate_int_test.Saturation4_1_1 Real)
78
(declare-var saturate_int_test.Saturation4_1_2 Real)
79
(declare-var saturate_int_test.Saturation4_1_3 Real)
80
(declare-var saturate_int_test.Saturation4_1_4 Real)
81
(declare-var saturate_int_test.Saturation4_1_5 Real)
82
(declare-var saturate_int_test.Saturation4_1_6 Real)
83
(declare-var saturate_int_test.Saturation5_1_1 Real)
84
(declare-var saturate_int_test.Saturation5_1_2 Real)
85
(declare-var saturate_int_test.Saturation5_1_3 Real)
86
(declare-var saturate_int_test.Saturation6_1_1 Real)
87
(declare-var saturate_int_test.Saturation6_1_2 Real)
88
(declare-var saturate_int_test.Saturation6_1_3 Real)
89
(declare-var saturate_int_test.Saturation6_1_4 Real)
90
(declare-var saturate_int_test.Saturation6_1_5 Real)
91
(declare-var saturate_int_test.Saturation6_1_6 Real)
92
(declare-var saturate_int_test.Saturation7_1_1 Real)
93
(declare-var saturate_int_test.Saturation7_1_2 Real)
94
(declare-var saturate_int_test.Saturation7_1_3 Real)
95
(declare-var saturate_int_test.Saturation8_1_1 Real)
96
(declare-var saturate_int_test.Saturation8_1_2 Real)
97
(declare-var saturate_int_test.Saturation8_1_3 Real)
98
(declare-var saturate_int_test.Saturation8_1_4 Real)
99
(declare-var saturate_int_test.Saturation8_1_5 Real)
100
(declare-var saturate_int_test.Saturation8_1_6 Real)
101
(declare-var saturate_int_test.Saturation_1_1 Real)
102
(declare-var saturate_int_test.__saturate_int_test_1 Bool)
103
(declare-var saturate_int_test.__saturate_int_test_10 Bool)
104
(declare-var saturate_int_test.__saturate_int_test_11 Bool)
105
(declare-var saturate_int_test.__saturate_int_test_12 Bool)
106
(declare-var saturate_int_test.__saturate_int_test_13 Bool)
107
(declare-var saturate_int_test.__saturate_int_test_14 Bool)
108
(declare-var saturate_int_test.__saturate_int_test_15 Bool)
109
(declare-var saturate_int_test.__saturate_int_test_16 Bool)
110
(declare-var saturate_int_test.__saturate_int_test_17 Bool)
111
(declare-var saturate_int_test.__saturate_int_test_18 Bool)
112
(declare-var saturate_int_test.__saturate_int_test_19 Bool)
113
(declare-var saturate_int_test.__saturate_int_test_2 Bool)
114
(declare-var saturate_int_test.__saturate_int_test_20 Bool)
115
(declare-var saturate_int_test.__saturate_int_test_21 Bool)
116
(declare-var saturate_int_test.__saturate_int_test_22 Bool)
117
(declare-var saturate_int_test.__saturate_int_test_23 Bool)
118
(declare-var saturate_int_test.__saturate_int_test_24 Bool)
119
(declare-var saturate_int_test.__saturate_int_test_25 Bool)
120
(declare-var saturate_int_test.__saturate_int_test_26 Bool)
121
(declare-var saturate_int_test.__saturate_int_test_27 Bool)
122
(declare-var saturate_int_test.__saturate_int_test_28 Bool)
123
(declare-var saturate_int_test.__saturate_int_test_29 Bool)
124
(declare-var saturate_int_test.__saturate_int_test_3 Bool)
125
(declare-var saturate_int_test.__saturate_int_test_30 Bool)
126
(declare-var saturate_int_test.__saturate_int_test_31 Bool)
127
(declare-var saturate_int_test.__saturate_int_test_32 Bool)
128
(declare-var saturate_int_test.__saturate_int_test_33 Bool)
129
(declare-var saturate_int_test.__saturate_int_test_34 Bool)
130
(declare-var saturate_int_test.__saturate_int_test_35 Bool)
131
(declare-var saturate_int_test.__saturate_int_test_36 Bool)
132
(declare-var saturate_int_test.__saturate_int_test_37 Bool)
133
(declare-var saturate_int_test.__saturate_int_test_38 Bool)
134
(declare-var saturate_int_test.__saturate_int_test_39 Bool)
135
(declare-var saturate_int_test.__saturate_int_test_4 Bool)
136
(declare-var saturate_int_test.__saturate_int_test_40 Bool)
137
(declare-var saturate_int_test.__saturate_int_test_41 Bool)
138
(declare-var saturate_int_test.__saturate_int_test_42 Bool)
139
(declare-var saturate_int_test.__saturate_int_test_43 Bool)
140
(declare-var saturate_int_test.__saturate_int_test_44 Bool)
141
(declare-var saturate_int_test.__saturate_int_test_45 Bool)
142
(declare-var saturate_int_test.__saturate_int_test_46 Bool)
143
(declare-var saturate_int_test.__saturate_int_test_47 Bool)
144
(declare-var saturate_int_test.__saturate_int_test_48 Bool)
145
(declare-var saturate_int_test.__saturate_int_test_49 Bool)
146
(declare-var saturate_int_test.__saturate_int_test_5 Bool)
147
(declare-var saturate_int_test.__saturate_int_test_50 Bool)
148
(declare-var saturate_int_test.__saturate_int_test_51 Bool)
149
(declare-var saturate_int_test.__saturate_int_test_52 Bool)
150
(declare-var saturate_int_test.__saturate_int_test_53 Bool)
151
(declare-var saturate_int_test.__saturate_int_test_54 Bool)
152
(declare-var saturate_int_test.__saturate_int_test_55 Bool)
153
(declare-var saturate_int_test.__saturate_int_test_56 Bool)
154
(declare-var saturate_int_test.__saturate_int_test_57 Bool)
155
(declare-var saturate_int_test.__saturate_int_test_58 Bool)
156
(declare-var saturate_int_test.__saturate_int_test_59 Bool)
157
(declare-var saturate_int_test.__saturate_int_test_6 Bool)
158
(declare-var saturate_int_test.__saturate_int_test_60 Bool)
159
(declare-var saturate_int_test.__saturate_int_test_61 Bool)
160
(declare-var saturate_int_test.__saturate_int_test_62 Bool)
161
(declare-var saturate_int_test.__saturate_int_test_63 Bool)
162
(declare-var saturate_int_test.__saturate_int_test_64 Bool)
163
(declare-var saturate_int_test.__saturate_int_test_65 Bool)
164
(declare-var saturate_int_test.__saturate_int_test_66 Bool)
165
(declare-var saturate_int_test.__saturate_int_test_67 Bool)
166
(declare-var saturate_int_test.__saturate_int_test_68 Bool)
167
(declare-var saturate_int_test.__saturate_int_test_7 Bool)
168
(declare-var saturate_int_test.__saturate_int_test_8 Bool)
169
(declare-var saturate_int_test.__saturate_int_test_9 Bool)
170
(declare-var saturate_int_test.i_virtual_local Real)
171
(declare-rel saturate_int_test_reset (Bool Bool))
172
(declare-rel saturate_int_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_int_test.ni_0._arrow._first_m true)
178
  )
179
  (saturate_int_test_reset saturate_int_test.ni_0._arrow._first_c
180
                           saturate_int_test.ni_0._arrow._first_m)
181
))
182

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