Project

General

Profile

Revision cc6eda98

View differences:

regression_tests/lustre_files/success/CMakeLists.txt
1 1
cmake_minimum_required(VERSION 2.8.4)
2 2

  
3
#add_subdirectory(Stateflow)
3
add_subdirectory(Stateflow)
4 4
add_subdirectory(Simulink)
5 5
add_subdirectory(kind_fmcad08)
6
#[[add_subdirectory(adrien)
7
add_subdirectory(automata)
6
add_subdirectory(adrien)
7
#[[add_subdirectory(automata)
8 8
add_subdirectory(clocks)
9 9
add_subdirectory(lego_robot)
10 10
add_subdirectory(linear_ctl)
regression_tests/lustre_files/success/Stateflow/CMakeLists.txt
1 1
cmake_minimum_required(VERSION 2.8.4)
2
include(FindUnixCommands)
3 2

  
4 3

  
4
set(LUSTRE_OPTIONS_OPT "" )
5
set(MAX_INPUT_VALUE 100)
5 6

  
6
#find_package(Lustre)
7

  
8
if(LUSTRE_COMPILER)
9
  message(STATUS "Found lustrec: ${LUSTRE_COMPILER} ")
10
else(LUSTRE_COMPILER)
11
  message(FATAL_ERROR "lustrec not found")
12
endif(LUSTRE_COMPILER)
13 7

  
14 8
#proceed all subdirectories
15 9
SUBDIRLIST(SUBDIRS ${CMAKE_CURRENT_SOURCE_DIR}  "src_")
16

  
17
#take all lustre files
18
set(GLOBAL_LUSTRE_FILES "")
19 10
FOREACH(subdir ${SUBDIRS})
20
  #message("${subdir}")
21
  LUSTREFILES(LFILE ${subdir} )
22
  list(APPEND GLOBAL_LUSTRE_FILES ${LFILE})
23
  get_filename_component(L ${LFILE} NAME_WE)
24
  set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/${L}")
25
  file(COPY ${LFILE} "${subdir}/input_values" "${subdir}/outputs_values"   DESTINATION  ${LUSTRE_OUTPUT_DIR})
26
ENDFOREACH()
27

  
28
#first combination :no option
29
set(LUSTRE_OPTIONS_OPT "")
30

  
31
FOREACH(lus_file ${GLOBAL_LUSTRE_FILES})
11
  LUSTREFILES(LFILES ${subdir} )
12
  set(TESTS_PREFIX "Steteflow")
13
  set(SRC_DIR "${CMAKE_CURRENT_SOURCE_DIR}/${subdir}")
14
  set(DST_DIR "${CMAKE_CURRENT_BINARY_DIR}")
15
  FOREACH(lus_file ${LFILES})
32 16
	get_filename_component(L ${lus_file} NAME_WE)
33
	set(LUSTRE_NODE_OPT  "${L}")
34
	
35
	# First command generate C files from Lustre file
36
	Lustre_Compile(LUS_FILE ${lus_file}
37
					NODE ${LUSTRE_NODE_OPT}
38
					OPTS ${LUSTRE_OPTIONS_OPT})
39
					
40
	set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
41
	add_test(NAME Stateflow_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
42
			COMMAND  ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}} 
43
			#REQUIRED_FILES ${lus_file}
17
	set(NODE_NAME  "${L}")
18
	Copy_or_generate_lusi_input_and_output_values_for_reference(
19
		LUS_FILE ${lus_file}
20
		NODE ${NODE_NAME}
21
		OPTS ${LUSTRE_OPTIONS_OPT}
22
		MAX ${MAX_INPUT_VALUE}  	#maximum value for input values.
23
		SRC_DIR ${SRC_DIR}
24
		DST_DIR ${DST_DIR}
44 25
	)
45 26

  
46
	 #********************* make -f ${L}.makefile ***************************
47
	 add_test(NAME Stateflow_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
48
			COMMAND  make -f ${L}.makefile
49
			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}}
27
	Lustre_compile_and_compare_to_reference(
28
		LUS_FILE ${lus_file}
29
		NODE ${NODE_NAME}
30
		TESTS_PREFIX ${TESTS_PREFIX}
31
		OPTS ${LUSTRE_OPTIONS_OPT}
32
		CALL_ID "1"
33
		SRC_DIR ${SRC_DIR}
34
		DST_DIR ${DST_DIR}
50 35
	)
51
	SET_TESTS_PROPERTIES ( Stateflow_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
52
	 PROPERTIES DEPENDS Stateflow_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
53
				REQUIRED_FILES ${L}.makefile
54
				)
55
	 
56
	 #************** execute C binary **********************************
57
	
58
	if (BASH)
59
		add_test(
60
			NAME Stateflow_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT} 
61
			COMMAND ${BASH} -c "./${L}_${LUSTRE_NODE_OPT} < ../input_values > ${L}_${LUSTRE_NODE_OPT}_outputs"
62
			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}}
63
		)
64
		SET_TESTS_PROPERTIES ( Stateflow_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
65
			PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}
66
				DEPENDS Stateflow_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT})
67
	else()
68
		message(FATAL_ERROR "Unknown shell command for ${CMAKE_HOST_SYSTEM_NAME}")
69
	endif()
70

  
71
	 #************** execute C binary **********************************
72
	 add_test(NAME Stateflow_DIFF_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
73
			COMMAND ${CMAKE_COMMAND} -E compare_files ${L}_${LUSTRE_NODE_OPT}_outputs ../outputs_values 
74
			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}}
75
	)
76
	SET_TESTS_PROPERTIES ( Stateflow_DIFF_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
77
	 PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}_outputs
78
				DEPENDS Stateflow_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT} )
79
				
80 36
	
37
  ENDFOREACH()
81 38
ENDFOREACH()
82 39

  
83
add_custom_target(Stateflow COMMAND ${CMAKE_CTEST_COMMAND} -R Stateflow)
40
add_custom_target(Steteflow COMMAND ${CMAKE_CTEST_COMMAND} -R Steteflow)
41

  
regression_tests/lustre_files/success/Stateflow/src_Arrays1/Arrays1.smt2
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.__Arrays1_A_ex_1 Bool)
8
(declare-var Arrays1_A_ex.idArrays1_Arrays1_2 Int)
9
(declare-rel Arrays1_A_ex (Int Bool Int))
10
(rule (=> 
11
  (and (= Arrays1_A_ex.__Arrays1_A_ex_1 (not Arrays1_A_ex.isInner))
12
       (and (or (not (= Arrays1_A_ex.__Arrays1_A_ex_1 true))
13
               (= Arrays1_A_ex.idArrays1_Arrays1_2 0))
14
            (or (not (= Arrays1_A_ex.__Arrays1_A_ex_1 false))
15
               (= Arrays1_A_ex.idArrays1_Arrays1_2 Arrays1_A_ex.idArrays1_Arrays1_1))
16
       )
17
       (= Arrays1_A_ex.idArrays1_Arrays1 Arrays1_A_ex.idArrays1_Arrays1_1)
18
       )
19
  (Arrays1_A_ex Arrays1_A_ex.idArrays1_Arrays1_1 Arrays1_A_ex.isInner Arrays1_A_ex.idArrays1_Arrays1)
20
))
21

  
22
; Arrays1_B_en
23
(declare-var Arrays1_B_en.idArrays1_Arrays1_1 Int)
24
(declare-var Arrays1_B_en.x_2_1 Int)
25
(declare-var Arrays1_B_en.isInner Bool)
26
(declare-var Arrays1_B_en.idArrays1_Arrays1 Int)
27
(declare-var Arrays1_B_en.x_2 Int)
28
(declare-var Arrays1_B_en.__Arrays1_B_en_1 Bool)
29
(declare-var Arrays1_B_en.idArrays1_Arrays1_2 Int)
30
(declare-var Arrays1_B_en.x_2_2 Int)
31
(declare-rel Arrays1_B_en (Int Int Bool Int Int))
32
(rule (=> 
33
  (and (= Arrays1_B_en.__Arrays1_B_en_1 (not Arrays1_B_en.isInner))
34
       (and (or (not (= Arrays1_B_en.__Arrays1_B_en_1 true))
35
               (= Arrays1_B_en.x_2_2 (+ Arrays1_B_en.x_2_1 1)))
36
            (or (not (= Arrays1_B_en.__Arrays1_B_en_1 false))
37
               (= Arrays1_B_en.x_2_2 Arrays1_B_en.x_2_1))
38
       )
39
       (= Arrays1_B_en.idArrays1_Arrays1_2 512)
40
       (= Arrays1_B_en.x_2 Arrays1_B_en.x_2_2)
41
       (= Arrays1_B_en.idArrays1_Arrays1 Arrays1_B_en.idArrays1_Arrays1_2)
42
       )
43
  (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)
44
))
45

  
46
; Arrays1_B_ex
47
(declare-var Arrays1_B_ex.idArrays1_Arrays1_1 Int)
48
(declare-var Arrays1_B_ex.isInner Bool)
49
(declare-var Arrays1_B_ex.idArrays1_Arrays1 Int)
50
(declare-var Arrays1_B_ex.__Arrays1_B_ex_1 Bool)
51
(declare-var Arrays1_B_ex.idArrays1_Arrays1_2 Int)
52
(declare-rel Arrays1_B_ex (Int Bool Int))
53
(rule (=> 
54
  (and (= Arrays1_B_ex.__Arrays1_B_ex_1 (not Arrays1_B_ex.isInner))
55
       (and (or (not (= Arrays1_B_ex.__Arrays1_B_ex_1 true))
56
               (= Arrays1_B_ex.idArrays1_Arrays1_2 0))
57
            (or (not (= Arrays1_B_ex.__Arrays1_B_ex_1 false))
58
               (= Arrays1_B_ex.idArrays1_Arrays1_2 Arrays1_B_ex.idArrays1_Arrays1_1))
59
       )
60
       (= Arrays1_B_ex.idArrays1_Arrays1 Arrays1_B_ex.idArrays1_Arrays1_1)
61
       )
62
  (Arrays1_B_ex Arrays1_B_ex.idArrays1_Arrays1_1 Arrays1_B_ex.isInner Arrays1_B_ex.idArrays1_Arrays1)
63
))
64

  
65
; Arrays1_C_en
66
(declare-var Arrays1_C_en.idArrays1_Arrays1_1 Int)
67
(declare-var Arrays1_C_en.x_3_1 Int)
68
(declare-var Arrays1_C_en.isInner Bool)
69
(declare-var Arrays1_C_en.idArrays1_Arrays1 Int)
70
(declare-var Arrays1_C_en.x_3 Int)
71
(declare-var Arrays1_C_en.__Arrays1_C_en_1 Bool)
72
(declare-var Arrays1_C_en.idArrays1_Arrays1_2 Int)
73
(declare-var Arrays1_C_en.x_3_2 Int)
74
(declare-rel Arrays1_C_en (Int Int Bool Int Int))
75
(rule (=> 
76
  (and (= Arrays1_C_en.__Arrays1_C_en_1 (not Arrays1_C_en.isInner))
77
       (and (or (not (= Arrays1_C_en.__Arrays1_C_en_1 true))
78
               (= Arrays1_C_en.x_3_2 (+ Arrays1_C_en.x_3_1 1)))
79
            (or (not (= Arrays1_C_en.__Arrays1_C_en_1 false))
80
               (= Arrays1_C_en.x_3_2 Arrays1_C_en.x_3_1))
81
       )
82
       (= Arrays1_C_en.idArrays1_Arrays1_2 513)
83
       (= Arrays1_C_en.x_3 Arrays1_C_en.x_3_2)
84
       (= Arrays1_C_en.idArrays1_Arrays1 Arrays1_C_en.idArrays1_Arrays1_2)
85
       )
86
  (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)
87
))
88

  
89
; Arrays1_A_en
90
(declare-var Arrays1_A_en.idArrays1_Arrays1_1 Int)
91
(declare-var Arrays1_A_en.x_1_1 Int)
92
(declare-var Arrays1_A_en.isInner Bool)
93
(declare-var Arrays1_A_en.idArrays1_Arrays1 Int)
94
(declare-var Arrays1_A_en.x_1 Int)
95
(declare-var Arrays1_A_en.__Arrays1_A_en_1 Bool)
96
(declare-var Arrays1_A_en.idArrays1_Arrays1_2 Int)
97
(declare-var Arrays1_A_en.x_1_2 Int)
98
(declare-rel Arrays1_A_en (Int Int Bool Int Int))
99
(rule (=> 
100
  (and (= Arrays1_A_en.__Arrays1_A_en_1 (not Arrays1_A_en.isInner))
101
       (and (or (not (= Arrays1_A_en.__Arrays1_A_en_1 true))
102
               (= Arrays1_A_en.x_1_2 (+ Arrays1_A_en.x_1_1 1)))
103
            (or (not (= Arrays1_A_en.__Arrays1_A_en_1 false))
104
               (= Arrays1_A_en.x_1_2 Arrays1_A_en.x_1_1))
105
       )
106
       (= Arrays1_A_en.idArrays1_Arrays1_2 511)
107
       (= Arrays1_A_en.x_1 Arrays1_A_en.x_1_2)
108
       (= Arrays1_A_en.idArrays1_Arrays1 Arrays1_A_en.idArrays1_Arrays1_2)
109
       )
110
  (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)
111
))
112

  
113
; Arrays1_C_ex
114
(declare-var Arrays1_C_ex.idArrays1_Arrays1_1 Int)
115
(declare-var Arrays1_C_ex.isInner Bool)
116
(declare-var Arrays1_C_ex.idArrays1_Arrays1 Int)
117
(declare-var Arrays1_C_ex.__Arrays1_C_ex_1 Bool)
118
(declare-var Arrays1_C_ex.idArrays1_Arrays1_2 Int)
119
(declare-rel Arrays1_C_ex (Int Bool Int))
120
(rule (=> 
121
  (and (= Arrays1_C_ex.__Arrays1_C_ex_1 (not Arrays1_C_ex.isInner))
122
       (and (or (not (= Arrays1_C_ex.__Arrays1_C_ex_1 true))
123
               (= Arrays1_C_ex.idArrays1_Arrays1_2 0))
124
            (or (not (= Arrays1_C_ex.__Arrays1_C_ex_1 false))
125
               (= Arrays1_C_ex.idArrays1_Arrays1_2 Arrays1_C_ex.idArrays1_Arrays1_1))
126
       )
127
       (= Arrays1_C_ex.idArrays1_Arrays1 Arrays1_C_ex.idArrays1_Arrays1_1)
128
       )
129
  (Arrays1_C_ex Arrays1_C_ex.idArrays1_Arrays1_1 Arrays1_C_ex.isInner Arrays1_C_ex.idArrays1_Arrays1)
130
))
131

  
132
; arrays1_arrays1__ARRAYS1_A_IDL_handler_until
133
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__restart_act Bool)
134
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1_1 Int)
135
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1_1 Int)
136
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2_1 Int)
137
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3_1 Int)
138
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__restart_in Bool)
139
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
140
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1_out Int)
141
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1_out Int)
142
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2_out Int)
143
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3_out Int)
144
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1 Int)
145
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1 Int)
146
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2 Int)
147
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3 Int)
148
(declare-rel arrays1_arrays1__ARRAYS1_A_IDL_handler_until (Bool Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
149
(rule (=> 
150
  (and (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3 arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3_1)
151
       (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3_out arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3)
152
       (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2 arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2_1)
153
       (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2_out arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2)
154
       (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1 arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1_1)
155
       (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1_out arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1)
156
       (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1 arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1_1)
157
       (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1)
158
       (and (or (not (= true true))
159
               (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1))
160
            (or (not (= true false))
161
               (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__state_in ARRAYS1_A_IDL))
162
       )
163
       (and (or (not (= true true))
164
               (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__restart_in true))
165
            (or (not (= true false))
166
               (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__restart_in false))
167
       )
168
       )
169
  (arrays1_arrays1__ARRAYS1_A_IDL_handler_until arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__restart_act 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)
170
))
171

  
172
; arrays1_arrays1__ARRAYS1_A_IDL_unless
173
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__restart_in Bool)
174
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__restart_act Bool)
175
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
176
(declare-rel arrays1_arrays1__ARRAYS1_A_IDL_unless (Bool Bool arrays1_arrays1__type))
177
(rule (=> 
178
  (and (= arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__state_act ARRAYS1_A_IDL)
179
       (= arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__restart_in)
180
       )
181
  (arrays1_arrays1__ARRAYS1_A_IDL_unless arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__state_act)
182
))
183

  
184
; arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until
185
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__restart_act Bool)
186
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_1 Int)
187
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_1_1 Int)
188
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_1 Int)
189
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_3_1 Int)
190
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__restart_in Bool)
191
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
192
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_out Int)
193
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_1_out Int)
194
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_out Int)
195
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_3_out Int)
196
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1 Int)
197
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_2 Int)
198
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_3 Int)
199
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_1 Int)
200
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2 Int)
201
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_2 Int)
202
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_3 Int)
203
(declare-rel arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until (Bool Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
204
(rule (=> 
205
  (and (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_3 arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_3_1)
206
       (= 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)
207
       (Arrays1_A_ex arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_1
208
                     false
209
                     arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_2)
210
       (Arrays1_B_en arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_2
211
                     arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_1
212
                     false
213
                     arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_3
214
                     arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_2)
215
       (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2 arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_2)
216
       (= 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)
217
       (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_1 arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_1_1)
218
       (= 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)
219
       (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1 arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_3)
220
       (= 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)
221
       (and (or (not (= true true))
222
               (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1))
223
            (or (not (= true false))
224
               (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__state_in ARRAYS1_A__TO__ARRAYS1_B_1))
225
       )
226
       (and (or (not (= true true))
227
               (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__restart_in true))
228
            (or (not (= true false))
229
               (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__restart_in false))
230
       )
231
       )
232
  (arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__restart_act 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)
233
))
234

  
235
; arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless
236
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__restart_in Bool)
237
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__restart_act Bool)
238
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
239
(declare-rel arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless (Bool Bool arrays1_arrays1__type))
240
(rule (=> 
241
  (and (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__state_act ARRAYS1_A__TO__ARRAYS1_B_1)
242
       (= 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)
243
       )
244
  (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__restart_act arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__state_act)
245
))
246

  
247
; arrays1_arrays1__ARRAYS1_B_IDL_handler_until
248
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__restart_act Bool)
249
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1_1 Int)
250
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1_1 Int)
251
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2_1 Int)
252
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3_1 Int)
253
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__restart_in Bool)
254
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
255
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1_out Int)
256
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1_out Int)
257
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2_out Int)
258
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3_out Int)
259
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1 Int)
260
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1 Int)
261
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2 Int)
262
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3 Int)
263
(declare-rel arrays1_arrays1__ARRAYS1_B_IDL_handler_until (Bool Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
264
(rule (=> 
265
  (and (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3 arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3_1)
266
       (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3_out arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3)
267
       (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2 arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2_1)
268
       (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2_out arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2)
269
       (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1 arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1_1)
270
       (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1_out arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1)
271
       (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1 arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1_1)
272
       (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1)
273
       (and (or (not (= true true))
274
               (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1))
275
            (or (not (= true false))
276
               (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__state_in ARRAYS1_B_IDL))
277
       )
278
       (and (or (not (= true true))
279
               (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__restart_in true))
280
            (or (not (= true false))
281
               (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__restart_in false))
282
       )
283
       )
284
  (arrays1_arrays1__ARRAYS1_B_IDL_handler_until arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__restart_act 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)
285
))
286

  
287
; arrays1_arrays1__ARRAYS1_B_IDL_unless
288
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__restart_in Bool)
289
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__restart_act Bool)
290
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
291
(declare-rel arrays1_arrays1__ARRAYS1_B_IDL_unless (Bool Bool arrays1_arrays1__type))
292
(rule (=> 
293
  (and (= arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__state_act ARRAYS1_B_IDL)
294
       (= arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__restart_in)
295
       )
296
  (arrays1_arrays1__ARRAYS1_B_IDL_unless arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__state_act)
297
))
298

  
299
; arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until
300
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__restart_act Bool)
301
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_1 Int)
302
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_1_1 Int)
303
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_2_1 Int)
304
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_1 Int)
305
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__restart_in Bool)
306
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
307
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_out Int)
308
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_1_out Int)
309
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_2_out Int)
310
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_out Int)
311
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1 Int)
312
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_2 Int)
313
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_3 Int)
314
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_1 Int)
315
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_2 Int)
316
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3 Int)
317
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_2 Int)
318
(declare-rel arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until (Bool Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
319
(rule (=> 
320
  (and (Arrays1_B_ex arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_1
321
                     false
322
                     arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_2)
323
       (Arrays1_C_en arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_2
324
                     arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_1
325
                     false
326
                     arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_3
327
                     arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_2)
328
       (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3 arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_2)
329
       (= 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)
330
       (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_2 arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_2_1)
331
       (= 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)
332
       (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_1 arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_1_1)
333
       (= 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)
334
       (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1 arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_3)
335
       (= 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)
336
       (and (or (not (= true true))
337
               (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1))
338
            (or (not (= true false))
339
               (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__state_in ARRAYS1_B__TO__ARRAYS1_C_1))
340
       )
341
       (and (or (not (= true true))
342
               (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__restart_in true))
343
            (or (not (= true false))
344
               (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__restart_in false))
345
       )
346
       )
347
  (arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__restart_act 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)
348
))
349

  
350
; arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless
351
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__restart_in Bool)
352
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__restart_act Bool)
353
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
354
(declare-rel arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless (Bool Bool arrays1_arrays1__type))
355
(rule (=> 
356
  (and (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__state_act ARRAYS1_B__TO__ARRAYS1_C_1)
357
       (= 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)
358
       )
359
  (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__restart_act arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__state_act)
360
))
361

  
362
; arrays1_arrays1__ARRAYS1_C_IDL_handler_until
363
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__restart_act Bool)
364
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1_1 Int)
365
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1_1 Int)
366
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2_1 Int)
367
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3_1 Int)
368
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__restart_in Bool)
369
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
370
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1_out Int)
371
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1_out Int)
372
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2_out Int)
373
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3_out Int)
374
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1 Int)
375
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1 Int)
376
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2 Int)
377
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3 Int)
378
(declare-rel arrays1_arrays1__ARRAYS1_C_IDL_handler_until (Bool Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
379
(rule (=> 
380
  (and (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3 arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3_1)
381
       (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3_out arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3)
382
       (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2 arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2_1)
383
       (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2_out arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2)
384
       (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1 arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1_1)
385
       (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1_out arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1)
386
       (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1 arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1_1)
387
       (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1)
388
       (and (or (not (= true true))
389
               (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1))
390
            (or (not (= true false))
391
               (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__state_in ARRAYS1_C_IDL))
392
       )
393
       (and (or (not (= true true))
394
               (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__restart_in true))
395
            (or (not (= true false))
396
               (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__restart_in false))
397
       )
398
       )
399
  (arrays1_arrays1__ARRAYS1_C_IDL_handler_until arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__restart_act 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)
400
))
401

  
402
; arrays1_arrays1__ARRAYS1_C_IDL_unless
403
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__restart_in Bool)
404
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__restart_act Bool)
405
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
406
(declare-rel arrays1_arrays1__ARRAYS1_C_IDL_unless (Bool Bool arrays1_arrays1__type))
407
(rule (=> 
408
  (and (= arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__state_act ARRAYS1_C_IDL)
409
       (= arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__restart_in)
410
       )
411
  (arrays1_arrays1__ARRAYS1_C_IDL_unless arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__state_act)
412
))
413

  
414
; arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until
415
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_act Bool)
416
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_1 Int)
417
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_1 Int)
418
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_2_1 Int)
419
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_3_1 Int)
420
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_in Bool)
421
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
422
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_out Int)
423
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_out Int)
424
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_2_out Int)
425
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_3_out Int)
426
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1 Int)
427
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_2 Int)
428
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_3 Int)
429
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1 Int)
430
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_2 Int)
431
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_2 Int)
432
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_3 Int)
433
(declare-rel arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until (Bool Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
434
(rule (=> 
435
  (and (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_3 arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_3_1)
436
       (= 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)
437
       (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_2 arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_2_1)
438
       (= 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)
439
       (Arrays1_C_ex arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_1
440
                     false
441
                     arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_2)
442
       (Arrays1_A_en arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_2
443
                     arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_1
444
                     false
445
                     arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_3
446
                     arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_2)
447
       (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1 arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_2)
448
       (= 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)
449
       (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1 arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_3)
450
       (= 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)
451
       (and (or (not (= true true))
452
               (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1))
453
            (or (not (= true false))
454
               (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__state_in ARRAYS1_C__TO__ARRAYS1_A_1))
455
       )
456
       (and (or (not (= true true))
457
               (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_in true))
458
            (or (not (= true false))
459
               (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_in false))
460
       )
461
       )
462
  (arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_act 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)
463
))
464

  
465
; arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless
466
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_in Bool)
467
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_act Bool)
468
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
469
(declare-rel arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless (Bool Bool arrays1_arrays1__type))
470
(rule (=> 
471
  (and (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_act ARRAYS1_C__TO__ARRAYS1_A_1)
472
       (= 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)
473
       )
474
  (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__restart_act arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_act)
475
))
476

  
477
; arrays1_arrays1__POINTArrays1_Arrays1_handler_until
478
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.arrays1_arrays1__restart_act Bool)
479
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1_1 Int)
480
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1_1 Int)
481
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2_1 Int)
482
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3_1 Int)
483
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.arrays1_arrays1__restart_in Bool)
484
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
485
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1_out Int)
486
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1_out Int)
487
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2_out Int)
488
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3_out Int)
489
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1 Int)
490
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1 Int)
491
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2 Int)
492
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3 Int)
493
(declare-rel arrays1_arrays1__POINTArrays1_Arrays1_handler_until (Bool Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
494
(rule (=> 
495
  (and (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3 arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3_1)
496
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3_out arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3)
497
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2 arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2_1)
498
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2_out arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2)
499
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1 arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1_1)
500
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1_out arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1)
501
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1 arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1_1)
502
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1)
503
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1)
504
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.arrays1_arrays1__restart_in false)
505
       )
506
  (arrays1_arrays1__POINTArrays1_Arrays1_handler_until arrays1_arrays1__POINTArrays1_Arrays1_handler_until.arrays1_arrays1__restart_act 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)
507
))
508

  
509
; arrays1_arrays1__POINTArrays1_Arrays1_unless
510
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_in Bool)
511
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 Int)
512
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.E Bool)
513
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act Bool)
514
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
515
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_1 Bool)
516
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_2 Bool)
517
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_3 Bool)
518
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_4 Bool)
519
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_5 Bool)
520
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_6 Bool)
521
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_7 Bool)
522
(declare-rel arrays1_arrays1__POINTArrays1_Arrays1_unless (Bool Int Bool Bool arrays1_arrays1__type))
523
(rule (=> 
524
  (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_7 (= arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 513))
525
       (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_6 (= arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 512))
526
       (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_5 (= arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 511))
527
       (= 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))
528
       (= 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))
529
       (= 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))
530
       (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_1 (= arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 0))
531
       (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_1 false))
532
               (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_2 false))
533
                       (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_3 false))
534
                               (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_4 false))
535
                                       (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_5 false))
536
                                               (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_6 false))
537
                                                       (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_7 false))
538
                                                               (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act POINTArrays1_Arrays1)
539
                                                                    (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_in)
540
                                                                    ))
541
                                                            (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_7 true))
542
                                                               (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act ARRAYS1_C_IDL)
543
                                                                    (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
544
                                                                    ))
545
                                                       ))
546
                                                    (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_6 true))
547
                                                       (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act ARRAYS1_B_IDL)
548
                                                            (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
549
                                                            ))
550
                                               ))
551
                                            (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_5 true))
552
                                               (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act ARRAYS1_A_IDL)
553
                                                    (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
554
                                                    ))
555
                                       ))
556
                                    (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_4 true))
557
                                       (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act ARRAYS1_C__TO__ARRAYS1_A_1)
558
                                            (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
559
                                            ))
560
                               ))
561
                            (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_3 true))
562
                               (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act ARRAYS1_B__TO__ARRAYS1_C_1)
563
                                    (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
564
                                    ))
565
                       ))
566
                    (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_2 true))
567
                       (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act ARRAYS1_A__TO__ARRAYS1_B_1)
568
                            (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
569
                            ))
570
               ))
571
            (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_1 true))
572
               (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act POINT__TO__ARRAYS1_A_1)
573
                    (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
574
                    ))
575
       )
576
       )
577
  (arrays1_arrays1__POINTArrays1_Arrays1_unless arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_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)
578
))
579

  
580
; arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until
581
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_act Bool)
582
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_1 Int)
583
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1_1 Int)
584
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_2_1 Int)
585
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_3_1 Int)
586
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_in Bool)
587
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
588
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_out Int)
589
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1_out Int)
590
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_2_out Int)
591
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_3_out Int)
592
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1 Int)
593
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_2 Int)
594
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1 Int)
595
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1_2 Int)
596
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_2 Int)
597
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_3 Int)
598
(declare-rel arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until (Bool Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
599
(rule (=> 
600
  (and (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_3 arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_3_1)
601
       (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_3_out arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_3)
602
       (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_2 arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_2_1)
603
       (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_2_out arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_2)
604
       (Arrays1_A_en arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_1
605
                     arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1_1
606
                     false
607
                     arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_2
608
                     arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1_2)
609
       (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1 arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1_2)
610
       (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1_out arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.x_1)
611
       (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1 arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_2)
612
       (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1)
613
       (and (or (not (= true true))
614
               (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1))
615
            (or (not (= true false))
616
               (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__state_in POINT__TO__ARRAYS1_A_1))
617
       )
618
       (and (or (not (= true true))
619
               (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_in true))
620
            (or (not (= true false))
621
               (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_in false))
622
       )
623
       )
624
  (arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_act 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)
625
))
626

  
627
; arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless
628
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_in Bool)
629
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_act Bool)
630
(declare-var arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
631
(declare-rel arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless (Bool Bool arrays1_arrays1__type))
632
(rule (=> 
633
  (and (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_act POINT__TO__ARRAYS1_A_1)
634
       (= arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_act arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_in)
635
       )
636
  (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__restart_act arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_act)
637
))
638

  
639
; Arrays1_Arrays1_node
640
(declare-var Arrays1_Arrays1_node.idArrays1_Arrays1_1 Int)
641
(declare-var Arrays1_Arrays1_node.x_1_1 Int)
642
(declare-var Arrays1_Arrays1_node.E Bool)
643
(declare-var Arrays1_Arrays1_node.x_2_1 Int)
644
(declare-var Arrays1_Arrays1_node.x_3_1 Int)
645
(declare-var Arrays1_Arrays1_node.idArrays1_Arrays1 Int)
646
(declare-var Arrays1_Arrays1_node.x_1 Int)
647
(declare-var Arrays1_Arrays1_node.x_2 Int)
648
(declare-var Arrays1_Arrays1_node.x_3 Int)
649
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c Bool)
650
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c arrays1_arrays1__type)
651
(declare-var Arrays1_Arrays1_node.ni_4._arrow._first_c Bool)
652
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m Bool)
653
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m arrays1_arrays1__type)
654
(declare-var Arrays1_Arrays1_node.ni_4._arrow._first_m Bool)
655
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_x Bool)
656
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_x arrays1_arrays1__type)
657
(declare-var Arrays1_Arrays1_node.ni_4._arrow._first_x Bool)
658
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_1 Bool)
659
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_10 arrays1_arrays1__type)
660
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_11 Bool)
661
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_12 arrays1_arrays1__type)
662
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_13 Bool)
663
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_14 arrays1_arrays1__type)
664
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_15 Bool)
665
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_16 arrays1_arrays1__type)
666
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_17 Bool)
667
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_18 arrays1_arrays1__type)
668
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_19 Int)
669
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_2 arrays1_arrays1__type)
670
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_20 Int)
671
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_21 Int)
672
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_22 Int)
673
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_23 Bool)
674
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_24 arrays1_arrays1__type)
675
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_25 Int)
676
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_26 Int)
677
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_27 Int)
678
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_28 Int)
679
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_29 Bool)
680
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_3 Bool)
681
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_30 arrays1_arrays1__type)
682
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_31 Int)
683
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_32 Int)
684
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_33 Int)
685
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_34 Int)
686
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_35 Bool)
687
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_36 arrays1_arrays1__type)
688
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_37 Int)
689
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_38 Int)
690
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_39 Int)
691
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_4 arrays1_arrays1__type)
692
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_40 Int)
693
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_41 Bool)
694
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_42 arrays1_arrays1__type)
695
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_43 Int)
696
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_44 Int)
697
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_45 Int)
698
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_46 Int)
699
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_47 Bool)
700
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_48 arrays1_arrays1__type)
701
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_49 Int)
702
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_5 Bool)
703
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_50 Int)
704
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_51 Int)
705
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_52 Int)
706
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_53 Bool)
707
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_54 arrays1_arrays1__type)
708
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_55 Int)
709
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_56 Int)
710
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_57 Int)
711
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_58 Int)
712
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_59 Bool)
713
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_6 arrays1_arrays1__type)
714
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_60 arrays1_arrays1__type)
715
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_61 Int)
716
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_62 Int)
717
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_63 Int)
718
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_64 Int)
719
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_65 Bool)
720
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_7 Bool)
721
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_8 arrays1_arrays1__type)
722
(declare-var Arrays1_Arrays1_node.__Arrays1_Arrays1_node_9 Bool)
723
(declare-var Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in Bool)
724
(declare-var Arrays1_Arrays1_node.arrays1_arrays1__next_state_in arrays1_arrays1__type)
725
(declare-var Arrays1_Arrays1_node.arrays1_arrays1__restart_act Bool)
726
(declare-var Arrays1_Arrays1_node.arrays1_arrays1__restart_in Bool)
727
(declare-var Arrays1_Arrays1_node.arrays1_arrays1__state_act arrays1_arrays1__type)
728
(declare-var Arrays1_Arrays1_node.arrays1_arrays1__state_in arrays1_arrays1__type)
729
(declare-rel Arrays1_Arrays1_node_reset (Bool arrays1_arrays1__type Bool Bool arrays1_arrays1__type Bool))
730
(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))
731

  
732
(rule (=> 
733
  (and 
734
       (= Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c)
735
       (= Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c)
736
       (= Arrays1_Arrays1_node.ni_4._arrow._first_m true)
737
  )
738
  (Arrays1_Arrays1_node_reset Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c
739
                              Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c
740
                              Arrays1_Arrays1_node.ni_4._arrow._first_c
741
                              Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m
742
                              Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m
743
                              Arrays1_Arrays1_node.ni_4._arrow._first_m)
744
))
745

  
746
(rule (=> 
747
  (and (= Arrays1_Arrays1_node.ni_4._arrow._first_m Arrays1_Arrays1_node.ni_4._arrow._first_c)
748
       (and (= Arrays1_Arrays1_node.__Arrays1_Arrays1_node_65 (ite Arrays1_Arrays1_node.ni_4._arrow._first_m true false))
749
            (= Arrays1_Arrays1_node.ni_4._arrow._first_x false))
750
       (and (or (not (= Arrays1_Arrays1_node.__Arrays1_Arrays1_node_65 false))
751
               (and (= Arrays1_Arrays1_node.arrays1_arrays1__state_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c)
752
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c)
753
                    ))
754
            (or (not (= Arrays1_Arrays1_node.__Arrays1_Arrays1_node_65 true))
755
               (and (= Arrays1_Arrays1_node.arrays1_arrays1__state_in POINTArrays1_Arrays1)
756
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_in false)
757
                    ))
758
       )
759
       (and (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_in ARRAYS1_A_IDL))
760
               (and (arrays1_arrays1__ARRAYS1_A_IDL_unless Arrays1_Arrays1_node.arrays1_arrays1__restart_in
761
                                                           Arrays1_Arrays1_node.__Arrays1_Arrays1_node_5
762
                                                           Arrays1_Arrays1_node.__Arrays1_Arrays1_node_6)
763
                    (= Arrays1_Arrays1_node.arrays1_arrays1__state_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_6)
764
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_5)
765
                    ))
766
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_in ARRAYS1_A__TO__ARRAYS1_B_1))
767
               (and (arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless 
768
                    Arrays1_Arrays1_node.arrays1_arrays1__restart_in
769
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_11
770
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_12)
771
                    (= Arrays1_Arrays1_node.arrays1_arrays1__state_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_12)
772
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_11)
773
                    ))
774
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_in ARRAYS1_B_IDL))
775
               (and (arrays1_arrays1__ARRAYS1_B_IDL_unless Arrays1_Arrays1_node.arrays1_arrays1__restart_in
776
                                                           Arrays1_Arrays1_node.__Arrays1_Arrays1_node_3
777
                                                           Arrays1_Arrays1_node.__Arrays1_Arrays1_node_4)
778
                    (= Arrays1_Arrays1_node.arrays1_arrays1__state_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_4)
779
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_3)
780
                    ))
781
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_in ARRAYS1_B__TO__ARRAYS1_C_1))
782
               (and (arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless 
783
                    Arrays1_Arrays1_node.arrays1_arrays1__restart_in
784
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_9
785
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_10)
786
                    (= Arrays1_Arrays1_node.arrays1_arrays1__state_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_10)
787
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_9)
788
                    ))
789
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_in ARRAYS1_C_IDL))
790
               (and (arrays1_arrays1__ARRAYS1_C_IDL_unless Arrays1_Arrays1_node.arrays1_arrays1__restart_in
791
                                                           Arrays1_Arrays1_node.__Arrays1_Arrays1_node_1
792
                                                           Arrays1_Arrays1_node.__Arrays1_Arrays1_node_2)
793
                    (= Arrays1_Arrays1_node.arrays1_arrays1__state_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_2)
794
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_1)
795
                    ))
796
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_in ARRAYS1_C__TO__ARRAYS1_A_1))
797
               (and (arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless 
798
                    Arrays1_Arrays1_node.arrays1_arrays1__restart_in
799
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_7
800
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_8)
801
                    (= Arrays1_Arrays1_node.arrays1_arrays1__state_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_8)
802
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_7)
803
                    ))
804
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_in POINTArrays1_Arrays1))
805
               (and (arrays1_arrays1__POINTArrays1_Arrays1_unless Arrays1_Arrays1_node.arrays1_arrays1__restart_in
806
                                                                  Arrays1_Arrays1_node.idArrays1_Arrays1_1
807
                                                                  Arrays1_Arrays1_node.E
808
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_15
809
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_16)
810
                    (= Arrays1_Arrays1_node.arrays1_arrays1__state_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_16)
811
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_15)
812
                    ))
813
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_in POINT__TO__ARRAYS1_A_1))
814
               (and (arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless Arrays1_Arrays1_node.arrays1_arrays1__restart_in
815
                                                                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_13
816
                                                                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_14)
817
                    (= Arrays1_Arrays1_node.arrays1_arrays1__state_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_14)
818
                    (= Arrays1_Arrays1_node.arrays1_arrays1__restart_act Arrays1_Arrays1_node.__Arrays1_Arrays1_node_13)
819
                    ))
820
       )
821
       (and (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_act ARRAYS1_A_IDL))
822
               (and (arrays1_arrays1__ARRAYS1_A_IDL_handler_until Arrays1_Arrays1_node.arrays1_arrays1__restart_act
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_29
828
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_30
829
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_31
830
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_32
831
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_33
832
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_34)
833
                    (= Arrays1_Arrays1_node.x_3 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_34)
834
                    (= Arrays1_Arrays1_node.x_2 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_33)
835
                    (= Arrays1_Arrays1_node.x_1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_32)
836
                    (= Arrays1_Arrays1_node.idArrays1_Arrays1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_31)
837
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_state_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_30)
838
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_29)
839
                    ))
840
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_act ARRAYS1_A__TO__ARRAYS1_B_1))
841
               (and (arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until 
842
                    Arrays1_Arrays1_node.arrays1_arrays1__restart_act
843
                    Arrays1_Arrays1_node.idArrays1_Arrays1_1
844
                    Arrays1_Arrays1_node.x_1_1
845
                    Arrays1_Arrays1_node.x_2_1
846
                    Arrays1_Arrays1_node.x_3_1
847
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_47
848
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_48
849
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_49
850
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_50
851
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_51
852
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_52)
853
                    (= Arrays1_Arrays1_node.x_3 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_52)
854
                    (= Arrays1_Arrays1_node.x_2 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_51)
855
                    (= Arrays1_Arrays1_node.x_1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_50)
856
                    (= Arrays1_Arrays1_node.idArrays1_Arrays1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_49)
857
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_state_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_48)
858
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_47)
859
                    ))
860
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_act ARRAYS1_B_IDL))
861
               (and (arrays1_arrays1__ARRAYS1_B_IDL_handler_until Arrays1_Arrays1_node.arrays1_arrays1__restart_act
862
                                                                  Arrays1_Arrays1_node.idArrays1_Arrays1_1
863
                                                                  Arrays1_Arrays1_node.x_1_1
864
                                                                  Arrays1_Arrays1_node.x_2_1
865
                                                                  Arrays1_Arrays1_node.x_3_1
866
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_23
867
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_24
868
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_25
869
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_26
870
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_27
871
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_28)
872
                    (= Arrays1_Arrays1_node.x_3 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_28)
873
                    (= Arrays1_Arrays1_node.x_2 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_27)
874
                    (= Arrays1_Arrays1_node.x_1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_26)
875
                    (= Arrays1_Arrays1_node.idArrays1_Arrays1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_25)
876
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_state_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_24)
877
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_23)
878
                    ))
879
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_act ARRAYS1_B__TO__ARRAYS1_C_1))
880
               (and (arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until 
881
                    Arrays1_Arrays1_node.arrays1_arrays1__restart_act
882
                    Arrays1_Arrays1_node.idArrays1_Arrays1_1
883
                    Arrays1_Arrays1_node.x_1_1
884
                    Arrays1_Arrays1_node.x_2_1
885
                    Arrays1_Arrays1_node.x_3_1
886
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_41
887
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_42
888
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_43
889
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_44
890
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_45
891
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_46)
892
                    (= Arrays1_Arrays1_node.x_3 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_46)
893
                    (= Arrays1_Arrays1_node.x_2 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_45)
894
                    (= Arrays1_Arrays1_node.x_1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_44)
895
                    (= Arrays1_Arrays1_node.idArrays1_Arrays1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_43)
896
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_state_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_42)
897
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_41)
898
                    ))
899
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_act ARRAYS1_C_IDL))
900
               (and (arrays1_arrays1__ARRAYS1_C_IDL_handler_until Arrays1_Arrays1_node.arrays1_arrays1__restart_act
901
                                                                  Arrays1_Arrays1_node.idArrays1_Arrays1_1
902
                                                                  Arrays1_Arrays1_node.x_1_1
903
                                                                  Arrays1_Arrays1_node.x_2_1
904
                                                                  Arrays1_Arrays1_node.x_3_1
905
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_17
906
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_18
907
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_19
908
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_20
909
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_21
910
                                                                  Arrays1_Arrays1_node.__Arrays1_Arrays1_node_22)
911
                    (= Arrays1_Arrays1_node.x_3 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_22)
912
                    (= Arrays1_Arrays1_node.x_2 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_21)
913
                    (= Arrays1_Arrays1_node.x_1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_20)
914
                    (= Arrays1_Arrays1_node.idArrays1_Arrays1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_19)
915
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_state_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_18)
916
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_17)
917
                    ))
918
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_act ARRAYS1_C__TO__ARRAYS1_A_1))
919
               (and (arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until 
920
                    Arrays1_Arrays1_node.arrays1_arrays1__restart_act
921
                    Arrays1_Arrays1_node.idArrays1_Arrays1_1
922
                    Arrays1_Arrays1_node.x_1_1
923
                    Arrays1_Arrays1_node.x_2_1
924
                    Arrays1_Arrays1_node.x_3_1
925
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_35
926
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_36
927
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_37
928
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_38
929
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_39
930
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_40)
931
                    (= Arrays1_Arrays1_node.x_3 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_40)
932
                    (= Arrays1_Arrays1_node.x_2 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_39)
933
                    (= Arrays1_Arrays1_node.x_1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_38)
934
                    (= Arrays1_Arrays1_node.idArrays1_Arrays1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_37)
935
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_state_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_36)
936
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_35)
937
                    ))
938
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_act POINTArrays1_Arrays1))
939
               (and (arrays1_arrays1__POINTArrays1_Arrays1_handler_until 
940
                    Arrays1_Arrays1_node.arrays1_arrays1__restart_act
941
                    Arrays1_Arrays1_node.idArrays1_Arrays1_1
942
                    Arrays1_Arrays1_node.x_1_1
943
                    Arrays1_Arrays1_node.x_2_1
944
                    Arrays1_Arrays1_node.x_3_1
945
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_59
946
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_60
947
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_61
948
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_62
949
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_63
950
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_64)
951
                    (= Arrays1_Arrays1_node.x_3 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_64)
952
                    (= Arrays1_Arrays1_node.x_2 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_63)
953
                    (= Arrays1_Arrays1_node.x_1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_62)
954
                    (= Arrays1_Arrays1_node.idArrays1_Arrays1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_61)
955
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_state_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_60)
956
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_59)
957
                    ))
958
            (or (not (= Arrays1_Arrays1_node.arrays1_arrays1__state_act POINT__TO__ARRAYS1_A_1))
959
               (and (arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until 
960
                    Arrays1_Arrays1_node.arrays1_arrays1__restart_act
961
                    Arrays1_Arrays1_node.idArrays1_Arrays1_1
962
                    Arrays1_Arrays1_node.x_1_1
963
                    Arrays1_Arrays1_node.x_2_1
964
                    Arrays1_Arrays1_node.x_3_1
965
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_53
966
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_54
967
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_55
968
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_56
969
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_57
970
                    Arrays1_Arrays1_node.__Arrays1_Arrays1_node_58)
971
                    (= Arrays1_Arrays1_node.x_3 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_58)
972
                    (= Arrays1_Arrays1_node.x_2 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_57)
973
                    (= Arrays1_Arrays1_node.x_1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_56)
974
                    (= Arrays1_Arrays1_node.idArrays1_Arrays1 Arrays1_Arrays1_node.__Arrays1_Arrays1_node_55)
975
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_state_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_54)
976
                    (= Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in Arrays1_Arrays1_node.__Arrays1_Arrays1_node_53)
977
                    ))
978
       )
979
       (= Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_x Arrays1_Arrays1_node.arrays1_arrays1__next_state_in)
980
       (= Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_x Arrays1_Arrays1_node.arrays1_arrays1__next_restart_in)
981
       )
982
  (Arrays1_Arrays1_node_step Arrays1_Arrays1_node.idArrays1_Arrays1_1
983
                             Arrays1_Arrays1_node.x_1_1
984
                             Arrays1_Arrays1_node.E
985
                             Arrays1_Arrays1_node.x_2_1
986
                             Arrays1_Arrays1_node.x_3_1
987
                             Arrays1_Arrays1_node.idArrays1_Arrays1
988
                             Arrays1_Arrays1_node.x_1
989
                             Arrays1_Arrays1_node.x_2
990
                             Arrays1_Arrays1_node.x_3
991
                             Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c
992
                             Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c
993
                             Arrays1_Arrays1_node.ni_4._arrow._first_c
994
                             Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_x
995
                             Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_x
996
                             Arrays1_Arrays1_node.ni_4._arrow._first_x)
997
))
998

  
999
; Arrays1_Arrays1
1000
(declare-var Arrays1_Arrays1.E Bool)
1001
(declare-var Arrays1_Arrays1.x_1 Int)
1002
(declare-var Arrays1_Arrays1.x_2 Int)
1003
(declare-var Arrays1_Arrays1.x_3 Int)
1004
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_6_c Int)
1005
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_7_c Int)
1006
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_8_c Int)
1007
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_9_c Int)
1008
(declare-var Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c Bool)
1009
(declare-var Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c arrays1_arrays1__type)
1010
(declare-var Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c Bool)
1011
(declare-var Arrays1_Arrays1.ni_3._arrow._first_c Bool)
1012
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_6_m Int)
1013
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_7_m Int)
1014
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_8_m Int)
1015
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_9_m Int)
1016
(declare-var Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m Bool)
1017
(declare-var Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m arrays1_arrays1__type)
1018
(declare-var Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m Bool)
1019
(declare-var Arrays1_Arrays1.ni_3._arrow._first_m Bool)
1020
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_6_x Int)
1021
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_7_x Int)
1022
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_8_x Int)
1023
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_9_x Int)
1024
(declare-var Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_x Bool)
1025
(declare-var Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_x arrays1_arrays1__type)
1026
(declare-var Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_x Bool)
1027
(declare-var Arrays1_Arrays1.ni_3._arrow._first_x Bool)
1028
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_1 Int)
1029
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_2 Int)
1030
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_3 Int)
1031
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_4 Int)
1032
(declare-var Arrays1_Arrays1.__Arrays1_Arrays1_5 Bool)
1033
(declare-var Arrays1_Arrays1.idArrays1_Arrays1 Int)
1034
(declare-var Arrays1_Arrays1.idArrays1_Arrays1_1 Int)
1035
(declare-var Arrays1_Arrays1.x_1_1 Int)
1036
(declare-var Arrays1_Arrays1.x_2_1 Int)
1037
(declare-var Arrays1_Arrays1.x_3_1 Int)
1038
(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))
1039
(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))
1040

  
1041
(rule (=> 
1042
  (and 
1043
       (= Arrays1_Arrays1.__Arrays1_Arrays1_6_m Arrays1_Arrays1.__Arrays1_Arrays1_6_c)
1044
       (= Arrays1_Arrays1.__Arrays1_Arrays1_7_m Arrays1_Arrays1.__Arrays1_Arrays1_7_c)
1045
       (= Arrays1_Arrays1.__Arrays1_Arrays1_8_m Arrays1_Arrays1.__Arrays1_Arrays1_8_c)
1046
       (= Arrays1_Arrays1.__Arrays1_Arrays1_9_m Arrays1_Arrays1.__Arrays1_Arrays1_9_c)
1047
       (= Arrays1_Arrays1.ni_3._arrow._first_m true)
1048
       (Arrays1_Arrays1_node_reset Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c
1049
                                   Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c
1050
                                   Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c
1051
                                   Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m
1052
                                   Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m
1053
                                   Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m)
1054
  )
1055
  (Arrays1_Arrays1_reset Arrays1_Arrays1.__Arrays1_Arrays1_6_c
1056
                         Arrays1_Arrays1.__Arrays1_Arrays1_7_c
1057
                         Arrays1_Arrays1.__Arrays1_Arrays1_8_c
1058
                         Arrays1_Arrays1.__Arrays1_Arrays1_9_c
1059
                         Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c
1060
                         Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c
1061
                         Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c
1062
                         Arrays1_Arrays1.ni_3._arrow._first_c
1063
                         Arrays1_Arrays1.__Arrays1_Arrays1_6_m
1064
                         Arrays1_Arrays1.__Arrays1_Arrays1_7_m
1065
                         Arrays1_Arrays1.__Arrays1_Arrays1_8_m
1066
                         Arrays1_Arrays1.__Arrays1_Arrays1_9_m
1067
                         Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m
1068
                         Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m
1069
                         Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m
1070
                         Arrays1_Arrays1.ni_3._arrow._first_m)
1071
))
1072

  
1073
(rule (=> 
1074
  (and (= Arrays1_Arrays1.ni_3._arrow._first_m Arrays1_Arrays1.ni_3._arrow._first_c)
1075
       (and (= Arrays1_Arrays1.__Arrays1_Arrays1_5 (ite Arrays1_Arrays1.ni_3._arrow._first_m true false))
1076
            (= Arrays1_Arrays1.ni_3._arrow._first_x false))
1077
       (and (or (not (= Arrays1_Arrays1.__Arrays1_Arrays1_5 false))
1078
               (and (= Arrays1_Arrays1.x_3_1 Arrays1_Arrays1.__Arrays1_Arrays1_7_c)
1079
                    (= Arrays1_Arrays1.x_2_1 Arrays1_Arrays1.__Arrays1_Arrays1_8_c)
1080
                    (= Arrays1_Arrays1.x_1_1 Arrays1_Arrays1.__Arrays1_Arrays1_9_c)
1081
                    (= Arrays1_Arrays1.idArrays1_Arrays1_1 Arrays1_Arrays1.__Arrays1_Arrays1_6_c)
1082
                    ))
1083
            (or (not (= Arrays1_Arrays1.__Arrays1_Arrays1_5 true))
1084
               (and (= Arrays1_Arrays1.x_3_1 1)
1085
                    (= Arrays1_Arrays1.x_2_1 1)
1086
                    (= Arrays1_Arrays1.x_1_1 1)
1087
                    (= Arrays1_Arrays1.idArrays1_Arrays1_1 0)
1088
                    ))
1089
       )
1090
       (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)
1091
            (= Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c)
1092
            (= Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c)
1093
            )
1094
       (Arrays1_Arrays1_node_step Arrays1_Arrays1.idArrays1_Arrays1_1
1095
                                  Arrays1_Arrays1.x_1_1
1096
                                  Arrays1_Arrays1.E
1097
                                  Arrays1_Arrays1.x_2_1
1098
                                  Arrays1_Arrays1.x_3_1
1099
                                  Arrays1_Arrays1.__Arrays1_Arrays1_1
1100
                                  Arrays1_Arrays1.__Arrays1_Arrays1_2
1101
                                  Arrays1_Arrays1.__Arrays1_Arrays1_3
1102
                                  Arrays1_Arrays1.__Arrays1_Arrays1_4
1103
                                  Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m
1104
                                  Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m
1105
                                  Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m
1106
                                  Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_x
1107
                                  Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_x
1108
                                  Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_x)
1109
       (and (or (not (= Arrays1_Arrays1.E false))
1110
               (and (= Arrays1_Arrays1.x_3 Arrays1_Arrays1.x_3_1)
1111
                    (= Arrays1_Arrays1.x_2 Arrays1_Arrays1.x_2_1)
1112
                    (= Arrays1_Arrays1.x_1 Arrays1_Arrays1.x_1_1)
1113
                    (= Arrays1_Arrays1.idArrays1_Arrays1 Arrays1_Arrays1.idArrays1_Arrays1_1)
1114
                    ))
1115
            (or (not (= Arrays1_Arrays1.E true))
1116
               (and (= Arrays1_Arrays1.x_3 Arrays1_Arrays1.__Arrays1_Arrays1_4)
1117
                    (= Arrays1_Arrays1.x_2 Arrays1_Arrays1.__Arrays1_Arrays1_3)
1118
                    (= Arrays1_Arrays1.x_1 Arrays1_Arrays1.__Arrays1_Arrays1_2)
1119
                    (= Arrays1_Arrays1.idArrays1_Arrays1 Arrays1_Arrays1.__Arrays1_Arrays1_1)
1120
                    ))
1121
       )
1122
       (= Arrays1_Arrays1.__Arrays1_Arrays1_9_x Arrays1_Arrays1.x_1)
1123
       (= Arrays1_Arrays1.__Arrays1_Arrays1_8_x Arrays1_Arrays1.x_2)
1124
       (= Arrays1_Arrays1.__Arrays1_Arrays1_7_x Arrays1_Arrays1.x_3)
1125
       (= Arrays1_Arrays1.__Arrays1_Arrays1_6_x Arrays1_Arrays1.idArrays1_Arrays1)
1126
       )
1127
  (Arrays1_Arrays1_step Arrays1_Arrays1.E
1128
                        Arrays1_Arrays1.x_1
1129
                        Arrays1_Arrays1.x_2
1130
                        Arrays1_Arrays1.x_3
1131
                        Arrays1_Arrays1.__Arrays1_Arrays1_6_c
1132
                        Arrays1_Arrays1.__Arrays1_Arrays1_7_c
1133
                        Arrays1_Arrays1.__Arrays1_Arrays1_8_c
1134
                        Arrays1_Arrays1.__Arrays1_Arrays1_9_c
1135
                        Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c
1136
                        Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c
1137
                        Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c
1138
                        Arrays1_Arrays1.ni_3._arrow._first_c
1139
                        Arrays1_Arrays1.__Arrays1_Arrays1_6_x
1140
                        Arrays1_Arrays1.__Arrays1_Arrays1_7_x
1141
                        Arrays1_Arrays1.__Arrays1_Arrays1_8_x
1142
                        Arrays1_Arrays1.__Arrays1_Arrays1_9_x
1143
                        Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_x
1144
                        Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_x
1145
                        Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_x
1146
                        Arrays1_Arrays1.ni_3._arrow._first_x)
1147
))
1148

  
1149
; Arrays1
1150
(declare-var Arrays1.E_1_1 Real)
1151
(declare-var Arrays1.x1_1_1 Int)
1152
(declare-var Arrays1.x2_2_1 Int)
1153
(declare-var Arrays1.x3_3_1 Int)
1154
(declare-var Arrays1.__Arrays1_2_c Real)
1155
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_c Int)
1156
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_c Int)
1157
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_c Int)
1158
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_c Int)
1159
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c Bool)
1160
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c arrays1_arrays1__type)
1161
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c Bool)
1162
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_c Bool)
1163
(declare-var Arrays1.ni_1._arrow._first_c Bool)
1164
(declare-var Arrays1.__Arrays1_2_m Real)
1165
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_m Int)
1166
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_m Int)
1167
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_m Int)
1168
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_m Int)
1169
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m Bool)
1170
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m arrays1_arrays1__type)
1171
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m Bool)
1172
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_m Bool)
1173
(declare-var Arrays1.ni_1._arrow._first_m Bool)
1174
(declare-var Arrays1.__Arrays1_2_x Real)
1175
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_x Int)
1176
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_x Int)
1177
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_x Int)
1178
(declare-var Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_x Int)
1179
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_x Bool)
1180
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_x arrays1_arrays1__type)
1181
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_x Bool)
1182
(declare-var Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_x Bool)
1183
(declare-var Arrays1.ni_1._arrow._first_x Bool)
1184
(declare-var Arrays1.Arrays1E_1_1_event Bool)
1185
(declare-var Arrays1.Arrays1_1_1 Int)
1186
(declare-var Arrays1.Arrays1_1_2 Int)
1187
(declare-var Arrays1.Arrays1_1_3 Int)
1188
(declare-var Arrays1.Demux_1_1 Int)
1189
(declare-var Arrays1.Demux_2_1 Int)
1190
(declare-var Arrays1.Demux_3_1 Int)
1191
(declare-var Arrays1.__Arrays1_1 Bool)
1192
(declare-var Arrays1.i_virtual_local Real)
1193
(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))
1194
(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))
1195

  
1196
(rule (=> 
1197
  (and 
1198
       (= Arrays1.__Arrays1_2_m Arrays1.__Arrays1_2_c)
1199
       (= Arrays1.ni_1._arrow._first_m true)
1200
       (Arrays1_Arrays1_reset Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_c
1201
                              Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_c
1202
                              Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_c
1203
                              Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_c
1204
                              Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c
1205
                              Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c
1206
                              Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c
1207
                              Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_c
1208
                              Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_m
1209
                              Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_m
1210
                              Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_m
1211
                              Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_m
1212
                              Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m
1213
                              Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m
1214
                              Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m
1215
                              Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_m)
1216
  )
1217
  (Arrays1_reset Arrays1.__Arrays1_2_c
1218
                 Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_c
1219
                 Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_c
1220
                 Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_c
1221
                 Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_c
1222
                 Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c
1223
                 Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c
1224
                 Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c
1225
                 Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_c
1226
                 Arrays1.ni_1._arrow._first_c
1227
                 Arrays1.__Arrays1_2_m
1228
                 Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_m
1229
                 Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_m
1230
                 Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_m
1231
                 Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_m
1232
                 Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m
1233
                 Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m
1234
                 Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m
1235
                 Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_m
1236
                 Arrays1.ni_1._arrow._first_m)
1237
))
1238

  
1239
(rule (=> 
1240
  (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))
1241
                                                                    (= Arrays1.ni_1._arrow._first_x false))
1242
       (and (or (not (= Arrays1.__Arrays1_1 true))
1243
               (= Arrays1.Arrays1E_1_1_event false))
1244
            (or (not (= Arrays1.__Arrays1_1 false))
1245
               (= Arrays1.Arrays1E_1_1_event (and (<= Arrays1.__Arrays1_2_c 0.0) (> Arrays1.E_1_1 0.0))))
1246
       )
1247
       (and (= Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_m Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_c)
1248
            (= Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_m Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_c)
1249
            (= Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_m Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_c)
1250
            (= Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_m Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_c)
1251
            (= 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)
1252
            (= 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)
1253
            (= 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)
1254
            (= Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_m Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_c)
1255
            )
1256
       (Arrays1_Arrays1_step Arrays1.Arrays1E_1_1_event
1257
                             Arrays1.Arrays1_1_1
1258
                             Arrays1.Arrays1_1_2
1259
                             Arrays1.Arrays1_1_3
1260
                             Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_m
1261
                             Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_m
1262
                             Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_m
1263
                             Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_m
1264
                             Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_m
1265
                             Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_m
1266
                             Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_m
1267
                             Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_m
1268
                             Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_x
1269
                             Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_x
1270
                             Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_x
1271
                             Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_x
1272
                             Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_x
1273
                             Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_x
1274
                             Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_x
1275
                             Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_x)
1276
       (= Arrays1.Demux_3_1 Arrays1.Arrays1_1_3)
1277
       (= Arrays1.x3_3_1 Arrays1.Demux_3_1)
1278
       (= Arrays1.Demux_2_1 Arrays1.Arrays1_1_2)
1279
       (= Arrays1.x2_2_1 Arrays1.Demux_2_1)
1280
       (= Arrays1.Demux_1_1 Arrays1.Arrays1_1_1)
1281
       (= Arrays1.x1_1_1 Arrays1.Demux_1_1)
1282
       (and (or (not (= Arrays1.__Arrays1_1 true))
1283
               (= Arrays1.i_virtual_local 0.0))
1284
            (or (not (= Arrays1.__Arrays1_1 false))
1285
               (= Arrays1.i_virtual_local 1.0))
1286
       )
1287
       (= Arrays1.__Arrays1_2_x Arrays1.E_1_1)
1288
       )
1289
  (Arrays1_step Arrays1.E_1_1
1290
                Arrays1.x1_1_1
1291
                Arrays1.x2_2_1
1292
                Arrays1.x3_3_1
1293
                Arrays1.__Arrays1_2_c
1294
                Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_c
1295
                Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_c
1296
                Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_c
1297
                Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_c
1298
                Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_c
1299
                Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_c
1300
                Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_c
1301
                Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_c
1302
                Arrays1.ni_1._arrow._first_c
1303
                Arrays1.__Arrays1_2_x
1304
                Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_6_x
1305
                Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_7_x
1306
                Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_8_x
1307
                Arrays1.ni_0.Arrays1_Arrays1.__Arrays1_Arrays1_9_x
1308
                Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_66_x
1309
                Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.__Arrays1_Arrays1_node_67_x
1310
                Arrays1.ni_0.Arrays1_Arrays1.ni_2.Arrays1_Arrays1_node.ni_4._arrow._first_x
1311
                Arrays1.ni_0.Arrays1_Arrays1.ni_3._arrow._first_x
1312
                Arrays1.ni_1._arrow._first_x)
1313
))
1314

  
regression_tests/lustre_files/success/Stateflow/src_Arrays1/input_values
1
1.0000000000000000
2
1.0000000000000000
3
1.0000000000000000
4
1.0000000000000000
5
-1.0000000000000000
6
-1.0000000000000000
7
-1.0000000000000000
8
1.0000000000000000
9
1.0000000000000000
10
1.0000000000000000
11
-1.0000000000000000
12
-1.0000000000000000
13
-1.0000000000000000
14
1.0000000000000000
15
1.0000000000000000
16
1.0000000000000000
17
-1.0000000000000000
18
-1.0000000000000000
19
-1.0000000000000000
20
1.0000000000000000
21
1.0000000000000000
22
1.0000000000000000
23
-1.0000000000000000
24
-1.0000000000000000
25
-1.0000000000000000
26
-1.0000000000000000
27
1.0000000000000000
28
1.0000000000000000
29
1.0000000000000000
30
-1.0000000000000000
31
-1.0000000000000000
32
-1.0000000000000000
33
1.0000000000000000
34
1.0000000000000000
35
1.0000000000000000
36
-1.0000000000000000
37
-1.0000000000000000
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff