Skip to content

Commit faf21d0

Browse files
committed
Implement converting void type
for the SMT2 queries.
1 parent 199b231 commit faf21d0

File tree

1 file changed

+9
-0
lines changed

1 file changed

+9
-0
lines changed

src/solvers/smt2/smt2_conv.cpp

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2214,6 +2214,10 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
22142214
convert_typecast(tmp);
22152215
}
22162216
}
2217+
else if(src_type.id() == ID_empty)
2218+
{
2219+
convert_expr(src);
2220+
}
22172221
else
22182222
{
22192223
std::ostringstream e_str;
@@ -4626,6 +4630,11 @@ void smt2_convt::convert_type(const typet &type)
46264630
{
46274631
convert_type(c_bit_field_replacement_type(to_c_bit_field_type(type), ns));
46284632
}
4633+
else if(type.id() == ID_empty)
4634+
{
4635+
// the NONDET(void) is in fact of type char
4636+
out << "(_ BitVec " << boolbv_width(char_type()) << " )";
4637+
}
46294638
else
46304639
{
46314640
UNEXPECTEDCASE("unsupported type: "+type.id_string());

0 commit comments

Comments
 (0)