Add non-determinism to array_address_of test

This test is intended to cover incremental SMT decision procedure
support expressions of the form `address_of(array[0])`. These occur as
part of the conversion from array to pointer, which may be implicitly
introduced by applying `__CPROVER_OBJECT_SIZE` to an array. The existing
test is not actually checking this conversion due to it being simplified
away during constant propagation. The introduction of non-determinism in
this commit prevents constant propagation from removing expressions of
this form, so that their conversion will actually be tested.

Author: thomasspriggs

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");
 }

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$