Skip to content

Commit 70e4573

Browse files
committed
SMT2 back-end: parse c_bool values
We had the ability to parse literals of c_bool type, but parse_rec did not consider this type. Fixes: diffblue#7308
1 parent d60295d commit 70e4573

File tree

3 files changed

+4
-3
lines changed

3 files changed

+4
-3
lines changed

regression/cbmc/Bool/bool3.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
bool3.c
3-
3+
--json-ui
44
^EXIT=10$
55
^SIGNAL=0$
6-
^VERIFICATION FAILED$
6+
VERIFICATION FAILED
77
--
88
^warning: ignoring

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,7 @@
5656
# this uses json-ui (fails for a different reason actually, but should also
5757
# fail because of command line incompatibility)
5858
['json1', 'test.desc'],
59+
['Bool', 'bool3.desc'],
5960
['Empty_struct3', 'test.desc'],
6061
# uses show-goto-functions
6162
['reachability-slice', 'test.desc'],

src/solvers/smt2/smt2_conv.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -638,7 +638,7 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &type)
638638
type.id() == ID_integer || type.id() == ID_rational ||
639639
type.id() == ID_real || type.id() == ID_c_enum ||
640640
type.id() == ID_c_enum_tag || type.id() == ID_fixedbv ||
641-
type.id() == ID_floatbv)
641+
type.id() == ID_floatbv || type.id() == ID_c_bool)
642642
{
643643
return parse_literal(src, type);
644644
}

0 commit comments

Comments
 (0)