diff --git a/regression/cbmc-incr-smt2/arrays/address_of_two_array_sizes.c b/regression/cbmc-incr-smt2/arrays/address_of_two_array_sizes.c
new file mode 100644
index 00000000000..642f8a7933a
--- /dev/null
+++ b/regression/cbmc-incr-smt2/arrays/address_of_two_array_sizes.c
@@ -0,0 +1,19 @@
+int main()
+{
+  int example_array1[10000];
+  char example_array2[20000];
+  void *foo;
+  __CPROVER_bool choice = nondet___CPROVER_bool();
+  if(choice)
+    foo = example_array1;
+  else
+    foo = example_array2;
+  __CPROVER_assert(
+    foo != example_array1 || __CPROVER_OBJECT_SIZE(foo) == 40000,
+    "Array condition 1");
+  __CPROVER_assert(__CPROVER_OBJECT_SIZE(foo) == 40000, "Array condition 2");
+  __CPROVER_assert(
+    foo != example_array2 || __CPROVER_OBJECT_SIZE(foo) == 20000,
+    "Array condition 3");
+  __CPROVER_assert(__CPROVER_OBJECT_SIZE(foo) == 20000, "Array condition 4");
+}
diff --git a/regression/cbmc-incr-smt2/arrays/address_of_two_array_sizes.desc b/regression/cbmc-incr-smt2/arrays/address_of_two_array_sizes.desc
new file mode 100644
index 00000000000..61ce18f498f
--- /dev/null
+++ b/regression/cbmc-incr-smt2/arrays/address_of_two_array_sizes.desc
@@ -0,0 +1,17 @@
+CORE
+address_of_two_array_sizes.c
+--verbosity 10
+Passing problem to incremental SMT2 solving
+address_of\(main\:\:1\:\:example_array1\!0\@1\[0\]\)
+address_of\(main\:\:1\:\:example_array2\!0\@1\[0\]\)
+line \d+ Array condition 1: SUCCESS
+line \d+ Array condition 2: FAILURE
+line \d+ Array condition 3: SUCCESS
+line \d+ Array condition 4: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that __CPROVER_OBJECT_SIZE returns the expected results in the case where
+the pointer passed to it may point to one of 2 arrays, where each array has a
+different size.
diff --git a/regression/cbmc-incr-smt2/arrays/array_address_of.c b/regression/cbmc-incr-smt2/arrays/array_address_of.c
index 91c0935edad..47ad2310f7a 100644
--- a/regression/cbmc-incr-smt2/arrays/array_address_of.c
+++ b/regression/cbmc-incr-smt2/arrays/array_address_of.c
@@ -1,8 +1,13 @@
 int main()
 {
-  int example_array[10000];
-  __CPROVER_assert(
-    __CPROVER_OBJECT_SIZE(example_array) == 40000, "Array condition 1");
-  __CPROVER_assert(
-    __CPROVER_OBJECT_SIZE(example_array) == 40001, "Array condition 2");
+  int example_array1[10000];
+  int example_array2[10000];
+  int *foo;
+  int choice;
+  if(choice)
+    foo = example_array1;
+  else
+    foo = example_array2;
+  __CPROVER_assert(__CPROVER_OBJECT_SIZE(foo) == 40000, "Array condition 1");
+  __CPROVER_assert(__CPROVER_OBJECT_SIZE(foo) == 40001, "Array condition 2");
 }
diff --git a/regression/cbmc-incr-smt2/arrays/array_address_of.desc b/regression/cbmc-incr-smt2/arrays/array_address_of.desc
index 61907cb03f6..6e5c016fdf5 100644
--- a/regression/cbmc-incr-smt2/arrays/array_address_of.desc
+++ b/regression/cbmc-incr-smt2/arrays/array_address_of.desc
@@ -1,7 +1,9 @@
 CORE
 array_address_of.c
-
+--verbosity 10
 Passing problem to incremental SMT2 solving
+address_of\(main\:\:1\:\:example_array1\!0\@1\[0\]\)
+address_of\(main\:\:1\:\:example_array2\!0\@1\[0\]\)
 line \d+ Array condition 1: SUCCESS
 line \d+ Array condition 2: FAILURE
 ^EXIT=10$