Merge pull request #7400 from tautschnig/bugfixes/7308-c_bool

SMT2 back-end: parse c_bool values

Author: tautschnig

regression/cbmc/Bool/bool3.desc

@@ -1,8 +1,8 @@
 CORE
 bool3.c
-
+--json-ui
 ^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION FAILED$
+VERIFICATION FAILED
 --
 ^warning: ignoring

regression/validate-trace-xml-schema/check.py

@@ -56,6 +56,7 @@
     # this uses json-ui (fails for a different reason actually, but should also
     #   fail because of command line incompatibility)
     ['json1', 'test.desc'],
+    ['Bool', 'bool3.desc'],
     ['Empty_struct3', 'test.desc'],
     # uses show-goto-functions
     ['reachability-slice', 'test.desc'],

src/solvers/smt2/smt2_conv.cpp

@@ -638,7 +638,7 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &type)
     type.id() == ID_integer || type.id() == ID_rational ||
     type.id() == ID_real || type.id() == ID_c_enum ||
     type.id() == ID_c_enum_tag || type.id() == ID_fixedbv ||
-    type.id() == ID_floatbv)
+    type.id() == ID_floatbv || type.id() == ID_c_bool)
   {
     return parse_literal(src, type);
   }