Constant propagation for individual fields through byte extract

tautschnig · tautschnig · commit 619353432d43 · 2022-06-01T10:01:48.000Z
Field sensitivity in goto symex updates the full object as well as individual fields for divisible objects. The updates of individual fields, however, previously used index or member expressions on that full object. Consequently, constant propagation was only possible when the full-object assignment had a constant as the right-hand side. In some cases, however, only parts of the whole object might be constant. We are now able to constant propagate the fields covering those (constant) parts. Fixes: #6846
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc b/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.
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test.desc b/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$
diff --git a/regression/cbmc/Array_UF22/test.desc b/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$
diff --git a/regression/cbmc/Pointer21/test.desc b/regression/cbmc/Pointer21/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/array-cell-sensitivity1/test.desc b/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$
diff --git a/regression/cbmc/array-cell-sensitivity10/test.desc b/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$
 --
diff --git a/regression/cbmc/array-cell-sensitivity3/test.desc b/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$
diff --git a/regression/cbmc/array-cell-sensitivity4/test.desc b/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$
diff --git a/regression/cbmc/array-cell-sensitivity5/test.desc b/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$
diff --git a/regression/cbmc/array-cell-sensitivity6/test.desc b/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$
diff --git a/regression/cbmc/array-cell-sensitivity7/test.desc b/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$
diff --git a/regression/cbmc/array-cell-sensitivity8/test.desc b/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$
 --
diff --git a/regression/cbmc/array-cell-sensitivity9/test.desc b/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$
 --
diff --git a/regression/cbmc/field-sensitivity14/main.c b/regression/cbmc/field-sensitivity14/main.c
@@ -0,0 +1,20 @@
+#include <string.h>
+
+struct S
+{
+  int x;
+  int y;
+};
+
+int main()
+{
+  struct S s1, s2, s3;
+
+  s1.y = 42;
+  memcpy(&s2, &s1, sizeof(struct S));
+  __CPROVER_assert(s2.y == 42, "should propagate");
+
+  s3.x = 42;
+  memcpy(&s2, &s3, sizeof(struct S));
+  __CPROVER_assert(s2.x == 42, "should propagate");
+}
diff --git a/regression/cbmc/field-sensitivity14/test.desc b/regression/cbmc/field-sensitivity14/test.desc
diff --git a/regression/cbmc/field-sensitivity9/test.desc b/regression/cbmc/field-sensitivity9/test.desc
diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp
diff --git a/src/goto-symex/field_sensitivity.h b/src/goto-symex/field_sensitivity.h
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
diff --git a/unit/goto-symex/symex_assign.cpp b/unit/goto-symex/symex_assign.cpp

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE broken-smt-backend`
	`1`	`+CORE`
`2`	`2`	`main.c`
`3`	`3`	`--pointer-check`
`4`	`4`	`^EXIT=0$`