diff --git a/regression/cbmc/field-sensitivity1/test.c b/regression/cbmc/field-sensitivity1/test.c
new file mode 100644
index 00000000000..cdd1b2f3b5d
--- /dev/null
+++ b/regression/cbmc/field-sensitivity1/test.c
@@ -0,0 +1,15 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+int main(int argc, char **argv)
+{
+  struct A a;
+  a.x = argc;
+  a.y = argc + 1;
+  assert(a.x == argc);
+}
diff --git a/regression/cbmc/field-sensitivity1/test.desc b/regression/cbmc/field-sensitivity1/test.desc
new file mode 100644
index 00000000000..1f475162f69
--- /dev/null
+++ b/regression/cbmc/field-sensitivity1/test.desc
@@ -0,0 +1,13 @@
+CORE
+test.c
+--show-vcc
+main::1::a!0@1#2\.\.x = main::argc!0@1#1
+main::1::a!0@1#2\.\.y = 1 \+ main::argc!0@1#1
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::a!\d+@\d+#\d+\.x
+main::1::a!\d+@\d+#\d+\.y
+--
+Fields A::x and A::y should be referred to as atomic symbols (a..x and a..y) but not using
+member operators (a.x and a.y).
diff --git a/regression/cbmc/field-sensitivity10/test.c b/regression/cbmc/field-sensitivity10/test.c
new file mode 100644
index 00000000000..c9131780795
--- /dev/null
+++ b/regression/cbmc/field-sensitivity10/test.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+  int z;
+};
+
+int main(int argc, char **argv)
+{
+  struct A a1, a2;
+  char *field = (argc % 2 ? (char *)&a1.y : (char *)&a2.z) + 1;
+  *field = (char)argc;
+  assert(a1.y == argc);
+  assert(a2.z == argc);
+}
diff --git a/regression/cbmc/field-sensitivity10/test.desc b/regression/cbmc/field-sensitivity10/test.desc
new file mode 100644
index 00000000000..b1d83b1c4c2
--- /dev/null
+++ b/regression/cbmc/field-sensitivity10/test.desc
@@ -0,0 +1,15 @@
+CORE
+test.c
+--show-vcc
+main::1::a1!0@1#2\.\.y =
+main::1::a2!0@1#2\.\.z =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::a[12]!\d+@\d+#\d+\.[xyz]
+--
+Fields A::y and A::z should be referred to as atomic symbols (a[12]..y and a[12]..z) but not using
+member operators (a[12].[xyz]).
+While the field is aliased with a different type, the typecast is successfully reduced to address just
+one field, rather than using a byte-update operation against the whole structure.
+This is like field-sensitivity8 except the pointer leads into the middle of a field.
diff --git a/regression/cbmc/field-sensitivity11/test.c b/regression/cbmc/field-sensitivity11/test.c
new file mode 100644
index 00000000000..f4d28e87fcc
--- /dev/null
+++ b/regression/cbmc/field-sensitivity11/test.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+int main(int argc, char **argv)
+{
+  struct A a1, a2;
+  a1.x = argc;
+  a1.y = argc + 1;
+  a2 = a1;
+  assert(a2.x == argc);
+}
diff --git a/regression/cbmc/field-sensitivity11/test.desc b/regression/cbmc/field-sensitivity11/test.desc
new file mode 100644
index 00000000000..ece83e62801
--- /dev/null
+++ b/regression/cbmc/field-sensitivity11/test.desc
@@ -0,0 +1,15 @@
+CORE
+test.c
+--show-vcc
+main::1::a1!0@1#2\.\.x = main::argc!0@1#1
+main::1::a1!0@1#2\.\.y = 1 \+ main::argc!0@1#1
+main::1::a2!0@1#2\.\.x = main::1::a1!0@1#2\.\.x
+main::1::a2!0@1#2\.\.y = main::1::a1!0@1#2\.\.y
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::a[12]!\d+@\d+#\d+\.[xy]
+--
+Fields A::x and A::y should be referred to as atomic symbols (a[12]..x and a[12]..y) but not using
+member operators (a[12].x and a[12].y).
+This test looks at the particular case of whole-struct assignment.
diff --git a/regression/cbmc/field-sensitivity12/test.c b/regression/cbmc/field-sensitivity12/test.c
new file mode 100644
index 00000000000..909681a043d
--- /dev/null
+++ b/regression/cbmc/field-sensitivity12/test.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+int main(int argc, char **argv)
+{
+  struct A a1, a2;
+  a1.x = argc;
+  a1.y = argc + 1;
+  struct A *aptr = argc % 2 ? &a1 : &a2;
+  *aptr = a1;
+  assert(a2.x == argc);
+}
diff --git a/regression/cbmc/field-sensitivity12/test.desc b/regression/cbmc/field-sensitivity12/test.desc
new file mode 100644
index 00000000000..357b6b7df6c
--- /dev/null
+++ b/regression/cbmc/field-sensitivity12/test.desc
@@ -0,0 +1,18 @@
+CORE
+test.c
+--show-vcc
+main::1::a1!0@1#2\.\.x = main::argc!0@1#1
+main::1::a1!0@1#2\.\.y = 1 \+ main::argc!0@1#1
+main::1::a1!0@1#3\.\.x = main::1::a1!0@1#2\.\.x
+main::1::a1!0@1#3\.\.y = main::1::a1!0@1#2\.\.y
+main::1::a2!0@1#2\.\.x =
+main::1::a2!0@1#2\.\.y =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::a[12]!\d+@\d+#\d+\.[xy]
+--
+Fields A::x and A::y should be referred to as atomic symbols (a[12]..x and a[12]..y) but not using
+member operators (a[12].x and a[12].y).
+This test looks at the particular case of whole-struct assignment when the target of the assignment
+is uncertain due to pointer indirection.
diff --git a/regression/cbmc/field-sensitivity13/test.c b/regression/cbmc/field-sensitivity13/test.c
new file mode 100644
index 00000000000..5853203765e
--- /dev/null
+++ b/regression/cbmc/field-sensitivity13/test.c
@@ -0,0 +1,23 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+struct B
+{
+  struct A a;
+  int z;
+};
+
+int main(int argc, char **argv)
+{
+  struct B b1, b2;
+  b1.a.x = argc;
+  b1.a.y = argc + 1;
+  struct A *aptr = argc % 2 ? &b1.a : &b2.a;
+  *aptr = b1.a;
+  assert(b2.a.x == argc);
+}
diff --git a/regression/cbmc/field-sensitivity13/test.desc b/regression/cbmc/field-sensitivity13/test.desc
new file mode 100644
index 00000000000..4b3898ea24a
--- /dev/null
+++ b/regression/cbmc/field-sensitivity13/test.desc
@@ -0,0 +1,18 @@
+CORE
+test.c
+--show-vcc
+main::1::b1!0@1#2\.\.a\.\.x = main::argc!0@1#1
+main::1::b1!0@1#2\.\.a\.\.y = 1 \+ main::argc!0@1#1
+main::1::b1!0@1#3\.\.a\.\.x = main::1::b1!0@1#2\.\.a\.\.x
+main::1::b1!0@1#3\.\.a\.\.y = main::1::b1!0@1#2\.\.a\.\.y
+main::1::b2!0@1#2\.\.a\.\.x =
+main::1::b2!0@1#2\.\.a\.\.y =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::b[12]!\d+@\d+#\d+\.a
+--
+Fields A::x and A::y should be referred to as atomic symbols (b[12]..a..x and b[12]..a..y) but not using
+member operators (b[12].a.x and b[12].a.y).
+This test looks at the particular case of whole-struct assignment when the target of the assignment
+is uncertain due to pointer indirection.
diff --git a/regression/cbmc/field-sensitivity2/test.c b/regression/cbmc/field-sensitivity2/test.c
new file mode 100644
index 00000000000..c3dec8642c8
--- /dev/null
+++ b/regression/cbmc/field-sensitivity2/test.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+int main(int argc, char **argv)
+{
+  struct A a1, a2;
+  struct A *aptr = argc % 2 ? &a1 : &a2;
+  aptr->x = argc;
+  aptr->y = argc + 1;
+  assert(a1.x == argc);
+  assert(a2.x == argc);
+}
diff --git a/regression/cbmc/field-sensitivity2/test.desc b/regression/cbmc/field-sensitivity2/test.desc
new file mode 100644
index 00000000000..622076d0a44
--- /dev/null
+++ b/regression/cbmc/field-sensitivity2/test.desc
@@ -0,0 +1,14 @@
+CORE
+test.c
+--show-vcc
+main::1::a1!0@1#2\.\.x =
+main::1::a1!0@1#2\.\.y =
+main::1::a2!0@1#2\.\.x =
+main::1::a2!0@1#2\.\.y =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::a[12]!\d+@\d+#\d+\.[xy]
+--
+Fields A::x and A::y should be referred to as atomic symbols (a[12]..x and a[12]..y) but not using
+member operators (a[12].x and a[12].y).
diff --git a/regression/cbmc/field-sensitivity3/test.c b/regression/cbmc/field-sensitivity3/test.c
new file mode 100644
index 00000000000..acbb45ba2e6
--- /dev/null
+++ b/regression/cbmc/field-sensitivity3/test.c
@@ -0,0 +1,19 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+int main(int argc, char **argv)
+{
+  struct A a1, a2, a3, a4;
+  struct A *aptr = argc % 2 ? &a1 : argc % 3 ? &a2 : argc % 5 ? &a3 : &a4;
+  aptr->x = argc;
+  aptr->y = argc + 1;
+  assert(a1.x == argc);
+  assert(a2.x == argc);
+  assert(a3.x == argc);
+  assert(a4.x == argc);
+}
diff --git a/regression/cbmc/field-sensitivity3/test.desc b/regression/cbmc/field-sensitivity3/test.desc
new file mode 100644
index 00000000000..ef0725b67eb
--- /dev/null
+++ b/regression/cbmc/field-sensitivity3/test.desc
@@ -0,0 +1,18 @@
+CORE
+test.c
+--show-vcc
+main::1::a1!0@1#2\.\.x =
+main::1::a1!0@1#2\.\.y =
+main::1::a2!0@1#2\.\.x =
+main::1::a2!0@1#2\.\.y =
+main::1::a3!0@1#2\.\.x =
+main::1::a3!0@1#2\.\.y =
+main::1::a4!0@1#2\.\.x =
+main::1::a4!0@1#2\.\.y =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::a[1234]!\d+@\d+#\d+\.[xy]
+--
+Fields A::x and A::y should be referred to as atomic symbols (a[1234]..x and a[1234]..y) but not using
+member operators (a[1234].x and a[1234].y).
diff --git a/regression/cbmc/field-sensitivity4/test.c b/regression/cbmc/field-sensitivity4/test.c
new file mode 100644
index 00000000000..1948eab9dcb
--- /dev/null
+++ b/regression/cbmc/field-sensitivity4/test.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+int main(int argc, char **argv)
+{
+  struct A a;
+  int *field = argc % 2 ? &a.x : &a.y;
+  *field = argc;
+  assert(a.x == argc);
+  assert(a.y == argc);
+}
diff --git a/regression/cbmc/field-sensitivity4/test.desc b/regression/cbmc/field-sensitivity4/test.desc
new file mode 100644
index 00000000000..9cc03329adf
--- /dev/null
+++ b/regression/cbmc/field-sensitivity4/test.desc
@@ -0,0 +1,16 @@
+FUTURE
+test.c
+--show-vcc
+main::1::a!0@1#2\.\.x =
+main::1::a!0@1#2\.\.y =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::a!\d+@\d+#\d+\.x
+main::1::a!\d+@\d+#\d+\.y
+--
+Fields A::x and A::y should be referred to as atomic symbols (a..x and a..y) but not using
+member operators (a.x and a.y).
+Currently this generates a byte_update operation followed by field expansion; could be improved
+if value_sett kept track of a finite set of constant offsets rather than degrading to unknown-offset
+whenever multiple offsets into the same allocation are merged.
diff --git a/regression/cbmc/field-sensitivity5/test.c b/regression/cbmc/field-sensitivity5/test.c
new file mode 100644
index 00000000000..21fb8ba957e
--- /dev/null
+++ b/regression/cbmc/field-sensitivity5/test.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+
+struct A
+{
+  int head;
+  struct A *tail;
+};
+
+int main(int argc, char **argv)
+{
+  struct A node1, node2, node3;
+  node1.tail = argc % 2 ? &node2 : &node3;
+  node2.tail = argc % 3 ? &node1 : &node3;
+  node3.tail = argc % 5 ? &node1 : &node2;
+  node1.tail->tail->tail->head = argc;
+  assert(node1.head == argc);
+}
diff --git a/regression/cbmc/field-sensitivity5/test.desc b/regression/cbmc/field-sensitivity5/test.desc
new file mode 100644
index 00000000000..161c5b5d6fb
--- /dev/null
+++ b/regression/cbmc/field-sensitivity5/test.desc
@@ -0,0 +1,14 @@
+CORE
+test.c
+--show-vcc
+main::1::node1!0@1#2\.\.head =
+main::1::node2!0@1#2\.\.head =
+main::1::node3!0@1#2\.\.head =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::node[123]!\d+@\d+#\d+\.head
+main::1::node[123]!\d+@\d+#\d+\.tail
+--
+Fields A::head and A::tail should be referred to as atomic symbols (node[123]..head and node[123]..tail)
+but not using member operators (node[123].(head)|(tail))
diff --git a/regression/cbmc/field-sensitivity6/test.c b/regression/cbmc/field-sensitivity6/test.c
new file mode 100644
index 00000000000..fb740339918
--- /dev/null
+++ b/regression/cbmc/field-sensitivity6/test.c
@@ -0,0 +1,21 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+struct B
+{
+  struct A a;
+};
+
+int main(int argc, char **argv)
+{
+  struct B b1, b2;
+  struct A *aptr = argc % 2 ? &b1.a : &b2.a;
+  aptr->x = argc;
+  assert(b1.a.x == argc);
+  assert(b2.a.x == argc);
+}
diff --git a/regression/cbmc/field-sensitivity6/test.desc b/regression/cbmc/field-sensitivity6/test.desc
new file mode 100644
index 00000000000..a976d428bb5
--- /dev/null
+++ b/regression/cbmc/field-sensitivity6/test.desc
@@ -0,0 +1,13 @@
+CORE
+test.c
+--show-vcc
+main::1::b1!0@1#2\.\.a\.\.x =
+main::1::b2!0@1#2\.\.a\.\.x =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::b1!\d+@\d+#\d+\.a
+main::1::b2!\d+@\d+#\d+\.a
+--
+Field A::x should be referred to as atomic symbols (b[12]..x) but not using
+member operators (b[12].a)
diff --git a/regression/cbmc/field-sensitivity7/test.c b/regression/cbmc/field-sensitivity7/test.c
new file mode 100644
index 00000000000..fc0ac772abe
--- /dev/null
+++ b/regression/cbmc/field-sensitivity7/test.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+  int z;
+};
+
+int main(int argc, char **argv)
+{
+  struct A a1, a2;
+  int *field = argc % 2 ? &a1.y : &a2.z;
+  *field = argc;
+  assert(a1.y == argc);
+  assert(a2.z == argc);
+}
diff --git a/regression/cbmc/field-sensitivity7/test.desc b/regression/cbmc/field-sensitivity7/test.desc
new file mode 100644
index 00000000000..7b97c8c7d95
--- /dev/null
+++ b/regression/cbmc/field-sensitivity7/test.desc
@@ -0,0 +1,15 @@
+CORE
+test.c
+--show-vcc
+main::1::a1!0@1#2\.\.y =
+main::1::a2!0@1#2\.\.z =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::a[12]!\d+@\d+#\d+\.[xyz]
+--
+Fields A::y and A::z should be referred to as atomic symbols (a[12]..y and a[12]..z) but not using
+member operators (a[12].[xyz]).
+Note the contrast with field-sensitivity4, where the fields the pointer may address are part of the
+same allocated object resulting in inability to resolve them, contrasting against this test where
+the fields belong to different objects.
diff --git a/regression/cbmc/field-sensitivity8/test.c b/regression/cbmc/field-sensitivity8/test.c
new file mode 100644
index 00000000000..b8aeb903e8f
--- /dev/null
+++ b/regression/cbmc/field-sensitivity8/test.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+  int z;
+};
+
+int main(int argc, char **argv)
+{
+  struct A a1, a2;
+  char *field = argc % 2 ? (char *)&a1.y : (char *)&a2.z;
+  *field = (char)argc;
+  assert(a1.y == argc);
+  assert(a2.z == argc);
+}
diff --git a/regression/cbmc/field-sensitivity8/test.desc b/regression/cbmc/field-sensitivity8/test.desc
new file mode 100644
index 00000000000..0d0db3d2bff
--- /dev/null
+++ b/regression/cbmc/field-sensitivity8/test.desc
@@ -0,0 +1,14 @@
+CORE
+test.c
+--show-vcc
+main::1::a1!0@1#2\.\.y =
+main::1::a2!0@1#2\.\.z =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::a[12]!\d+@\d+#\d+\.[xyz]
+--
+Fields A::y and A::z should be referred to as atomic symbols (a[12]..y and a[12]..z) but not using
+member operators (a[12].[xyz]).
+While the field is aliased with a different type, the typecast is successfully reduced to address just
+one field, rather than using a byte-update operation against the whole structure.
diff --git a/regression/cbmc/field-sensitivity9/test.c b/regression/cbmc/field-sensitivity9/test.c
new file mode 100644
index 00000000000..5852da21e18
--- /dev/null
+++ b/regression/cbmc/field-sensitivity9/test.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+  int z;
+};
+
+int main(int argc, char **argv)
+{
+  struct A a1, a2;
+  long long *field = argc % 2 ? (char *)&a1.y : (char *)&a2.z;
+  *field = argc;
+  assert(a1.y == argc);
+  assert(a2.z == argc);
+}
diff --git a/regression/cbmc/field-sensitivity9/test.desc b/regression/cbmc/field-sensitivity9/test.desc
new file mode 100644
index 00000000000..f6f973c33a7
--- /dev/null
+++ b/regression/cbmc/field-sensitivity9/test.desc
@@ -0,0 +1,18 @@
+CORE
+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
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+In this case because struct fields are addressed via a pointer cast to a larger type,
+we expect to have to use a whole-struct byte-update operation and then to re-expand the
+individual field symbols.