Test support for incremental SMT traces containing C_bool

Author: thomasspriggs

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

@@ -0,0 +1,13 @@
+CORE
+stdbool_example.c
+--incremental-smt2-solver 'z3 --smt2 -in' --trace
+Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+VERIFICATION FAILED
+equal=FALSE\s*\([0 ]+\)
+equal=TRUE\s*\([0 ]+1\)
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that running cbmc with the `--incremental-smt2-solver` argument can be used
+to generate a trace including values of C bool variables.

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

@@ -0,0 +1,10 @@
+#include <stdbool.h>
+
+int main()
+{
+  int x, y;
+  bool equal = x == y;
+  __CPROVER_assert(equal, "Assert of integer equality.");
+  __CPROVER_assert(!equal, "Assert of not integer equality.");
+  return 0;
+}

unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp

@@ -2,6 +2,7 @@
 
 #include <util/arith_tools.h>
 #include <util/bitvector_types.h>
+#include <util/c_types.h>
 #include <util/mp_arith.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
@@ -65,6 +66,8 @@ TEST_CASE("Value expr construction from smt.", "[core][smt2_incremental]")
   std::tie(input_term, expected_result) = GENERATE(
     rowt{smt_bool_literal_termt{true}, true_exprt{}},
     rowt{smt_bool_literal_termt{false}, false_exprt{}},
+    rowt{smt_bit_vector_constant_termt{0, 8}, from_integer(0, c_bool_typet(8))},
+    rowt{smt_bit_vector_constant_termt{1, 8}, from_integer(1, c_bool_typet(8))},
     UNSIGNED_BIT_VECTOR_TESTS(8),
     SIGNED_BIT_VECTOR_TESTS(8),
     UNSIGNED_BIT_VECTOR_TESTS(16),