Add support for incremental SMT traces containing C_bool

An "unsupported type" invariant violation would previously have been
encountered when attempting to generate traces featuring `c_bool_typet`.
This is due to `c_bool_typet` not being castable to
`integer_bitvector_typet`.

Author: thomasspriggs

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