Add array_of_exprt unit and regression tests

Author: Enrico Steffinlongo

regression/cbmc-incr-smt2/arrays/array_of.c

@@ -0,0 +1,12 @@
+int main()
+{
+  int example_array[10000];
+  unsigned int index;
+  __CPROVER_assume(index < 999);
+
+  __CPROVER_array_set(example_array, 43);
+  __CPROVER_assert(example_array[index] != 43, "False array condition");
+
+  __CPROVER_array_set(example_array, 42);
+  __CPROVER_assert(example_array[index] == 42, "Valid array condition");
+}

regression/cbmc-incr-smt2/arrays/array_of.desc

@@ -0,0 +1,13 @@
+CORE
+array_of.c
+
+Passing problem to incremental SMT2 solving
+line \d+ False array condition: FAILURE
+line \d+ Valid array condition: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test using __CPROVER_array_set consisting in an `array_of` node which sets all values of a given
+array to a given value.
+This test uses a forall SMT statement.

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -614,5 +614,36 @@ TEST_CASE(
       smt_declare_function_commandt{index_term, {}},
       smt_assert_commandt{smt_core_theoryt::equal(
         foo_term, smt_array_theoryt::select(array_term, index_term))}};
+    REQUIRE(test.sent_commands == expected_commands);
+  }
+  SECTION("array_of_exprt - all elements set to a given value")
+  {
+    const array_of_exprt array_of_expr{
+      from_integer(42, value_type), array_type};
+    test.sent_commands.clear();
+    test.procedure.set_to(
+      equal_exprt{
+        foo.symbol_expr(), index_exprt{array_of_expr, index.symbol_expr()}},
+      true);
+    const auto foo_term = smt_identifier_termt{"foo", smt_bit_vector_sortt{8}};
+    const auto array_term = smt_identifier_termt{
+      "array_0",
+      smt_array_sortt{smt_bit_vector_sortt{32}, smt_bit_vector_sortt{8}}};
+    const auto index_term =
+      smt_identifier_termt{"index", smt_bit_vector_sortt{32}};
+    const auto forall_term = smt_identifier_termt{
+      id2string(array_term.identifier()) + "_index", smt_bit_vector_sortt{32}};
+    const std::vector<smt_commandt> expected_commands{
+      smt_declare_function_commandt{foo_term, {}},
+      smt_declare_function_commandt{array_term, {}},
+      smt_assert_commandt{smt_forall_termt{
+        {forall_term},
+        smt_core_theoryt::equal(
+          smt_array_theoryt::select(array_term, forall_term),
+          smt_bit_vector_constant_termt{42, 8})}},
+      smt_declare_function_commandt{index_term, {}},
+      smt_assert_commandt{smt_core_theoryt::equal(
+        foo_term, smt_array_theoryt::select(array_term, index_term))}};
+    REQUIRE(test.sent_commands == expected_commands);
   }
 }