Skip to content

Commit

Permalink
SMT2 back-end: parse c_bool values
Browse files Browse the repository at this point in the history
We had the ability to parse literals of c_bool type, but parse_rec did
not consider this type.

Fixes: diffblue#7308
  • Loading branch information
tautschnig committed Nov 29, 2022
1 parent d60295d commit 70e4573
Show file tree
Hide file tree
Showing 3 changed files with 4 additions and 3 deletions.
4 changes: 2 additions & 2 deletions regression/cbmc/Bool/bool3.desc
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
CORE
bool3.c

--json-ui
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
VERIFICATION FAILED
--
^warning: ignoring
1 change: 1 addition & 0 deletions regression/validate-trace-xml-schema/check.py
Original file line number Diff line number Diff line change
Expand Up @@ -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'],
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/smt2/smt2_conv.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Expand Down

0 comments on commit 70e4573

Please sign in to comment.