Constant propagation for individual fields through byte extract

jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc

@@ -1,20 +1,20 @@
 CORE
 Test
 --function Test.main --show-vcc --max-field-sensitivity-array-size 10
-symex_dynamic::dynamic_2_array#2\[\[0\]\] = symex_dynamic::dynamic_2_array#2\[0\]
-symex_dynamic::dynamic_2_array#2\[\[1\]\] = symex_dynamic::dynamic_2_array#2\[1\]
-symex_dynamic::dynamic_2_array#2\[\[2\]\] = symex_dynamic::dynamic_2_array#2\[2\]
-symex_dynamic::dynamic_2_array#2\[\[3\]\] = symex_dynamic::dynamic_2_array#2\[3\]
-symex_dynamic::dynamic_2_array#2\[\[4\]\] = symex_dynamic::dynamic_2_array#2\[4\]
-symex_dynamic::dynamic_2_array#2\[\[5\]\] = symex_dynamic::dynamic_2_array#2\[5\]
-symex_dynamic::dynamic_2_array#2\[\[6\]\] = symex_dynamic::dynamic_2_array#2\[6\]
-symex_dynamic::dynamic_2_array#2\[\[7\]\] = symex_dynamic::dynamic_2_array#2\[7\]
-symex_dynamic::dynamic_2_array#2\[\[8\]\] = symex_dynamic::dynamic_2_array#2\[8\]
-symex_dynamic::dynamic_2_array#2\[\[9\]\] = symex_dynamic::dynamic_2_array#2\[9\]
+symex_dynamic::dynamic_2_array#2\[\[0\]\] =
+symex_dynamic::dynamic_2_array#2\[\[1\]\] =
+symex_dynamic::dynamic_2_array#2\[\[2\]\] =
+symex_dynamic::dynamic_2_array#2\[\[3\]\] =
+symex_dynamic::dynamic_2_array#2\[\[4\]\] =
+symex_dynamic::dynamic_2_array#2\[\[5\]\] =
+symex_dynamic::dynamic_2_array#2\[\[6\]\] =
+symex_dynamic::dynamic_2_array#2\[\[7\]\] =
+symex_dynamic::dynamic_2_array#2\[\[8\]\] =
+symex_dynamic::dynamic_2_array#2\[\[9\]\] =
 symex_dynamic::dynamic_2_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
 This checks that field sensitvity is still applied to an array of size 10
-when the max is set to 10.
+when the max is set to 10.

jbmc/regression/jbmc/array-cell-sensitivity1/test.desc

@@ -1,16 +1,16 @@
 CORE
 Test
 --function Test.main --show-vcc
-symex_dynamic::dynamic_2_array#2\[\[0\]\] = symex_dynamic::dynamic_2_array#2\[0\]
-symex_dynamic::dynamic_2_array#2\[\[1\]\] = symex_dynamic::dynamic_2_array#2\[1\]
-symex_dynamic::dynamic_2_array#2\[\[2\]\] = symex_dynamic::dynamic_2_array#2\[2\]
-symex_dynamic::dynamic_2_array#2\[\[3\]\] = symex_dynamic::dynamic_2_array#2\[3\]
-symex_dynamic::dynamic_2_array#2\[\[4\]\] = symex_dynamic::dynamic_2_array#2\[4\]
-symex_dynamic::dynamic_2_array#2\[\[5\]\] = symex_dynamic::dynamic_2_array#2\[5\]
-symex_dynamic::dynamic_2_array#2\[\[6\]\] = symex_dynamic::dynamic_2_array#2\[6\]
-symex_dynamic::dynamic_2_array#2\[\[7\]\] = symex_dynamic::dynamic_2_array#2\[7\]
-symex_dynamic::dynamic_2_array#2\[\[8\]\] = symex_dynamic::dynamic_2_array#2\[8\]
-symex_dynamic::dynamic_2_array#2\[\[9\]\] = symex_dynamic::dynamic_2_array#2\[9\]
+symex_dynamic::dynamic_2_array#2\[\[0\]\] =
+symex_dynamic::dynamic_2_array#2\[\[1\]\] =
+symex_dynamic::dynamic_2_array#2\[\[2\]\] =
+symex_dynamic::dynamic_2_array#2\[\[3\]\] =
+symex_dynamic::dynamic_2_array#2\[\[4\]\] =
+symex_dynamic::dynamic_2_array#2\[\[5\]\] =
+symex_dynamic::dynamic_2_array#2\[\[6\]\] =
+symex_dynamic::dynamic_2_array#2\[\[7\]\] =
+symex_dynamic::dynamic_2_array#2\[\[8\]\] =
+symex_dynamic::dynamic_2_array#2\[\[9\]\] =
 symex_dynamic::dynamic_2_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc-incr-oneloop/Makefile

@@ -2,10 +2,10 @@ default: tests.log
 
 # Note the `perl -e` serves the purpose of providing timeout
 test:
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 8 ../../../src/cbmc/cbmc --slice-formula"
+	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --slice-formula"
 
 tests.log: ../test.pl
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 8 ../../../src/cbmc/cbmc --slice-formula"
+	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --slice-formula"
 
 clean:
 	@$(RM) *.log

regression/cbmc/Array_UF22/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG broken-smt-backend
 main.c
---arrays-uf-always --no-propagation
+--arrays-uf-always --no-propagation --no-simplify
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/Pointer21/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=0$

regression/cbmc/array-cell-sensitivity1/test.desc

@@ -1,15 +1,15 @@
 CORE
 test.c
 --show-vcc
-main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\]
-main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\]
-main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\]
-main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\]
-main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\]
-main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\]
-main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\]
-main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\]
-main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\]
+main::1::array!0@1#2\[\[1\]\] =
+main::1::array!0@1#2\[\[2\]\] =
+main::1::array!0@1#2\[\[3\]\] =
+main::1::array!0@1#2\[\[4\]\] =
+main::1::array!0@1#2\[\[5\]\] =
+main::1::array!0@1#2\[\[6\]\] =
+main::1::array!0@1#2\[\[7\]\] =
+main::1::array!0@1#2\[\[8\]\] =
+main::1::array!0@1#2\[\[9\]\] =
 main::1::array!0@1#3\[\[1\]\] =
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/array-cell-sensitivity10/test.desc

@@ -1,27 +1,27 @@
 CORE
 test.c
 --show-vcc
-main::1::array!0@1#2\[\[0\]\]..x = main::1::array!0@1#1\[0\].x
-main::1::array!0@1#2\[\[1\]\]..x = main::1::array!0@1#1\[1\].x
-main::1::array!0@1#2\[\[2\]\]..x = main::1::array!0@1#1\[2\].x
-main::1::array!0@1#2\[\[3\]\]..x = main::1::array!0@1#1\[3\].x
-main::1::array!0@1#2\[\[4\]\]..x = main::1::array!0@1#1\[4\].x
-main::1::array!0@1#2\[\[5\]\]..x = main::1::array!0@1#1\[5\].x
-main::1::array!0@1#2\[\[6\]\]..x = main::1::array!0@1#1\[6\].x
-main::1::array!0@1#2\[\[7\]\]..x = main::1::array!0@1#1\[7\].x
-main::1::array!0@1#2\[\[8\]\]..x = main::1::array!0@1#1\[8\].x
-main::1::array!0@1#2\[\[9\]\]..x = main::1::array!0@1#1\[9\].x
+main::1::array!0@1#2\[\[0\]\]..x =
+main::1::array!0@1#2\[\[1\]\]..x =
+main::1::array!0@1#2\[\[2\]\]..x =
+main::1::array!0@1#2\[\[3\]\]..x =
+main::1::array!0@1#2\[\[4\]\]..x =
+main::1::array!0@1#2\[\[5\]\]..x =
+main::1::array!0@1#2\[\[6\]\]..x =
+main::1::array!0@1#2\[\[7\]\]..x =
+main::1::array!0@1#2\[\[8\]\]..x =
+main::1::array!0@1#2\[\[9\]\]..x =
 main::1::array!0@1#3\[\[1\]\]..x =
-main::1::array!0@1#2\[\[0\]\]..y = main::1::array!0@1#1\[0\].y
-main::1::array!0@1#2\[\[1\]\]..y = main::1::array!0@1#1\[1\].y
-main::1::array!0@1#2\[\[2\]\]..y = main::1::array!0@1#1\[2\].y
-main::1::array!0@1#2\[\[3\]\]..y = main::1::array!0@1#1\[3\].y
-main::1::array!0@1#2\[\[4\]\]..y = main::1::array!0@1#1\[4\].y
-main::1::array!0@1#2\[\[5\]\]..y = main::1::array!0@1#1\[5\].y
-main::1::array!0@1#2\[\[6\]\]..y = main::1::array!0@1#1\[6\].y
-main::1::array!0@1#2\[\[7\]\]..y = main::1::array!0@1#1\[7\].y
-main::1::array!0@1#2\[\[8\]\]..y = main::1::array!0@1#1\[8\].y
-main::1::array!0@1#2\[\[9\]\]..y = main::1::array!0@1#1\[9\].y
+main::1::array!0@1#2\[\[0\]\]..y =
+main::1::array!0@1#2\[\[1\]\]..y =
+main::1::array!0@1#2\[\[2\]\]..y =
+main::1::array!0@1#2\[\[3\]\]..y =
+main::1::array!0@1#2\[\[4\]\]..y =
+main::1::array!0@1#2\[\[5\]\]..y =
+main::1::array!0@1#2\[\[6\]\]..y =
+main::1::array!0@1#2\[\[7\]\]..y =
+main::1::array!0@1#2\[\[8\]\]..y =
+main::1::array!0@1#2\[\[9\]\]..y =
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc/array-cell-sensitivity3/test.desc

@@ -1,16 +1,16 @@
 CORE
 test.c
 --show-vcc
-main::1::array!0@1#2\[\[0]\] = main::1::array!0@1#1\[0\]
-main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\]
-main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\]
-main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\]
-main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\]
-main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\]
-main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\]
-main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\]
-main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\]
-main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\]
+main::1::array!0@1#2\[\[0\]\] =
+main::1::array!0@1#2\[\[1\]\] =
+main::1::array!0@1#2\[\[2\]\] =
+main::1::array!0@1#2\[\[3\]\] =
+main::1::array!0@1#2\[\[4\]\] =
+main::1::array!0@1#2\[\[5\]\] =
+main::1::array!0@1#2\[\[6\]\] =
+main::1::array!0@1#2\[\[7\]\] =
+main::1::array!0@1#2\[\[8\]\] =
+main::1::array!0@1#2\[\[9\]\] =
 main::1::array!0@1#3\[\[1\]\] =
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/array-cell-sensitivity4/test.desc

@@ -1,15 +1,15 @@
 CORE
 test.c
 --show-vcc
-main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\]
-main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\]
-main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\]
-main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\]
-main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\]
-main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\]
-main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\]
-main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\]
-main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\]
+main::1::array!0@1#2\[\[1\]\] =
+main::1::array!0@1#2\[\[2\]\] =
+main::1::array!0@1#2\[\[3\]\] =
+main::1::array!0@1#2\[\[4\]\] =
+main::1::array!0@1#2\[\[5\]\] =
+main::1::array!0@1#2\[\[6\]\] =
+main::1::array!0@1#2\[\[7\]\] =
+main::1::array!0@1#2\[\[8\]\] =
+main::1::array!0@1#2\[\[9\]\] =
 main::1::array!0@1#3\[\[1\]\] =
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/array-cell-sensitivity5/test.desc

@@ -1,15 +1,15 @@
 CORE
 test.c
 --show-vcc
-symex_dynamic::dynamic_object1#2\[\[1\]\] = symex_dynamic::dynamic_object1#2\[1\]
-symex_dynamic::dynamic_object1#2\[\[2\]\] = symex_dynamic::dynamic_object1#2\[2\]
-symex_dynamic::dynamic_object1#2\[\[3\]\] = symex_dynamic::dynamic_object1#2\[3\]
-symex_dynamic::dynamic_object1#2\[\[4\]\] = symex_dynamic::dynamic_object1#2\[4\]
-symex_dynamic::dynamic_object1#2\[\[5\]\] = symex_dynamic::dynamic_object1#2\[5\]
-symex_dynamic::dynamic_object1#2\[\[6\]\] = symex_dynamic::dynamic_object1#2\[6\]
-symex_dynamic::dynamic_object1#2\[\[7\]\] = symex_dynamic::dynamic_object1#2\[7\]
-symex_dynamic::dynamic_object1#2\[\[8\]\] = symex_dynamic::dynamic_object1#2\[8\]
-symex_dynamic::dynamic_object1#2\[\[9\]\] = symex_dynamic::dynamic_object1#2\[9\]
+symex_dynamic::dynamic_object1#2\[\[1\]\] =
+symex_dynamic::dynamic_object1#2\[\[2\]\] =
+symex_dynamic::dynamic_object1#2\[\[3\]\] =
+symex_dynamic::dynamic_object1#2\[\[4\]\] =
+symex_dynamic::dynamic_object1#2\[\[5\]\] =
+symex_dynamic::dynamic_object1#2\[\[6\]\] =
+symex_dynamic::dynamic_object1#2\[\[7\]\] =
+symex_dynamic::dynamic_object1#2\[\[8\]\] =
+symex_dynamic::dynamic_object1#2\[\[9\]\] =
 symex_dynamic::dynamic_object1#3\[\[1\]\] =
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/array-cell-sensitivity6/test.desc

@@ -1,15 +1,15 @@
 CORE
 test.c
 --show-vcc
-symex_dynamic::dynamic_object1#2\[\[1\]\] = symex_dynamic::dynamic_object1#2\[1\]
-symex_dynamic::dynamic_object1#2\[\[2\]\] = symex_dynamic::dynamic_object1#2\[2\]
-symex_dynamic::dynamic_object1#2\[\[3\]\] = symex_dynamic::dynamic_object1#2\[3\]
-symex_dynamic::dynamic_object1#2\[\[4\]\] = symex_dynamic::dynamic_object1#2\[4\]
-symex_dynamic::dynamic_object1#2\[\[5\]\] = symex_dynamic::dynamic_object1#2\[5\]
-symex_dynamic::dynamic_object1#2\[\[6\]\] = symex_dynamic::dynamic_object1#2\[6\]
-symex_dynamic::dynamic_object1#2\[\[7\]\] = symex_dynamic::dynamic_object1#2\[7\]
-symex_dynamic::dynamic_object1#2\[\[8\]\] = symex_dynamic::dynamic_object1#2\[8\]
-symex_dynamic::dynamic_object1#2\[\[9\]\] = symex_dynamic::dynamic_object1#2\[9\]
+symex_dynamic::dynamic_object1#2\[\[1\]\] =
+symex_dynamic::dynamic_object1#2\[\[2\]\] =
+symex_dynamic::dynamic_object1#2\[\[3\]\] =
+symex_dynamic::dynamic_object1#2\[\[4\]\] =
+symex_dynamic::dynamic_object1#2\[\[5\]\] =
+symex_dynamic::dynamic_object1#2\[\[6\]\] =
+symex_dynamic::dynamic_object1#2\[\[7\]\] =
+symex_dynamic::dynamic_object1#2\[\[8\]\] =
+symex_dynamic::dynamic_object1#2\[\[9\]\] =
 symex_dynamic::dynamic_object1#3\[\[1\]\] =
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/array-cell-sensitivity7/test.desc

@@ -1,15 +1,15 @@
 CORE
 test.c
 --show-vcc
-main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\]
-main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\]
-main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\]
-main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\]
-main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\]
-main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\]
-main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\]
-main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\]
-main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\]
+main::1::array!0@1#2\[\[1\]\] =
+main::1::array!0@1#2\[\[2\]\] =
+main::1::array!0@1#2\[\[3\]\] =
+main::1::array!0@1#2\[\[4\]\] =
+main::1::array!0@1#2\[\[5\]\] =
+main::1::array!0@1#2\[\[6\]\] =
+main::1::array!0@1#2\[\[7\]\] =
+main::1::array!0@1#2\[\[8\]\] =
+main::1::array!0@1#2\[\[9\]\] =
 main::1::array!0@1#3\[\[0\]\] =
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/array-cell-sensitivity8/test.desc

@@ -1,26 +1,26 @@
 CORE
 test.c
 --show-vcc
-main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\]
-main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\]
-main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\]
-main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\]
-main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\]
-main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\]
-main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\]
-main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\]
-main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\]
+main::1::array!0@1#2\[\[1\]\] =
+main::1::array!0@1#2\[\[2\]\] =
+main::1::array!0@1#2\[\[3\]\] =
+main::1::array!0@1#2\[\[4\]\] =
+main::1::array!0@1#2\[\[5\]\] =
+main::1::array!0@1#2\[\[6\]\] =
+main::1::array!0@1#2\[\[7\]\] =
+main::1::array!0@1#2\[\[8\]\] =
+main::1::array!0@1#2\[\[9\]\] =
 main::1::array!0@1#2 =.*byte_extract_little_endian
-main::1::array!0@1#3\[\[0\]\] = main::1::array!0@1#2\[0\]
-main::1::array!0@1#3\[\[1\]\] = main::1::array!0@1#2\[1\]
-main::1::array!0@1#3\[\[2\]\] = main::1::array!0@1#2\[2\]
-main::1::array!0@1#3\[\[3\]\] = main::1::array!0@1#2\[3\]
-main::1::array!0@1#3\[\[4\]\] = main::1::array!0@1#2\[4\]
-main::1::array!0@1#3\[\[5\]\] = main::1::array!0@1#2\[5\]
-main::1::array!0@1#3\[\[6\]\] = main::1::array!0@1#2\[6\]
-main::1::array!0@1#3\[\[7\]\] = main::1::array!0@1#2\[7\]
-main::1::array!0@1#3\[\[8\]\] = main::1::array!0@1#2\[8\]
-main::1::array!0@1#3\[\[9\]\] = main::1::array!0@1#2\[9\]
+main::1::array!0@1#3\[\[0\]\] =
+main::1::array!0@1#3\[\[1\]\] =
+main::1::array!0@1#3\[\[2\]\] =
+main::1::array!0@1#3\[\[3\]\] =
+main::1::array!0@1#3\[\[4\]\] =
+main::1::array!0@1#3\[\[5\]\] =
+main::1::array!0@1#3\[\[6\]\] =
+main::1::array!0@1#3\[\[7\]\] =
+main::1::array!0@1#3\[\[8\]\] =
+main::1::array!0@1#3\[\[9\]\] =
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc/array-cell-sensitivity9/test.desc

@@ -1,27 +1,27 @@
 CORE
 test.c
 --show-vcc
-main::1::array!0@1#2\[\[0\]\]..x = main::1::array!0@1#1\[0\].x
-main::1::array!0@1#2\[\[1\]\]..x = main::1::array!0@1#1\[1\].x
-main::1::array!0@1#2\[\[2\]\]..x = main::1::array!0@1#1\[2\].x
-main::1::array!0@1#2\[\[3\]\]..x = main::1::array!0@1#1\[3\].x
-main::1::array!0@1#2\[\[4\]\]..x = main::1::array!0@1#1\[4\].x
-main::1::array!0@1#2\[\[5\]\]..x = main::1::array!0@1#1\[5\].x
-main::1::array!0@1#2\[\[6\]\]..x = main::1::array!0@1#1\[6\].x
-main::1::array!0@1#2\[\[7\]\]..x = main::1::array!0@1#1\[7\].x
-main::1::array!0@1#2\[\[8\]\]..x = main::1::array!0@1#1\[8\].x
-main::1::array!0@1#2\[\[9\]\]..x = main::1::array!0@1#1\[9\].x
+main::1::array!0@1#2\[\[0\]\]..x =
+main::1::array!0@1#2\[\[1\]\]..x =
+main::1::array!0@1#2\[\[2\]\]..x =
+main::1::array!0@1#2\[\[3\]\]..x =
+main::1::array!0@1#2\[\[4\]\]..x =
+main::1::array!0@1#2\[\[5\]\]..x =
+main::1::array!0@1#2\[\[6\]\]..x =
+main::1::array!0@1#2\[\[7\]\]..x =
+main::1::array!0@1#2\[\[8\]\]..x =
+main::1::array!0@1#2\[\[9\]\]..x =
 main::1::array!0@1#3\[\[1\]\]..x =
-main::1::array!0@1#2\[\[0\]\]..y = main::1::array!0@1#1\[0\].y
-main::1::array!0@1#2\[\[1\]\]..y = main::1::array!0@1#1\[1\].y
-main::1::array!0@1#2\[\[2\]\]..y = main::1::array!0@1#1\[2\].y
-main::1::array!0@1#2\[\[3\]\]..y = main::1::array!0@1#1\[3\].y
-main::1::array!0@1#2\[\[4\]\]..y = main::1::array!0@1#1\[4\].y
-main::1::array!0@1#2\[\[5\]\]..y = main::1::array!0@1#1\[5\].y
-main::1::array!0@1#2\[\[6\]\]..y = main::1::array!0@1#1\[6\].y
-main::1::array!0@1#2\[\[7\]\]..y = main::1::array!0@1#1\[7\].y
-main::1::array!0@1#2\[\[8\]\]..y = main::1::array!0@1#1\[8\].y
-main::1::array!0@1#2\[\[9\]\]..y = main::1::array!0@1#1\[9\].y
+main::1::array!0@1#2\[\[0\]\]..y =
+main::1::array!0@1#2\[\[1\]\]..y =
+main::1::array!0@1#2\[\[2\]\]..y =
+main::1::array!0@1#2\[\[3\]\]..y =
+main::1::array!0@1#2\[\[4\]\]..y =
+main::1::array!0@1#2\[\[5\]\]..y =
+main::1::array!0@1#2\[\[6\]\]..y =
+main::1::array!0@1#2\[\[7\]\]..y =
+main::1::array!0@1#2\[\[8\]\]..y =
+main::1::array!0@1#2\[\[9\]\]..y =
 ^EXIT=0$
 ^SIGNAL=0$
 --