Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Arrays1 / Arrays1.smt2 @ eb639349

History | View | Annotate | Download (92.5 KB)

1
(declare-datatypes () ((arrays1_arrays1__type POINTArrays1_Arrays1 POINT__TO__ARRAYS1_A_1 ARRAYS1_A__TO__ARRAYS1_B_1 ARRAYS1_B__TO__ARRAYS1_C_1 ARRAYS1_C__TO__ARRAYS1_A_1 ARRAYS1_A_IDL ARRAYS1_B_IDL ARRAYS1_C_IDL)));
2

    
3
; Arrays1_A_ex
4
(declare-var Arrays1_A_ex.idArrays1_Arrays1_1 Int)
5
(declare-var Arrays1_A_ex.isInner Bool)
6
(declare-var Arrays1_A_ex.idArrays1_Arrays1 Int)
7
(declare-var Arrays1_A_ex.idArrays1_Arrays1_2 Int)
8
(declare-rel Arrays1_A_ex (Int Bool Int))
9
(rule (=> 
10
  (and (and (or (not (= (not Arrays1_A_ex.isInner) true))
11
               (= Arrays1_A_ex.idArrays1_Arrays1_2 0))
12
            (or (not (= (not Arrays1_A_ex.isInner) false))
13
               (= Arrays1_A_ex.idArrays1_Arrays1_2 Arrays1_A_ex.idArrays1_Arrays1_1))
14
       )
15
       (= Arrays1_A_ex.idArrays1_Arrays1 Arrays1_A_ex.idArrays1_Arrays1_1)
16
       )
17
  (Arrays1_A_ex Arrays1_A_ex.idArrays1_Arrays1_1 Arrays1_A_ex.isInner Arrays1_A_ex.idArrays1_Arrays1)
18
))
19

    
20
; Arrays1_B_en
21
(declare-var Arrays1_B_en.idArrays1_Arrays1_1 Int)
22
(declare-var Arrays1_B_en.x_2_1 Int)
23
(declare-var Arrays1_B_en.isInner Bool)
24
(declare-var Arrays1_B_en.idArrays1_Arrays1 Int)
25
(declare-var Arrays1_B_en.x_2 Int)
26
(declare-var Arrays1_B_en.x_2_2 Int)
27
(declare-rel Arrays1_B_en (Int Int Bool Int Int))
28
(rule (=> 
29
  (and (and (or (not (= (not Arrays1_B_en.isInner) true))
30
               (= Arrays1_B_en.x_2_2 (+ Arrays1_B_en.x_2_1 1)))
31
            (or (not (= (not Arrays1_B_en.isInner) false))
32
               (= Arrays1_B_en.x_2_2 Arrays1_B_en.x_2_1))
33
       )
34
       (= Arrays1_B_en.x_2 Arrays1_B_en.x_2_2)
35
       (= Arrays1_B_en.idArrays1_Arrays1 512)
36
       )
37
  (Arrays1_B_en Arrays1_B_en.idArrays1_Arrays1_1 Arrays1_B_en.x_2_1 Arrays1_B_en.isInner Arrays1_B_en.idArrays1_Arrays1 Arrays1_B_en.x_2)
38
))
39

    
40
; Arrays1_B_ex
41
(declare-var Arrays1_B_ex.idArrays1_Arrays1_1 Int)
42
(declare-var Arrays1_B_ex.isInner Bool)
43
(declare-var Arrays1_B_ex.idArrays1_Arrays1 Int)
44
(declare-var Arrays1_B_ex.idArrays1_Arrays1_2 Int)
45
(declare-rel Arrays1_B_ex (Int Bool Int))
46
(rule (=> 
47
  (and (and (or (not (= (not Arrays1_B_ex.isInner) true))
48
               (= Arrays1_B_ex.idArrays1_Arrays1_2 0))
49
            (or (not (= (not Arrays1_B_ex.isInner) false))
50
               (= Arrays1_B_ex.idArrays1_Arrays1_2 Arrays1_B_ex.idArrays1_Arrays1_1))
51
       )
52
       (= Arrays1_B_ex.idArrays1_Arrays1 Arrays1_B_ex.idArrays1_Arrays1_1)
53
       )
54
  (Arrays1_B_ex Arrays1_B_ex.idArrays1_Arrays1_1 Arrays1_B_ex.isInner Arrays1_B_ex.idArrays1_Arrays1)
55
))
56

    
57
; Arrays1_C_en
58
(declare-var Arrays1_C_en.idArrays1_Arrays1_1 Int)
59
(declare-var Arrays1_C_en.x_3_1 Int)
60
(declare-var Arrays1_C_en.isInner Bool)
61
(declare-var Arrays1_C_en.idArrays1_Arrays1 Int)
62
(declare-var Arrays1_C_en.x_3 Int)
63
(declare-var Arrays1_C_en.x_3_2 Int)
64
(declare-rel Arrays1_C_en (Int Int Bool Int Int))
65
(rule (=> 
66
  (and (and (or (not (= (not Arrays1_C_en.isInner) true))
67
               (= Arrays1_C_en.x_3_2 (+ Arrays1_C_en.x_3_1 1)))
68
            (or (not (= (not Arrays1_C_en.isInner) false))
69
               (= Arrays1_C_en.x_3_2 Arrays1_C_en.x_3_1))
70
       )
71
       (= Arrays1_C_en.x_3 Arrays1_C_en.x_3_2)
72
       (= Arrays1_C_en.idArrays1_Arrays1 513)
73
       )
74
  (Arrays1_C_en Arrays1_C_en.idArrays1_Arrays1_1 Arrays1_C_en.x_3_1 Arrays1_C_en.isInner Arrays1_C_en.idArrays1_Arrays1 Arrays1_C_en.x_3)
75
))
76

    
77
; Arrays1_A_en
78
(declare-var Arrays1_A_en.idArrays1_Arrays1_1 Int)
79
(declare-var Arrays1_A_en.x_1_1 Int)
80
(declare-var Arrays1_A_en.isInner Bool)
81
(declare-var Arrays1_A_en.idArrays1_Arrays1 Int)
82
(declare-var Arrays1_A_en.x_1 Int)
83
(declare-var Arrays1_A_en.x_1_2 Int)
84
(declare-rel Arrays1_A_en (Int Int Bool Int Int))
85
(rule (=> 
86
  (and (and (or (not (= (not Arrays1_A_en.isInner) true))
87
               (= Arrays1_A_en.x_1_2 (+ Arrays1_A_en.x_1_1 1)))
88
            (or (not (= (not Arrays1_A_en.isInner) false))
89
               (= Arrays1_A_en.x_1_2 Arrays1_A_en.x_1_1))
90
       )
91
       (= Arrays1_A_en.x_1 Arrays1_A_en.x_1_2)
92
       (= Arrays1_A_en.idArrays1_Arrays1 511)
93
       )
94
  (Arrays1_A_en Arrays1_A_en.idArrays1_Arrays1_1 Arrays1_A_en.x_1_1 Arrays1_A_en.isInner Arrays1_A_en.idArrays1_Arrays1 Arrays1_A_en.x_1)
95
))
96

    
97
; Arrays1_C_ex
98
(declare-var Arrays1_C_ex.idArrays1_Arrays1_1 Int)
99
(declare-var Arrays1_C_ex.isInner Bool)
100
(declare-var Arrays1_C_ex.idArrays1_Arrays1 Int)
101
(declare-var Arrays1_C_ex.idArrays1_Arrays1_2 Int)
102
(declare-rel Arrays1_C_ex (Int Bool Int))
103
(rule (=> 
104
  (and (and (or (not (= (not Arrays1_C_ex.isInner) true))
105
               (= Arrays1_C_ex.idArrays1_Arrays1_2 0))
106
            (or (not (= (not Arrays1_C_ex.isInner) false))
107
               (= Arrays1_C_ex.idArrays1_Arrays1_2 Arrays1_C_ex.idArrays1_Arrays1_1))
108
       )
109
       (= Arrays1_C_ex.idArrays1_Arrays1 Arrays1_C_ex.idArrays1_Arrays1_1)
110
       )
111
  (Arrays1_C_ex Arrays1_C_ex.idArrays1_Arrays1_1 Arrays1_C_ex.isInner Arrays1_C_ex.idArrays1_Arrays1)
112
))
113

    
114
; arrays1_arrays1__ARRAYS1_A_IDL_handler_until
115
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1_1 Int)
116
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1_1 Int)
117
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2_1 Int)
118
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3_1 Int)
119
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__restart_in Bool)
120
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
121
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1_out Int)
122
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1_out Int)
123
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2_out Int)
124
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3_out Int)
125
(declare-rel arrays1_arrays1__ARRAYS1_A_IDL_handler_until (Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
126
(rule (=> 
127
  (and (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3_out arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3_1)
128
       (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2_out arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2_1)
129
       (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1_out arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1_1)
130
       (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1_1)
131
       (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1)
132
       (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__restart_in true)
133
       )
134
  (arrays1_arrays1__ARRAYS1_A_IDL_handler_until arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1_1 arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1_1 arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2_1 arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3_1 arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1_out arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2_out arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3_out)
135
))
136

    
137
; arrays1_arrays1__ARRAYS1_A_IDL_unless
138
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__restart_in Bool)
139
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__state_in arrays1_arrays1__type)
140
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__restart_act Bool)
141
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
142
(declare-rel arrays1_arrays1__ARRAYS1_A_IDL_unless (Bool arrays1_arrays1__type Bool arrays1_arrays1__type))
143
(rule (=> 
144
  (and (= arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__state_act arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__state_in)
145
       (= arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__restart_in)
146
       )
147
  (arrays1_arrays1__ARRAYS1_A_IDL_unless arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__state_act)
148
))
149

    
150
; arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until
151
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_1 Int)
152
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_1_1 Int)
153
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_1 Int)
154
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_3_1 Int)
155
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__restart_in Bool)
156
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
157
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_out Int)
158
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_1_out Int)
159
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_out Int)
160
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_3_out Int)
161
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_2 Int)
162
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_3 Int)
163
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_2 Int)
164
(declare-rel arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until (Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
165
(rule (=> 
166
  (and (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_3_out arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_3_1)
167
       (Arrays1_A_ex arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_1
168
                     false
169
                     arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_2)
170
       (Arrays1_B_en arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_2
171
                     arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_1
172
                     false
173
                     arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_3
174
                     arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_2)
175
       (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_out arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_2)
176
       (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_1_out arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_1_1)
177
       (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_3)
178
       (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1)
179
       (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__restart_in true)
180
       )
181
  (arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_1 arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_1_1 arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_1 arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_3_1 arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_1_out arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_out arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_3_out)
182
))
183

    
184
; arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless
185
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__restart_in Bool)
186
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__state_in arrays1_arrays1__type)
187
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__restart_act Bool)
188
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
189
(declare-rel arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless (Bool arrays1_arrays1__type Bool arrays1_arrays1__type))
190
(rule (=> 
191
  (and (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__state_act arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__state_in)
192
       (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__restart_in)
193
       )
194
  (arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__state_act)
195
))
196

    
197
; arrays1_arrays1__ARRAYS1_B_IDL_handler_until
198
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1_1 Int)
199
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1_1 Int)
200
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2_1 Int)
201
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3_1 Int)
202
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__restart_in Bool)
203
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
204
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1_out Int)
205
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1_out Int)
206
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2_out Int)
207
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3_out Int)
208
(declare-rel arrays1_arrays1__ARRAYS1_B_IDL_handler_until (Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
209
(rule (=> 
210
  (and (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3_out arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3_1)
211
       (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2_out arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2_1)
212
       (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1_out arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1_1)
213
       (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1_1)
214
       (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1)
215
       (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__restart_in true)
216
       )
217
  (arrays1_arrays1__ARRAYS1_B_IDL_handler_until arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1_1 arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1_1 arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2_1 arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3_1 arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1_out arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2_out arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3_out)
218
))
219

    
220
; arrays1_arrays1__ARRAYS1_B_IDL_unless
221
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__restart_in Bool)
222
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__state_in arrays1_arrays1__type)
223
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__restart_act Bool)
224
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
225
(declare-rel arrays1_arrays1__ARRAYS1_B_IDL_unless (Bool arrays1_arrays1__type Bool arrays1_arrays1__type))
226
(rule (=> 
227
  (and (= arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__state_act arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__state_in)
228
       (= arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__restart_in)
229
       )
230
  (arrays1_arrays1__ARRAYS1_B_IDL_unless arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__state_act)
231
))
232

    
233
; arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until
234
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_1 Int)
235
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_1_1 Int)
236
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_2_1 Int)
237
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_1 Int)
238
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__restart_in Bool)
239
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
240
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_out Int)
241
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_1_out Int)
242
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_2_out Int)
243
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_out Int)
244
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_2 Int)
245
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_3 Int)
246
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_2 Int)
247
(declare-rel arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until (Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
248
(rule (=> 
249
  (and (Arrays1_B_ex arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_1
250
                     false
251
                     arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_2)
252
       (Arrays1_C_en arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_2
253
                     arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_1
254
                     false
255
                     arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_3
256
                     arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_2)
257
       (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_out arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_2)
258
       (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_2_out arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_2_1)
259
       (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_1_out arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_1_1)
260
       (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_3)
261
       (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1)
262
       (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__restart_in true)
263
       )
264
  (arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_1 arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_1_1 arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_2_1 arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_1 arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_1_out arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_2_out arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_out)
265
))
266

    
267
; arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless
268
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__restart_in Bool)
269
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__state_in arrays1_arrays1__type)
270
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__restart_act Bool)
271
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
272
(declare-rel arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless (Bool arrays1_arrays1__type Bool arrays1_arrays1__type))
273
(rule (=> 
274
  (and (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__state_act arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__state_in)
275
       (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__restart_in)
276
       )
277
  (arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__state_act)
278
))
279

    
280
; arrays1_arrays1__ARRAYS1_C_IDL_handler_until
281
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1_1 Int)
282
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1_1 Int)
283
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2_1 Int)
284
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3_1 Int)
285
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__restart_in Bool)
286
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
287
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1_out Int)
288
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1_out Int)
289
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2_out Int)
290
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3_out Int)
291
(declare-rel arrays1_arrays1__ARRAYS1_C_IDL_handler_until (Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
292
(rule (=> 
293
  (and (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3_out arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3_1)
294
       (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2_out arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2_1)
295
       (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1_out arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1_1)
296
       (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1_1)
297
       (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1)
298
       (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__restart_in true)
299
       )
300
  (arrays1_arrays1__ARRAYS1_C_IDL_handler_until arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1_1 arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1_1 arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2_1 arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3_1 arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1_out arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2_out arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3_out)
301
))
302

    
303
; arrays1_arrays1__ARRAYS1_C_IDL_unless
304
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__restart_in Bool)
305
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__state_in arrays1_arrays1__type)
306
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__restart_act Bool)
307
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
308
(declare-rel arrays1_arrays1__ARRAYS1_C_IDL_unless (Bool arrays1_arrays1__type Bool arrays1_arrays1__type))
309
(rule (=> 
310
  (and (= arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__state_act arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__state_in)
311
       (= arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__restart_in)
312
       )
313
  (arrays1_arrays1__ARRAYS1_C_IDL_unless arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__state_act)
314
))
315

    
316
; arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until
317
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_1 Int)
318
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_1 Int)
319
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_2_1 Int)
320
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_3_1 Int)
321
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_in Bool)
322
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
323
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_out Int)
324
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_out Int)
325
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_2_out Int)
326
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_3_out Int)
327
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_2 Int)
328
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_3 Int)
329
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_2 Int)
330
(declare-rel arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until (Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
331
(rule (=> 
332
  (and (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_3_out arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_3_1)
333
       (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_2_out arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_2_1)
334
       (Arrays1_C_ex arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_1
335
                     false
336
                     arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_2)
337
       (Arrays1_A_en arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_2
338
                     arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_1
339
                     false
340
                     arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_3
341
                     arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_2)
342
       (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_out arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_2)
343
       (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_3)
344
       (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1)
345
       (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_in true)
346
       )
347
  (arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_1 arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_1 arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_2_1 arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_3_1 arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_out arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_2_out arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_3_out)
348
))
349

    
350
; arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless
351
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_in Bool)
352
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_in arrays1_arrays1__type)
353
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_act Bool)
354
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
355
(declare-rel arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless (Bool arrays1_arrays1__type Bool arrays1_arrays1__type))
356
(rule (=> 
357
  (and (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_act arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_in)
358
       (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_in)
359
       )
360
  (arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_act)
361
))
362

    
363
; arrays1_arrays1__POINTArrays1_Arrays1_handler_until
364
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1_1 Int)
365
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1_1 Int)
366
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2_1 Int)
367
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3_1 Int)
368
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.arrays1_arrays1__restart_in Bool)
369
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
370
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1_out Int)
371
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1_out Int)
372
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2_out Int)
373
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3_out Int)
374
(declare-rel arrays1_arrays1__POINTArrays1_Arrays1_handler_until (Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
375
(rule (=> 
376
  (and (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3_out arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3_1)
377
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2_out arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2_1)
378
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1_out arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1_1)
379
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1_1)
380
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1)
381
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.arrays1_arrays1__restart_in false)
382
       )
383
  (arrays1_arrays1__POINTArrays1_Arrays1_handler_until arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1_1 arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1_1 arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2_1 arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3_1 arrays1_arrays1__POINTArrays1_Arrays1_handler_until.arrays1_arrays1__restart_in arrays1_arrays1__POINTArrays1_Arrays1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1_out arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2_out arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3_out)
384
))
385

    
386
; arrays1_arrays1__POINTArrays1_Arrays1_unless
387
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_in Bool)
388
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_in arrays1_arrays1__type)
389
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 Int)
390
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.E Bool)
391
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act Bool)
392
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
393
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_1 Bool)
394
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_2 Bool)
395
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_3 Bool)
396
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_4 Bool)
397
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_5 Bool)
398
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_6 Bool)
399
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_7 Bool)
400
(declare-rel arrays1_arrays1__POINTArrays1_Arrays1_unless (Bool arrays1_arrays1__type Int Bool Bool arrays1_arrays1__type))
401
(rule (=> 
402
  (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_7 (= arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 513))
403
       (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_6 (= arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 512))
404
       (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_5 (= arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 511))
405
       (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_4 (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 513) arrays1_arrays1__POINTArrays1_Arrays1_unless.E))
406
       (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_3 (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 512) arrays1_arrays1__POINTArrays1_Arrays1_unless.E))
407
       (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_2 (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 511) arrays1_arrays1__POINTArrays1_Arrays1_unless.E))
408
       (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_1 (= arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 0))
409
       (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_1 false))
410
               (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_2 false))
411
                       (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_3 false))
412
                               (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_4 false))
413
                                       (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_5 false))
414
                                               (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_6 false))
415
                                                       (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_7 false))
416
                                                               (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_in)
417
                                                                    (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_in)
418
                                                                    ))
419
                                                            (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_7 true))
420
                                                               (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act ARRAYS1_C_IDL)
421
                                                                    (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
422
                                                                    ))
423
                                                       ))
424
                                                    (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_6 true))
425
                                                       (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act ARRAYS1_B_IDL)
426
                                                            (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
427
                                                            ))
428
                                               ))
429
                                            (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_5 true))
430
                                               (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act ARRAYS1_A_IDL)
431
                                                    (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
432
                                                    ))
433
                                       ))
434
                                    (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_4 true))
435
                                       (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act ARRAYS1_C__TO__ARRAYS1_A_1)
436
                                            (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
437
                                            ))
438
                               ))
439
                            (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_3 true))
440
                               (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act ARRAYS1_B__TO__ARRAYS1_C_1)
441
                                    (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
442
                                    ))
443
                       ))
444
                    (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_2 true))
445
                       (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act ARRAYS1_A__TO__ARRAYS1_B_1)
446
                            (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
447
                            ))
448
               ))
449
            (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_1 true))
450
               (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act POINT__TO__ARRAYS1_A_1)
451
                    (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
452
                    ))
453
       )
454
       )
455
  (arrays1_arrays1__POINTArrays1_Arrays1_unless arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_in arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_in arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 arrays1_arrays1__POINTArrays1_Arrays1_unless.E arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act)
456
))
457

    
458
; arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until
459
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_1 Int)
460
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1_1 Int)
461
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_2_1 Int)
462
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_3_1 Int)
463
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_in Bool)
464
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
465
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_out Int)
466
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1_out Int)
467
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_2_out Int)
468
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_3_out Int)
469
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_2 Int)
470
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1_2 Int)
471
(declare-rel arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until (Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
472
(rule (=> 
473
  (and (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_3_out arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_3_1)
474
       (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_2_out arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_2_1)
475
       (Arrays1_A_en arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_1
476
                     arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1_1
477
                     false
478
                     arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_2
479
                     arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1_2)
480
       (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1_out arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1_2)
481
       (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_2)
482
       (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1)
483
       (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_in true)
484
       )
485
  (arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_1 arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1_1 arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_2_1 arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_3_1 arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_in arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1_out arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_2_out arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_3_out)
486
))
487

    
488
; arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless
489
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_in Bool)
490
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_in arrays1_arrays1__type)
491
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_act Bool)
492
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
493
(declare-rel arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless (Bool arrays1_arrays1__type Bool arrays1_arrays1__type))
494
(rule (=> 
495
  (and (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_act arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_in)
496
       (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_act arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_in)
497
       )
498
  (arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_in arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_in arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_act arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_act)
499
))
500

    
501
; Arrays1_Arrays1_node
502
(declare-var Arrays1_Arrays1_node.idArrays1_Arrays1_1 Int)
503
(declare-var Arrays1_Arrays1_node.x_1_1 Int)
504
(declare-var Arrays1_Arrays1_node.E Bool)
505
(declare-var Arrays1_Arrays1_node.x_2_1 Int)
506
(declare-var Arrays1_Arrays1_node.x_3_1 Int)
507
(declare-var Arrays1_Arrays1_node.idArrays1_Arrays1 Int)
508
(declare-var Arrays1_Arrays1_node.x_1 Int)
509
(declare-var Arrays1_Arrays1_node.x_2 Int)
510
(declare-var Arrays1_Arrays1_node.x_3 Int)
511
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c Bool)
512
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c arrays1_arrays1__type)
513
(declare-var Arrays1_Arrays1_node.ni_4._arrow._first_c Bool)
514
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m Bool)
515
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m arrays1_arrays1__type)
516
(declare-var Arrays1_Arrays1_node.ni_4._arrow._first_m Bool)
517
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_x Bool)
518
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_x arrays1_arrays1__type)
519
(declare-var Arrays1_Arrays1_node.ni_4._arrow._first_x Bool)
520
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_1 Bool)
521
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_10 arrays1_arrays1__type)
522
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_11 Bool)
523
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_12 arrays1_arrays1__type)
524
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_13 Bool)
525
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_14 arrays1_arrays1__type)
526
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_15 Bool)
527
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_16 arrays1_arrays1__type)
528
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_17 Bool)
529
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_18 arrays1_arrays1__type)
530
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_19 Int)
531
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_2 arrays1_arrays1__type)
532
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_20 Int)
533
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_21 Int)
534
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_22 Int)
535
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_23 Bool)
536
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_24 arrays1_arrays1__type)
537
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_25 Int)
538
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_26 Int)
539
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_27 Int)
540
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_28 Int)
541
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_29 Bool)
542
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_3 Bool)
543
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_30 arrays1_arrays1__type)
544
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_31 Int)
545
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_32 Int)
546
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_33 Int)
547
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_34 Int)
548
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_35 Bool)
549
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_36 arrays1_arrays1__type)
550
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_37 Int)
551
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_38 Int)
552
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_39 Int)
553
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_4 arrays1_arrays1__type)
554
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_40 Int)
555
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_41 Bool)
556
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_42 arrays1_arrays1__type)
557
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_43 Int)
558
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_44 Int)
559
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_45 Int)
560
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_46 Int)
561
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_47 Bool)
562
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_48 arrays1_arrays1__type)
563
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_49 Int)
564
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_5 Bool)
565
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_50 Int)
566
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_51 Int)
567
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_52 Int)
568
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_53 Bool)
569
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_54 arrays1_arrays1__type)
570
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_55 Int)
571
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_56 Int)
572
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_57 Int)
573
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_58 Int)
574
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_59 Bool)
575
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_6 arrays1_arrays1__type)
576
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_60 arrays1_arrays1__type)
577
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_61 Int)
578
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_62 Int)
579
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_63 Int)
580
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_64 Int)
581
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_65 Bool)
582
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_7 Bool)
583
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_8 arrays1_arrays1__type)
584
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_9 Bool)
585
(declare-var Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in Bool)
586
(declare-var Arrays1_Arrays1_node.arrays1_arrays1__next_state_in arrays1_arrays1__type)
587
(declare-var Arrays1_Arrays1_node.arrays1_arrays1__restart_act Bool)
588
(declare-var Arrays1_Arrays1_node.arrays1_arrays1__restart_in Bool)
589
(declare-var Arrays1_Arrays1_node.arrays1_arrays1__state_act arrays1_arrays1__type)
590
(declare-var Arrays1_Arrays1_node.arrays1_arrays1__state_in arrays1_arrays1__type)
591
(declare-rel Arrays1_Arrays1_node_reset (Bool arrays1_arrays1__type Bool Bool arrays1_arrays1__type Bool))
592
(declare-rel Arrays1_Arrays1_node_step (Int Int Bool Int Int Int Int Int Int Bool arrays1_arrays1__type Bool Bool arrays1_arrays1__type Bool))
593

    
594
(rule (=> 
595
  (and 
596
       (= Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c)
597
       (= Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c)
598
       (= Arrays1_Arrays1_node.ni_4._arrow._first_m true)
599
  )
600
  (Arrays1_Arrays1_node_reset Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c
601
                              Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c
602
                              Arrays1_Arrays1_node.ni_4._arrow._first_c
603
                              Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m
604
                              Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m
605
                              Arrays1_Arrays1_node.ni_4._arrow._first_m)
606
))
607

    
608
(rule (=> 
609
  (and (= Arrays1_Arrays1_node.ni_4._arrow._first_m Arrays1_Arrays1_node.ni_4._arrow._first_c)
610
       (and (= Arrays1_Arrays1_node.__Arrays1_Arrays1_node_65 (ite Arrays1_Arrays1_node.ni_4._arrow._first_m true false))
611
            (= Arrays1_Arrays1_node.ni_4._arrow._first_x false))
612
       (and (or (not (= Arrays1_Arrays1_node.__Arrays1_Arrays1_node_65 false))
613
               (and (= Arrays1_Arrays1_node.arrays1_arrays1__state_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c)
614
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c)
615
                    ))
616
            (or (not (= Arrays1_Arrays1_node.__Arrays1_Arrays1_node_65 true))
617
               (and (= Arrays1_Arrays1_node.arrays1_arrays1__state_in POINTArrays1_Arrays1)
618
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_in false)
619
                    ))
620
       )
621
       (and (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_in ARRAYS1_A_IDL))
622
               (and (arrays1_arrays1__ARRAYS1_A_IDL_unless Arrays1_Arrays1_node.arrays1_arrays1__restart_in
623
                                                           Arrays1_Arrays1_node.arrays1_arrays1__state_in
624
                                                           Arrays1_Arrays1_node.__Arrays1_Arrays1_node_5
625
                                                           Arrays1_Arrays1_node.__Arrays1_Arrays1_node_6)
626
                    (= Arrays1_Arrays1_node.arrays1_arrays1__state_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_6)
627
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_5)
628
                    ))
629
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_in ARRAYS1_A__TO__ARRAYS1_B_1))
630
               (and (arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless 
631
                    Arrays1_Arrays1_node.arrays1_arrays1__restart_in
632
                    Arrays1_Arrays1_node.arrays1_arrays1__state_in
633
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_11
634
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_12)
635
                    (= Arrays1_Arrays1_node.arrays1_arrays1__state_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_12)
636
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_11)
637
                    ))
638
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_in ARRAYS1_B_IDL))
639
               (and (arrays1_arrays1__ARRAYS1_B_IDL_unless Arrays1_Arrays1_node.arrays1_arrays1__restart_in
640
                                                           Arrays1_Arrays1_node.arrays1_arrays1__state_in
641
                                                           Arrays1_Arrays1_node.__Arrays1_Arrays1_node_3
642
                                                           Arrays1_Arrays1_node.__Arrays1_Arrays1_node_4)
643
                    (= Arrays1_Arrays1_node.arrays1_arrays1__state_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_4)
644
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_3)
645
                    ))
646
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_in ARRAYS1_B__TO__ARRAYS1_C_1))
647
               (and (arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless 
648
                    Arrays1_Arrays1_node.arrays1_arrays1__restart_in
649
                    Arrays1_Arrays1_node.arrays1_arrays1__state_in
650
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_9
651
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_10)
652
                    (= Arrays1_Arrays1_node.arrays1_arrays1__state_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_10)
653
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_9)
654
                    ))
655
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_in ARRAYS1_C_IDL))
656
               (and (arrays1_arrays1__ARRAYS1_C_IDL_unless Arrays1_Arrays1_node.arrays1_arrays1__restart_in
657
                                                           Arrays1_Arrays1_node.arrays1_arrays1__state_in
658
                                                           Arrays1_Arrays1_node.__Arrays1_Arrays1_node_1
659
                                                           Arrays1_Arrays1_node.__Arrays1_Arrays1_node_2)
660
                    (= Arrays1_Arrays1_node.arrays1_arrays1__state_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_2)
661
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_1)
662
                    ))
663
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_in ARRAYS1_C__TO__ARRAYS1_A_1))
664
               (and (arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless 
665
                    Arrays1_Arrays1_node.arrays1_arrays1__restart_in
666
                    Arrays1_Arrays1_node.arrays1_arrays1__state_in
667
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_7
668
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_8)
669
                    (= Arrays1_Arrays1_node.arrays1_arrays1__state_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_8)
670
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_7)
671
                    ))
672
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_in POINTArrays1_Arrays1))
673
               (and (arrays1_arrays1__POINTArrays1_Arrays1_unless Arrays1_Arrays1_node.arrays1_arrays1__restart_in
674
                                                                  Arrays1_Arrays1_node.arrays1_arrays1__state_in
675
                                                                  Arrays1_Arrays1_node.idArrays1_Arrays1_1
676
                                                                  Arrays1_Arrays1_node.E
677
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_15
678
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_16)
679
                    (= Arrays1_Arrays1_node.arrays1_arrays1__state_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_16)
680
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_15)
681
                    ))
682
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_in POINT__TO__ARRAYS1_A_1))
683
               (and (arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless Arrays1_Arrays1_node.arrays1_arrays1__restart_in
684
                                                                    Arrays1_Arrays1_node.arrays1_arrays1__state_in
685
                                                                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_13
686
                                                                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_14)
687
                    (= Arrays1_Arrays1_node.arrays1_arrays1__state_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_14)
688
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_13)
689
                    ))
690
       )
691
       (and (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_act ARRAYS1_A_IDL))
692
               (and (arrays1_arrays1__ARRAYS1_A_IDL_handler_until Arrays1_Arrays1_node.idArrays1_Arrays1_1
693
                                                                  Arrays1_Arrays1_node.x_1_1
694
                                                                  Arrays1_Arrays1_node.x_2_1
695
                                                                  Arrays1_Arrays1_node.x_3_1
696
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_29
697
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_30
698
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_31
699
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_32
700
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_33
701
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_34)
702
                    (= Arrays1_Arrays1_node.x_3 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_34)
703
                    (= Arrays1_Arrays1_node.x_2 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_33)
704
                    (= Arrays1_Arrays1_node.x_1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_32)
705
                    (= Arrays1_Arrays1_node.idArrays1_Arrays1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_31)
706
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_state_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_30)
707
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_29)
708
                    ))
709
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_act ARRAYS1_A__TO__ARRAYS1_B_1))
710
               (and (arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until 
711
                    Arrays1_Arrays1_node.idArrays1_Arrays1_1
712
                    Arrays1_Arrays1_node.x_1_1
713
                    Arrays1_Arrays1_node.x_2_1
714
                    Arrays1_Arrays1_node.x_3_1
715
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_47
716
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_48
717
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_49
718
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_50
719
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_51
720
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_52)
721
                    (= Arrays1_Arrays1_node.x_3 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_52)
722
                    (= Arrays1_Arrays1_node.x_2 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_51)
723
                    (= Arrays1_Arrays1_node.x_1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_50)
724
                    (= Arrays1_Arrays1_node.idArrays1_Arrays1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_49)
725
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_state_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_48)
726
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_47)
727
                    ))
728
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_act ARRAYS1_B_IDL))
729
               (and (arrays1_arrays1__ARRAYS1_B_IDL_handler_until Arrays1_Arrays1_node.idArrays1_Arrays1_1
730
                                                                  Arrays1_Arrays1_node.x_1_1
731
                                                                  Arrays1_Arrays1_node.x_2_1
732
                                                                  Arrays1_Arrays1_node.x_3_1
733
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_23
734
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_24
735
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_25
736
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_26
737
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_27
738
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_28)
739
                    (= Arrays1_Arrays1_node.x_3 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_28)
740
                    (= Arrays1_Arrays1_node.x_2 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_27)
741
                    (= Arrays1_Arrays1_node.x_1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_26)
742
                    (= Arrays1_Arrays1_node.idArrays1_Arrays1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_25)
743
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_state_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_24)
744
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_23)
745
                    ))
746
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_act ARRAYS1_B__TO__ARRAYS1_C_1))
747
               (and (arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until 
748
                    Arrays1_Arrays1_node.idArrays1_Arrays1_1
749
                    Arrays1_Arrays1_node.x_1_1
750
                    Arrays1_Arrays1_node.x_2_1
751
                    Arrays1_Arrays1_node.x_3_1
752
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_41
753
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_42
754
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_43
755
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_44
756
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_45
757
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_46)
758
                    (= Arrays1_Arrays1_node.x_3 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_46)
759
                    (= Arrays1_Arrays1_node.x_2 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_45)
760
                    (= Arrays1_Arrays1_node.x_1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_44)
761
                    (= Arrays1_Arrays1_node.idArrays1_Arrays1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_43)
762
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_state_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_42)
763
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_41)
764
                    ))
765
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_act ARRAYS1_C_IDL))
766
               (and (arrays1_arrays1__ARRAYS1_C_IDL_handler_until Arrays1_Arrays1_node.idArrays1_Arrays1_1
767
                                                                  Arrays1_Arrays1_node.x_1_1
768
                                                                  Arrays1_Arrays1_node.x_2_1
769
                                                                  Arrays1_Arrays1_node.x_3_1
770
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_17
771
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_18
772
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_19
773
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_20
774
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_21
775
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_22)
776
                    (= Arrays1_Arrays1_node.x_3 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_22)
777
                    (= Arrays1_Arrays1_node.x_2 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_21)
778
                    (= Arrays1_Arrays1_node.x_1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_20)
779
                    (= Arrays1_Arrays1_node.idArrays1_Arrays1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_19)
780
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_state_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_18)
781
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_17)
782
                    ))
783
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_act ARRAYS1_C__TO__ARRAYS1_A_1))
784
               (and (arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until 
785
                    Arrays1_Arrays1_node.idArrays1_Arrays1_1
786
                    Arrays1_Arrays1_node.x_1_1
787
                    Arrays1_Arrays1_node.x_2_1
788
                    Arrays1_Arrays1_node.x_3_1
789
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_35
790
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_36
791
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_37
792
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_38
793
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_39
794
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_40)
795
                    (= Arrays1_Arrays1_node.x_3 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_40)
796
                    (= Arrays1_Arrays1_node.x_2 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_39)
797
                    (= Arrays1_Arrays1_node.x_1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_38)
798
                    (= Arrays1_Arrays1_node.idArrays1_Arrays1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_37)
799
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_state_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_36)
800
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_35)
801
                    ))
802
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_act POINTArrays1_Arrays1))
803
               (and (arrays1_arrays1__POINTArrays1_Arrays1_handler_until 
804
                    Arrays1_Arrays1_node.idArrays1_Arrays1_1
805
                    Arrays1_Arrays1_node.x_1_1
806
                    Arrays1_Arrays1_node.x_2_1
807
                    Arrays1_Arrays1_node.x_3_1
808
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_59
809
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_60
810
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_61
811
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_62
812
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_63
813
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_64)
814
                    (= Arrays1_Arrays1_node.x_3 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_64)
815
                    (= Arrays1_Arrays1_node.x_2 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_63)
816
                    (= Arrays1_Arrays1_node.x_1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_62)
817
                    (= Arrays1_Arrays1_node.idArrays1_Arrays1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_61)
818
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_state_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_60)
819
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_59)
820
                    ))
821
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_act POINT__TO__ARRAYS1_A_1))
822
               (and (arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until 
823
                    Arrays1_Arrays1_node.idArrays1_Arrays1_1
824
                    Arrays1_Arrays1_node.x_1_1
825
                    Arrays1_Arrays1_node.x_2_1
826
                    Arrays1_Arrays1_node.x_3_1
827
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_53
828
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_54
829
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_55
830
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_56
831
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_57
832
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_58)
833
                    (= Arrays1_Arrays1_node.x_3 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_58)
834
                    (= Arrays1_Arrays1_node.x_2 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_57)
835
                    (= Arrays1_Arrays1_node.x_1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_56)
836
                    (= Arrays1_Arrays1_node.idArrays1_Arrays1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_55)
837
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_state_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_54)
838
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_53)
839
                    ))
840
       )
841
       (= Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_x Arrays1_Arrays1_node.arrays1_arrays1__next_state_in)
842
       (= Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_x Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in)
843
       )
844
  (Arrays1_Arrays1_node_step Arrays1_Arrays1_node.idArrays1_Arrays1_1
845
                             Arrays1_Arrays1_node.x_1_1
846
                             Arrays1_Arrays1_node.E
847
                             Arrays1_Arrays1_node.x_2_1
848
                             Arrays1_Arrays1_node.x_3_1
849
                             Arrays1_Arrays1_node.idArrays1_Arrays1
850
                             Arrays1_Arrays1_node.x_1
851
                             Arrays1_Arrays1_node.x_2
852
                             Arrays1_Arrays1_node.x_3
853
                             Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c
854
                             Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c
855
                             Arrays1_Arrays1_node.ni_4._arrow._first_c
856
                             Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_x
857
                             Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_x
858
                             Arrays1_Arrays1_node.ni_4._arrow._first_x)
859
))
860

    
861
; Arrays1_Arrays1
862
(declare-var Arrays1_Arrays1.E Bool)
863
(declare-var Arrays1_Arrays1.x_1 Int)
864
(declare-var Arrays1_Arrays1.x_2 Int)
865
(declare-var Arrays1_Arrays1.x_3 Int)
866
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_6_c Int)
867
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_7_c Int)
868
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_8_c Int)
869
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_9_c Int)
870
(declare-var Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c Bool)
871
(declare-var Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c arrays1_arrays1__type)
872
(declare-var Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c Bool)
873
(declare-var Arrays1_Arrays1.ni_3._arrow._first_c Bool)
874
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_6_m Int)
875
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_7_m Int)
876
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_8_m Int)
877
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_9_m Int)
878
(declare-var Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m Bool)
879
(declare-var Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m arrays1_arrays1__type)
880
(declare-var Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m Bool)
881
(declare-var Arrays1_Arrays1.ni_3._arrow._first_m Bool)
882
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_6_x Int)
883
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_7_x Int)
884
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_8_x Int)
885
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_9_x Int)
886
(declare-var Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_x Bool)
887
(declare-var Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_x arrays1_arrays1__type)
888
(declare-var Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_x Bool)
889
(declare-var Arrays1_Arrays1.ni_3._arrow._first_x Bool)
890
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_1 Int)
891
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_2 Int)
892
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_3 Int)
893
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_4 Int)
894
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_5 Bool)
895
(declare-var Arrays1_Arrays1.idArrays1_Arrays1 Int)
896
(declare-var Arrays1_Arrays1.idArrays1_Arrays1_1 Int)
897
(declare-var Arrays1_Arrays1.x_1_1 Int)
898
(declare-var Arrays1_Arrays1.x_2_1 Int)
899
(declare-var Arrays1_Arrays1.x_3_1 Int)
900
(declare-rel Arrays1_Arrays1_reset (Int Int Int Int Bool arrays1_arrays1__type Bool Bool Int Int Int Int Bool arrays1_arrays1__type Bool Bool))
901
(declare-rel Arrays1_Arrays1_step (Bool Int Int Int Int Int Int Int Bool arrays1_arrays1__type Bool Bool Int Int Int Int Bool arrays1_arrays1__type Bool Bool))
902

    
903
(rule (=> 
904
  (and 
905
       (= Arrays1_Arrays1.__Arrays1_Arrays1_6_m Arrays1_Arrays1.__Arrays1_Arrays1_6_c)
906
       (= Arrays1_Arrays1.__Arrays1_Arrays1_7_m Arrays1_Arrays1.__Arrays1_Arrays1_7_c)
907
       (= Arrays1_Arrays1.__Arrays1_Arrays1_8_m Arrays1_Arrays1.__Arrays1_Arrays1_8_c)
908
       (= Arrays1_Arrays1.__Arrays1_Arrays1_9_m Arrays1_Arrays1.__Arrays1_Arrays1_9_c)
909
       (= Arrays1_Arrays1.ni_3._arrow._first_m true)
910
       (Arrays1_Arrays1_node_reset Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c
911
                                   Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c
912
                                   Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c
913
                                   Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m
914
                                   Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m
915
                                   Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m)
916
  )
917
  (Arrays1_Arrays1_reset Arrays1_Arrays1.__Arrays1_Arrays1_6_c
918
                         Arrays1_Arrays1.__Arrays1_Arrays1_7_c
919
                         Arrays1_Arrays1.__Arrays1_Arrays1_8_c
920
                         Arrays1_Arrays1.__Arrays1_Arrays1_9_c
921
                         Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c
922
                         Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c
923
                         Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c
924
                         Arrays1_Arrays1.ni_3._arrow._first_c
925
                         Arrays1_Arrays1.__Arrays1_Arrays1_6_m
926
                         Arrays1_Arrays1.__Arrays1_Arrays1_7_m
927
                         Arrays1_Arrays1.__Arrays1_Arrays1_8_m
928
                         Arrays1_Arrays1.__Arrays1_Arrays1_9_m
929
                         Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m
930
                         Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m
931
                         Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m
932
                         Arrays1_Arrays1.ni_3._arrow._first_m)
933
))
934

    
935
(rule (=> 
936
  (and (= Arrays1_Arrays1.ni_3._arrow._first_m Arrays1_Arrays1.ni_3._arrow._first_c)
937
       (and (= Arrays1_Arrays1.__Arrays1_Arrays1_5 (ite Arrays1_Arrays1.ni_3._arrow._first_m true false))
938
            (= Arrays1_Arrays1.ni_3._arrow._first_x false))
939
       (and (or (not (= Arrays1_Arrays1.__Arrays1_Arrays1_5 false))
940
               (and (= Arrays1_Arrays1.x_3_1 Arrays1_Arrays1.__Arrays1_Arrays1_7_c)
941
                    (= Arrays1_Arrays1.x_2_1 Arrays1_Arrays1.__Arrays1_Arrays1_8_c)
942
                    (= Arrays1_Arrays1.x_1_1 Arrays1_Arrays1.__Arrays1_Arrays1_9_c)
943
                    (= Arrays1_Arrays1.idArrays1_Arrays1_1 Arrays1_Arrays1.__Arrays1_Arrays1_6_c)
944
                    ))
945
            (or (not (= Arrays1_Arrays1.__Arrays1_Arrays1_5 true))
946
               (and (= Arrays1_Arrays1.x_3_1 1)
947
                    (= Arrays1_Arrays1.x_2_1 1)
948
                    (= Arrays1_Arrays1.x_1_1 1)
949
                    (= Arrays1_Arrays1.idArrays1_Arrays1_1 0)
950
                    ))
951
       )
952
       (and (= Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c)
953
            (= Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c)
954
            (= Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c)
955
            )
956
       (Arrays1_Arrays1_node_step Arrays1_Arrays1.idArrays1_Arrays1_1
957
                                  Arrays1_Arrays1.x_1_1
958
                                  Arrays1_Arrays1.E
959
                                  Arrays1_Arrays1.x_2_1
960
                                  Arrays1_Arrays1.x_3_1
961
                                  Arrays1_Arrays1.__Arrays1_Arrays1_1
962
                                  Arrays1_Arrays1.__Arrays1_Arrays1_2
963
                                  Arrays1_Arrays1.__Arrays1_Arrays1_3
964
                                  Arrays1_Arrays1.__Arrays1_Arrays1_4
965
                                  Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m
966
                                  Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m
967
                                  Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m
968
                                  Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_x
969
                                  Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_x
970
                                  Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_x)
971
       (and (or (not (= Arrays1_Arrays1.E false))
972
               (and (= Arrays1_Arrays1.x_3 Arrays1_Arrays1.x_3_1)
973
                    (= Arrays1_Arrays1.x_2 Arrays1_Arrays1.x_2_1)
974
                    (= Arrays1_Arrays1.x_1 Arrays1_Arrays1.x_1_1)
975
                    (= Arrays1_Arrays1.idArrays1_Arrays1 Arrays1_Arrays1.idArrays1_Arrays1_1)
976
                    ))
977
            (or (not (= Arrays1_Arrays1.E true))
978
               (and (= Arrays1_Arrays1.x_3 Arrays1_Arrays1.__Arrays1_Arrays1_4)
979
                    (= Arrays1_Arrays1.x_2 Arrays1_Arrays1.__Arrays1_Arrays1_3)
980
                    (= Arrays1_Arrays1.x_1 Arrays1_Arrays1.__Arrays1_Arrays1_2)
981
                    (= Arrays1_Arrays1.idArrays1_Arrays1 Arrays1_Arrays1.__Arrays1_Arrays1_1)
982
                    ))
983
       )
984
       (= Arrays1_Arrays1.__Arrays1_Arrays1_9_x Arrays1_Arrays1.x_1)
985
       (= Arrays1_Arrays1.__Arrays1_Arrays1_8_x Arrays1_Arrays1.x_2)
986
       (= Arrays1_Arrays1.__Arrays1_Arrays1_7_x Arrays1_Arrays1.x_3)
987
       (= Arrays1_Arrays1.__Arrays1_Arrays1_6_x Arrays1_Arrays1.idArrays1_Arrays1)
988
       )
989
  (Arrays1_Arrays1_step Arrays1_Arrays1.E
990
                        Arrays1_Arrays1.x_1
991
                        Arrays1_Arrays1.x_2
992
                        Arrays1_Arrays1.x_3
993
                        Arrays1_Arrays1.__Arrays1_Arrays1_6_c
994
                        Arrays1_Arrays1.__Arrays1_Arrays1_7_c
995
                        Arrays1_Arrays1.__Arrays1_Arrays1_8_c
996
                        Arrays1_Arrays1.__Arrays1_Arrays1_9_c
997
                        Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c
998
                        Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c
999
                        Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c
1000
                        Arrays1_Arrays1.ni_3._arrow._first_c
1001
                        Arrays1_Arrays1.__Arrays1_Arrays1_6_x
1002
                        Arrays1_Arrays1.__Arrays1_Arrays1_7_x
1003
                        Arrays1_Arrays1.__Arrays1_Arrays1_8_x
1004
                        Arrays1_Arrays1.__Arrays1_Arrays1_9_x
1005
                        Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_x
1006
                        Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_x
1007
                        Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_x
1008
                        Arrays1_Arrays1.ni_3._arrow._first_x)
1009
))
1010

    
1011
; Arrays1
1012
(declare-var Arrays1.E_1_1 Real)
1013
(declare-var Arrays1.x1_1_1 Int)
1014
(declare-var Arrays1.x2_2_1 Int)
1015
(declare-var Arrays1.x3_3_1 Int)
1016
(declare-var Arrays1.__Arrays1_2_c Real)
1017
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_c Int)
1018
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_c Int)
1019
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_c Int)
1020
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_c Int)
1021
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c Bool)
1022
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c arrays1_arrays1__type)
1023
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c Bool)
1024
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_c Bool)
1025
(declare-var Arrays1.ni_1._arrow._first_c Bool)
1026
(declare-var Arrays1.__Arrays1_2_m Real)
1027
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_m Int)
1028
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_m Int)
1029
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_m Int)
1030
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_m Int)
1031
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m Bool)
1032
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m arrays1_arrays1__type)
1033
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m Bool)
1034
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_m Bool)
1035
(declare-var Arrays1.ni_1._arrow._first_m Bool)
1036
(declare-var Arrays1.__Arrays1_2_x Real)
1037
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_x Int)
1038
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_x Int)
1039
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_x Int)
1040
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_x Int)
1041
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_x Bool)
1042
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_x arrays1_arrays1__type)
1043
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_x Bool)
1044
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_x Bool)
1045
(declare-var Arrays1.ni_1._arrow._first_x Bool)
1046
(declare-var Arrays1.Arrays1E_1_1_event Bool)
1047
(declare-var Arrays1.Arrays1_1_1 Int)
1048
(declare-var Arrays1.Arrays1_1_2 Int)
1049
(declare-var Arrays1.Arrays1_1_3 Int)
1050
(declare-var Arrays1.__Arrays1_1 Bool)
1051
(declare-var Arrays1.i_virtual_local Real)
1052
(declare-rel Arrays1_reset (Real Int Int Int Int Bool arrays1_arrays1__type Bool Bool Bool Real Int Int Int Int Bool arrays1_arrays1__type Bool Bool Bool))
1053
(declare-rel Arrays1_step (Real Int Int Int Real Int Int Int Int Bool arrays1_arrays1__type Bool Bool Bool Real Int Int Int Int Bool arrays1_arrays1__type Bool Bool Bool))
1054

    
1055
(rule (=> 
1056
  (and 
1057
       (= Arrays1.__Arrays1_2_m Arrays1.__Arrays1_2_c)
1058
       (= Arrays1.ni_1._arrow._first_m true)
1059
       (Arrays1_Arrays1_reset Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_c
1060
                              Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_c
1061
                              Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_c
1062
                              Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_c
1063
                              Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c
1064
                              Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c
1065
                              Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c
1066
                              Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_c
1067
                              Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_m
1068
                              Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_m
1069
                              Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_m
1070
                              Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_m
1071
                              Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m
1072
                              Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m
1073
                              Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m
1074
                              Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_m)
1075
  )
1076
  (Arrays1_reset Arrays1.__Arrays1_2_c
1077
                 Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_c
1078
                 Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_c
1079
                 Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_c
1080
                 Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_c
1081
                 Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c
1082
                 Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c
1083
                 Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c
1084
                 Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_c
1085
                 Arrays1.ni_1._arrow._first_c
1086
                 Arrays1.__Arrays1_2_m
1087
                 Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_m
1088
                 Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_m
1089
                 Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_m
1090
                 Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_m
1091
                 Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m
1092
                 Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m
1093
                 Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m
1094
                 Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_m
1095
                 Arrays1.ni_1._arrow._first_m)
1096
))
1097

    
1098
(rule (=> 
1099
  (and (= Arrays1.ni_1._arrow._first_m Arrays1.ni_1._arrow._first_c)(and (= Arrays1.__Arrays1_1 (ite Arrays1.ni_1._arrow._first_m true false))
1100
                                                                    (= Arrays1.ni_1._arrow._first_x false))
1101
       (and (or (not (= Arrays1.__Arrays1_1 true))
1102
               (= Arrays1.Arrays1E_1_1_event false))
1103
            (or (not (= Arrays1.__Arrays1_1 false))
1104
               (= Arrays1.Arrays1E_1_1_event (and (<= Arrays1.__Arrays1_2_c 0.) (> Arrays1.E_1_1 0.))))
1105
       )
1106
       (and (= Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_m Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_c)
1107
            (= Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_m Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_c)
1108
            (= Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_m Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_c)
1109
            (= Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_m Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_c)
1110
            (= Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c)
1111
            (= Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c)
1112
            (= Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c)
1113
            (= Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_m Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_c)
1114
            )
1115
       (Arrays1_Arrays1_step Arrays1.Arrays1E_1_1_event
1116
                             Arrays1.Arrays1_1_1
1117
                             Arrays1.Arrays1_1_2
1118
                             Arrays1.Arrays1_1_3
1119
                             Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_m
1120
                             Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_m
1121
                             Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_m
1122
                             Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_m
1123
                             Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m
1124
                             Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m
1125
                             Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m
1126
                             Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_m
1127
                             Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_x
1128
                             Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_x
1129
                             Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_x
1130
                             Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_x
1131
                             Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_x
1132
                             Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_x
1133
                             Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_x
1134
                             Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_x)
1135
       (= Arrays1.x3_3_1 Arrays1.Arrays1_1_3)
1136
       (= Arrays1.x2_2_1 Arrays1.Arrays1_1_2)
1137
       (= Arrays1.x1_1_1 Arrays1.Arrays1_1_1)
1138
       (and (or (not (= Arrays1.__Arrays1_1 true))
1139
               (= Arrays1.i_virtual_local 0.))
1140
            (or (not (= Arrays1.__Arrays1_1 false))
1141
               (= Arrays1.i_virtual_local 1.))
1142
       )
1143
       (= Arrays1.__Arrays1_2_x Arrays1.E_1_1)
1144
       )
1145
  (Arrays1_step Arrays1.E_1_1
1146
                Arrays1.x1_1_1
1147
                Arrays1.x2_2_1
1148
                Arrays1.x3_3_1
1149
                Arrays1.__Arrays1_2_c
1150
                Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_c
1151
                Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_c
1152
                Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_c
1153
                Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_c
1154
                Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c
1155
                Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c
1156
                Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c
1157
                Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_c
1158
                Arrays1.ni_1._arrow._first_c
1159
                Arrays1.__Arrays1_2_x
1160
                Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_x
1161
                Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_x
1162
                Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_x
1163
                Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_x
1164
                Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_x
1165
                Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_x
1166
                Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_x
1167
                Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_x
1168
                Arrays1.ni_1._arrow._first_x)
1169
))
1170