Add unit/regression tests for nondet_symbol SMT2

Add test for nondet_symbol translation

Author: Enrico Steffinlongo

regression/cbmc-incr-smt2/nondeterministic-int-assert/nondet_symbol.c

@@ -0,0 +1,11 @@
+extern int undefined_function();
+
+int main()
+{
+  int nondet1 = undefined_function();
+  __CPROVER_assume(nondet1 == 10);
+  __CPROVER_assert(nondet1 < 11, "");
+  __CPROVER_assert(undefined_function() == 0, "");
+
+  __CPROVER_assert(undefined_function() == undefined_function(), "");
+}

regression/cbmc-incr-smt2/nondeterministic-int-assert/nondet_symbol.desc

@@ -0,0 +1,12 @@
+CORE
+nondet_symbol.c
+
+Passing problem to incremental SMT2 solving
+\[main\.assertion\.1\] line 7 assertion: SUCCESS
+\[main\.assertion\.2\] line 8 assertion: FAILURE
+\[main\.assertion\.3\] line 10 assertion: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that running cbmc with the `--incremental-smt2-solver` supports nondet_symbol expressions.

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -119,6 +119,20 @@ TEST_CASE("\"symbol_exprt\" to smt term conversion", "[core][smt2_incremental]")
     smt_identifier_termt("foo", smt_bool_sortt{}));
 }
 
+TEST_CASE(
+  "\"nondet_symbol_exprt\" to smt term conversion",
+  "[core][smt2_incremental]")
+{
+  auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::i386);
+  CHECK(
+    test.convert(nondet_symbol_exprt{"nondet_symbol1", bool_typet{}}) ==
+    smt_identifier_termt("nondet_symbol1", smt_bool_sortt{}));
+  CHECK(
+    test.convert(
+      nondet_symbol_exprt{"nondet_symbol2", bitvector_typet{ID_bv, 42}}) ==
+    smt_identifier_termt{"nondet_symbol2", smt_bit_vector_sortt{42}});
+}
+
 TEST_CASE(
   "\"exprt\" to smt term conversion for constants/literals",
   "[core][smt2_incremental]")
@@ -1350,7 +1364,7 @@ TEST_CASE("expr to smt conversion for type casts", "[core][smt2_incremental]")
         exprt{false_exprt{}});
       const smt_termt from_term = test.convert(from_expr);
       const std::size_t width = GENERATE(1, 8, 16, 32, 64);
-      const typecast_exprt cast{from_expr, bitvector_typet{ID_bv, width}};
+      const typecast_exprt cast{from_expr, bv_typet(width)};
       CHECK(
         test.convert(cast) == smt_core_theoryt::if_then_else(
                                 from_term,

unit/solvers/smt2_incremental/module_dependencies.txt

@@ -1,3 +1,4 @@
+goto-symex
 solvers/smt2_incremental
 testing-utils
 util

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -23,6 +23,7 @@
 // means that we get error messages showing the smt formula expressed as SMT2
 // strings instead of `{?}` being printed. It works because catch uses the
 // appropriate overload of `operator<<` where it exists.
+#include <goto-symex/path_storage.h>
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
 
 #include <deque>
@@ -306,6 +307,49 @@ TEST_CASE(
             "B0", {}, smt_identifier_termt{"bar", smt_bit_vector_sortt{8}}}});
     }
   }
+  SECTION("Handle single nondet_symbol")
+  {
+    // Using the standard way to create nondet_symbol_exprt.
+    ::symex_nondet_generatort generator;
+    const nondet_symbol_exprt nondet_symbol0 =
+      generator(bool_typet{}, source_locationt{});
+    const smt_identifier_termt nondet_symbol_term0{
+      nondet_symbol0.get_identifier(), smt_bool_sortt{}};
+    test.sent_commands.clear();
+    test.procedure.handle(nondet_symbol0);
+    REQUIRE(
+      test.sent_commands ==
+      std::vector<smt_commandt>{
+        smt_declare_function_commandt{nondet_symbol_term0, {}},
+        smt_define_function_commandt{"B0", {}, nondet_symbol_term0}});
+  }
+  SECTION("Handle multiple nested nondet_symbol")
+  {
+    ::symex_nondet_generatort generator;
+    const nondet_symbol_exprt nondet_symbol1 =
+      generator(bv_typet(42), source_locationt{});
+    const smt_identifier_termt nondet_symbol_term1{
+      nondet_symbol1.get_identifier(), smt_bit_vector_sortt{42}};
+    const nondet_symbol_exprt nondet_symbol2 =
+      generator(bv_typet(42), source_locationt{});
+    const smt_identifier_termt nondet_symbol_term2{
+      nondet_symbol2.get_identifier(), smt_bit_vector_sortt{42}};
+    // Check that the 2 calls to the generator returns unique nondet_symbols.
+    REQUIRE(
+      nondet_symbol1.get_identifier() != nondet_symbol_term2.identifier());
+    test.sent_commands.clear();
+    test.procedure.handle(equal_exprt{nondet_symbol1, nondet_symbol2});
+    // Checking that we defined 2 symbols and that they are correctly compared.
+    REQUIRE(
+      test.sent_commands ==
+      std::vector<smt_commandt>{
+        smt_declare_function_commandt{nondet_symbol_term1, {}},
+        smt_declare_function_commandt{nondet_symbol_term2, {}},
+        smt_define_function_commandt{
+          "B0",
+          {},
+          smt_core_theoryt::equal(nondet_symbol_term1, nondet_symbol_term2)}});
+  }
 }
 
 TEST_CASE(