Merge pull request #6628 from thomasspriggs/tas/smt2_c_bool

Add 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;
+}

src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp

@@ -38,11 +38,12 @@ class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort
   void visit(const smt_bit_vector_constant_termt &bit_vector_constant) override
   {
     if(
-      const auto integer_type =
-        type_try_dynamic_cast<integer_bitvector_typet>(type_to_construct))
+      const auto bitvector_type =
+        type_try_dynamic_cast<bitvector_typet>(type_to_construct))
     {
       INVARIANT(
-        integer_type->get_width() == bit_vector_constant.get_sort().bit_width(),
+        bitvector_type->get_width() ==
+          bit_vector_constant.get_sort().bit_width(),
         "Width of smt bit vector term must match the width of bit vector "
         "type.");
       result = from_integer(bit_vector_constant.value(), type_to_construct);

unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp

@@ -1,20 +1,18 @@
 // Author: Diffblue Ltd.
 
-#include <testing-utils/use_catch.h>
+#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>
 
 #include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
-
 #include <solvers/smt2_incremental/smt_core_theory.h>
 #include <solvers/smt2_incremental/smt_terms.h>
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
-
 #include <testing-utils/invariant.h>
-
-#include <util/arith_tools.h>
-#include <util/bitvector_types.h>
-#include <util/mp_arith.h>
-#include <util/std_expr.h>
-#include <util/std_types.h>
+#include <testing-utils/use_catch.h>
 
 #include <string>
 
@@ -68,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),