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
index 7698360fdb2..df055e68c43 100644
--- 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.
\ No newline at end of file
+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
index 9246fe4d352..40608dd5d66 100644
--- 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-incr-oneloop/Makefile b/regression/cbmc-incr-oneloop/Makefile
index 2d19ae61d72..35d25c57e2c 100644
--- a/regression/cbmc-incr-oneloop/Makefile
+++ b/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
diff --git a/regression/cbmc/Array_UF22/test.desc b/regression/cbmc/Array_UF22/test.desc
index 67011369611..2aabbf95187 100644
--- 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
index 5136794fb58..39c491ba8bb 100644
--- 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
index 89d5291e18f..8660167f711 100644
--- 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
index 1061132428e..09a6e142f2c 100644
--- 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
index da0a7025fda..bc2967a5861 100644
--- 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
index 9f7da1d30cc..1507d095b49 100644
--- 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
index 923d28fc391..52dff950071 100644
--- 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
index cdbfa2c3aac..be4de5fb666 100644
--- 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
index ffd25206574..4ab41c78401 100644
--- 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
index da8e78103f9..3cb74addf6c 100644
--- 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
index 1a7d5937ac2..84fc8b0d9bd 100644
--- 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
new file mode 100644
index 00000000000..69de6730b89
--- /dev/null
+++ 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
new file mode 100644
index 00000000000..d1748c78147
--- /dev/null
+++ b/regression/cbmc/field-sensitivity14/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^Generated \d+ VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+All properties in this example can be solved by combining field-sensitive
+constant propagation and simplification.
diff --git a/regression/cbmc/field-sensitivity9/test.desc b/regression/cbmc/field-sensitivity9/test.desc
index f6f973c33a7..599668c7fe6 100644
--- a/regression/cbmc/field-sensitivity9/test.desc
+++ b/regression/cbmc/field-sensitivity9/test.desc
@@ -3,12 +3,12 @@ test.c
 --show-vcc
 main::1::a1!0@1#1 =
 main::1::a2!0@1#1 =
-main::1::a1!0@1#2\.\.x = main::1::a1!0@1#1\.x
-main::1::a1!0@1#2\.\.y = main::1::a1!0@1#1\.y
-main::1::a1!0@1#2\.\.z = main::1::a1!0@1#1\.z
-main::1::a2!0@1#2\.\.x = main::1::a2!0@1#1\.x
-main::1::a2!0@1#2\.\.y = main::1::a2!0@1#1\.y
-main::1::a2!0@1#2\.\.z = main::1::a2!0@1#1\.z
+main::1::a1!0@1#2\.\.x =
+main::1::a1!0@1#2\.\.y =
+main::1::a1!0@1#2\.\.z =
+main::1::a2!0@1#2\.\.x =
+main::1::a2!0@1#2\.\.y =
+main::1::a2!0@1#2\.\.z =
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/cbmc/member_bounds3/test.desc b/regression/cbmc/member_bounds3/test.desc
index f1e76cee227..3441cbd1973 100644
--- a/regression/cbmc/member_bounds3/test.desc
+++ b/regression/cbmc/member_bounds3/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+KNOWNBUG broken-smt-backend
 main.c
 --no-simplify
 ^VERIFICATION SUCCESSFUL$
@@ -6,3 +6,5 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+--
+See #6101 for a discussion as to whether this should be supported at all.
diff --git a/regression/cbmc/member_bounds4/test.desc b/regression/cbmc/member_bounds4/test.desc
index f1e76cee227..3441cbd1973 100644
--- a/regression/cbmc/member_bounds4/test.desc
+++ b/regression/cbmc/member_bounds4/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+KNOWNBUG broken-smt-backend
 main.c
 --no-simplify
 ^VERIFICATION SUCCESSFUL$
@@ -6,3 +6,5 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+--
+See #6101 for a discussion as to whether this should be supported at all.
diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp
index a71fde73733..7a1c8c988b3 100644
--- a/src/goto-symex/field_sensitivity.cpp
+++ b/src/goto-symex/field_sensitivity.cpp
@@ -52,14 +52,14 @@ exprt field_sensitivityt::apply(
     !write && expr.id() == ID_member &&
     to_member_expr(expr).struct_op().id() == ID_struct)
   {
-    return simplify_expr(std::move(expr), ns);
+    return simplify_opt(std::move(expr), ns);
   }
 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(
     !write && expr.id() == ID_index &&
     to_index_expr(expr).array().id() == ID_array)
   {
-    return simplify_expr(std::move(expr), ns);
+    return simplify_opt(std::move(expr), ns);
   }
 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(expr.id() == ID_member)
@@ -95,7 +95,8 @@ exprt field_sensitivityt::apply(
     // encoding the index access into an array as an individual symbol rather
     // than only the full array
     index_exprt &index = to_index_expr(expr);
-    simplify(index.index(), ns);
+    if(should_simplify)
+      simplify(index.index(), ns);
 
     if(
       is_ssa_expr(index.array()) && index.array().type().id() == ID_array &&
@@ -105,7 +106,8 @@ exprt field_sensitivityt::apply(
       // SSA expression
       ssa_exprt tmp = to_ssa_expr(index.array());
       auto l2_index = state.rename(index.index(), ns);
-      l2_index.simplify(ns);
+      if(should_simplify)
+        l2_index.simplify(ns);
       bool was_l2 = !tmp.get_level_2().empty();
       exprt l2_size =
         state.rename(to_array_type(index.array().type()).size(), ns).get();
@@ -227,16 +229,20 @@ void field_sensitivityt::field_assignments(
   const namespacet &ns,
   goto_symex_statet &state,
   const ssa_exprt &lhs,
+  const exprt &rhs,
   symex_targett &target,
   bool allow_pointer_unsoundness)
 {
   const exprt lhs_fs = apply(ns, state, lhs, false);
 
-  bool run_apply_bak = run_apply;
-  run_apply = false;
-  field_assignments_rec(
-    ns, state, lhs_fs, lhs, target, allow_pointer_unsoundness);
-  run_apply = run_apply_bak;
+  if(lhs != lhs_fs)
+  {
+    bool run_apply_bak = run_apply;
+    run_apply = false;
+    field_assignments_rec(
+      ns, state, lhs_fs, rhs, target, allow_pointer_unsoundness);
+    run_apply = run_apply_bak;
+  }
 }
 
 /// Assign to the individual fields \p lhs_fs of a non-expanded symbol \p lhs.
@@ -246,24 +252,19 @@ void field_sensitivityt::field_assignments(
 /// \param ns: a namespace to resolve type symbols/tag types
 /// \param state: symbolic execution state
 /// \param lhs_fs: expanded symbol
-/// \param lhs: non-expanded symbol
+/// \param ssa_rhs: right-hand-side value to assign
 /// \param target: symbolic execution equation store
 /// \param allow_pointer_unsoundness: allow pointer unsoundness
 void field_sensitivityt::field_assignments_rec(
   const namespacet &ns,
   goto_symex_statet &state,
   const exprt &lhs_fs,
-  const exprt &lhs,
+  const exprt &ssa_rhs,
   symex_targett &target,
   bool allow_pointer_unsoundness)
 {
-  if(lhs == lhs_fs)
-    return;
-  else if(is_ssa_expr(lhs_fs))
+  if(is_ssa_expr(lhs_fs))
   {
-    exprt ssa_rhs = state.rename(lhs, ns).get();
-    simplify(ssa_rhs, ns);
-
     const ssa_exprt ssa_lhs = state
                                 .assignment(
                                   to_ssa_expr(lhs_fs),
@@ -284,9 +285,10 @@ void field_sensitivityt::field_assignments_rec(
       state.source,
       symex_targett::assignment_typet::STATE);
   }
-  else if(lhs.type().id() == ID_struct || lhs.type().id() == ID_struct_tag)
+  else if(
+    ssa_rhs.type().id() == ID_struct || ssa_rhs.type().id() == ID_struct_tag)
   {
-    const struct_typet &type = to_struct_type(ns.follow(lhs.type()));
+    const struct_typet &type = to_struct_type(ns.follow(ssa_rhs.type()));
     const struct_union_typet::componentst &components = type.components();
 
     PRECONDITION(
@@ -296,7 +298,8 @@ void field_sensitivityt::field_assignments_rec(
     exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
     for(const auto &comp : components)
     {
-      const member_exprt member_rhs(lhs, comp.get_name(), comp.type());
+      const exprt member_rhs =
+        simplify_opt(member_exprt{ssa_rhs, comp.get_name(), comp.type()}, ns);
       const exprt &member_lhs = *fs_it;
 
       field_assignments_rec(
@@ -305,7 +308,7 @@ void field_sensitivityt::field_assignments_rec(
     }
   }
 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
-  else if(const auto &type = type_try_dynamic_cast<array_typet>(lhs.type()))
+  else if(const auto &type = type_try_dynamic_cast<array_typet>(ssa_rhs.type()))
   {
     const std::size_t array_size =
       numeric_cast_v<std::size_t>(to_constant_expr(type->size()));
@@ -317,7 +320,8 @@ void field_sensitivityt::field_assignments_rec(
     exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
     for(std::size_t i = 0; i < array_size; ++i)
     {
-      const index_exprt index_rhs(lhs, from_integer(i, type->index_type()));
+      const exprt index_rhs = simplify_opt(
+        index_exprt{ssa_rhs, from_integer(i, type->index_type())}, ns);
       const exprt &index_lhs = *fs_it;
 
       field_assignments_rec(
@@ -329,10 +333,11 @@ void field_sensitivityt::field_assignments_rec(
   else if(lhs_fs.has_operands())
   {
     PRECONDITION(
-      lhs.has_operands() && lhs_fs.operands().size() == lhs.operands().size());
+      ssa_rhs.has_operands() &&
+      lhs_fs.operands().size() == ssa_rhs.operands().size());
 
     exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
-    for(const exprt &op : lhs.operands())
+    for(const exprt &op : ssa_rhs.operands())
     {
       field_assignments_rec(
         ns, state, *fs_it, op, target, allow_pointer_unsoundness);
@@ -363,3 +368,11 @@ bool field_sensitivityt::is_divisible(const ssa_exprt &expr) const
 
   return false;
 }
+
+exprt field_sensitivityt::simplify_opt(exprt e, const namespacet &ns) const
+{
+  if(!should_simplify)
+    return e;
+
+  return simplify_expr(std::move(e), ns);
+}
diff --git a/src/goto-symex/field_sensitivity.h b/src/goto-symex/field_sensitivity.h
index 8c657a6b3c6..fc7a8543e0b 100644
--- a/src/goto-symex/field_sensitivity.h
+++ b/src/goto-symex/field_sensitivity.h
@@ -84,8 +84,10 @@ class field_sensitivityt
 public:
   /// \param max_array_size: maximum size for which field sensitivity will be
   ///   applied to array cells
-  explicit field_sensitivityt(std::size_t max_array_size)
-    : max_field_sensitivity_array_size(max_array_size)
+  /// \param should_simplify: simplify expressions
+  field_sensitivityt(std::size_t max_array_size, bool should_simplify)
+    : max_field_sensitivity_array_size(max_array_size),
+      should_simplify(should_simplify)
   {
   }
 
@@ -96,12 +98,15 @@ class field_sensitivityt
   /// \param ns: a namespace to resolve type symbols/tag types
   /// \param state: symbolic execution state
   /// \param lhs: non-expanded symbol
+  /// \param rhs: right-hand-side value that was used in the preceding update of
+  ///   the full object
   /// \param target: symbolic execution equation store
   /// \param allow_pointer_unsoundness: allow pointer unsoundness
   void field_assignments(
     const namespacet &ns,
     goto_symex_statet &state,
     const ssa_exprt &lhs,
+    const exprt &rhs,
     symex_targett &target,
     bool allow_pointer_unsoundness);
 
@@ -157,13 +162,17 @@ class field_sensitivityt
 
   const std::size_t max_field_sensitivity_array_size;
 
+  const bool should_simplify;
+
   void field_assignments_rec(
     const namespacet &ns,
     goto_symex_statet &state,
     const exprt &lhs_fs,
-    const exprt &lhs,
+    const exprt &ssa_rhs,
     symex_targett &target,
     bool allow_pointer_unsoundness);
+
+  exprt simplify_opt(exprt e, const namespacet &ns) const;
 };
 
 #endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index da88f723b9b..06f7e304d68 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -31,13 +31,14 @@ static void get_l1_name(exprt &expr);
 goto_symex_statet::goto_symex_statet(
   const symex_targett::sourcet &_source,
   std::size_t max_field_sensitive_array_size,
+  bool should_simplify,
   guard_managert &manager,
   std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider)
   : goto_statet(manager),
     source(_source),
     guard_manager(manager),
     symex_target(nullptr),
-    field_sensitivity(max_field_sensitive_array_size),
+    field_sensitivity(max_field_sensitive_array_size, should_simplify),
     record_events({true}),
     fresh_l2_name_provider(fresh_l2_name_provider)
 {
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index e78e2415755..ac3206e05ed 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -44,6 +44,7 @@ class goto_symex_statet final : public goto_statet
   goto_symex_statet(
     const symex_targett::sourcet &,
     std::size_t max_field_sensitive_array_size,
+    bool should_simplify,
     guard_managert &manager,
     std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider);
   ~goto_symex_statet();
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index f4358ba0e8b..da621d2cbcc 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -209,7 +209,12 @@ void symex_assignt::assign_non_struct_symbol(
   {
     // Split composite symbol lhs into its components
     state.field_sensitivity.field_assignments(
-      ns, state, l1_lhs, target, symex_config.allow_pointer_unsoundness);
+      ns,
+      state,
+      l1_lhs,
+      assignment.rhs,
+      target,
+      symex_config.allow_pointer_unsoundness);
     // Erase the composite symbol from our working state. Note that we need to
     // have it in the propagation table and the value set while doing the field
     // assignments, thus we cannot skip putting it in there above.
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 3be0f67f28e..ca7f174f06c 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -422,6 +422,7 @@ std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
   auto state = util_make_unique<statet>(
     symex_targett::sourcet(entry_point_id, start_function->body),
     symex_config.max_field_sensitivity_array_size,
+    symex_config.simplify_opt,
     guard_manager,
     [storage](const irep_idt &id) { return storage->get_unique_l2_index(id); });
 
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 0302da75c94..e8f3b8289e6 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -1835,6 +1835,46 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
       }
     }
   }
+  else if(expr.op().id() == ID_array)
+  {
+    const array_typet &array_type = to_array_type(expr.op().type());
+    const auto &element_bit_width =
+      pointer_offset_bits(array_type.element_type(), ns);
+    if(element_bit_width.has_value() && *element_bit_width > 0)
+    {
+      if(*offset > 0 && *offset * 8 % *element_bit_width == 0)
+      {
+        const auto elements_to_erase =
+          numeric_cast_v<std::size_t>((*offset * 8) / *element_bit_width);
+        array_exprt slice = to_array_expr(expr.op());
+        slice.operands().erase(
+          slice.operands().begin(),
+          slice.operands().begin() +
+            std::min(elements_to_erase, slice.operands().size()));
+        slice.type().size() =
+          from_integer(slice.operands().size(), slice.type().size().type());
+        byte_extract_exprt be = expr;
+        be.op() = slice;
+        be.offset() = from_integer(0, expr.offset().type());
+        return changed(simplify_byte_extract(be));
+      }
+      else if(*offset == 0 && *el_size % *element_bit_width == 0)
+      {
+        const auto elements_to_keep =
+          numeric_cast_v<std::size_t>(*el_size / *element_bit_width);
+        array_exprt slice = to_array_expr(expr.op());
+        if(slice.operands().size() > elements_to_keep)
+        {
+          slice.operands().resize(elements_to_keep);
+          slice.type().size() =
+            from_integer(slice.operands().size(), slice.type().size().type());
+          byte_extract_exprt be = expr;
+          be.op() = slice;
+          return changed(simplify_byte_extract(be));
+        }
+      }
+    }
+  }
 
   // try to refine it down to extracting from a member or an index in an array
   auto subexpr =
diff --git a/unit/goto-symex/apply_condition.cpp b/unit/goto-symex/apply_condition.cpp
index 058f48d72d7..ff843e99a34 100644
--- a/unit/goto-symex/apply_condition.cpp
+++ b/unit/goto-symex/apply_condition.cpp
@@ -44,10 +44,12 @@ SCENARIO(
   guard_managert guard_manager;
   std::size_t count = 0;
   auto fresh_name = [&count](const irep_idt &) { return count++; };
-  goto_symex_statet state{source,
-                          DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
-                          guard_manager,
-                          fresh_name};
+  goto_symex_statet state{
+    source,
+    DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
+    true,
+    guard_manager,
+    fresh_name};
 
   goto_statet goto_state{state};
   const exprt renamed_b = state.rename<L2>(b, ns).get();
diff --git a/unit/goto-symex/goto_symex_state.cpp b/unit/goto-symex/goto_symex_state.cpp
index 2f47b76c6a1..1935d184cfb 100644
--- a/unit/goto-symex/goto_symex_state.cpp
+++ b/unit/goto-symex/goto_symex_state.cpp
@@ -40,7 +40,11 @@ SCENARIO(
     return fresh_name_count++;
   };
   goto_symex_statet state{
-    source, DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE, manager, fresh_name};
+    source,
+    DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
+    true,
+    manager,
+    fresh_name};
 
   // Initialize dirty field of state
   incremental_dirtyt dirty;
diff --git a/unit/goto-symex/symex_assign.cpp b/unit/goto-symex/symex_assign.cpp
index aa417d8062a..00e006ff75c 100644
--- a/unit/goto-symex/symex_assign.cpp
+++ b/unit/goto-symex/symex_assign.cpp
@@ -51,7 +51,11 @@ SCENARIO(
     return fresh_name_count++;
   };
   goto_symex_statet state{
-    source, DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE, manager, fresh_name};
+    source,
+    DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
+    true,
+    manager,
+    fresh_name};
 
   // Initialize dirty field of state
   incremental_dirtyt dirty;
@@ -273,14 +277,9 @@ SCENARIO(
           REQUIRE(as_symbol);
           REQUIRE(as_symbol->get_identifier() == "struct1!0#2..field1");
         }
-        THEN("Expand step RHS is struct1!0#1.field1")
+        THEN("Expand step RHS is 234")
         {
-          ssa_exprt struct1_v1{struct1_sym};
-          struct1_v1.set_level_0(0);
-          struct1_v1.set_level_2(1);
-          REQUIRE(
-            expand_step.ssa_rhs ==
-            member_exprt{struct1_v1, "field1", int_type});
+          REQUIRE(expand_step.ssa_rhs == from_integer(234, int_type));
         }
       }
     }
diff --git a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp
index de6cce39c0f..bc46fac9c74 100644
--- a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp
+++ b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp
@@ -54,10 +54,12 @@ SCENARIO(
   guard_managert guard_manager;
   std::size_t count = 0;
   auto fresh_name = [&count](const irep_idt &) { return count++; };
-  goto_symex_statet state{source,
-                          DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
-                          guard_manager,
-                          fresh_name};
+  goto_symex_statet state{
+    source,
+    DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
+    true,
+    guard_manager,
+    fresh_name};
 
   GIVEN("A value set in which pointer symbol `ptr1` only points to `&value1`")
   {
@@ -249,7 +251,7 @@ SCENARIO(
     // struct_symbol..pointer_field <- &value1
     {
       field_sensitivityt field_sensitivity{
-        DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE};
+        DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE, true};
       const exprt index_fs =
         field_sensitivity.apply(ns, state, member_l1.get(), true);
       value_set.assign(index_fs, address1_l1.get(), ns, false, false);