Skip to content

Commit 80b914e

Browse files
committed
Also skip flattening zero-sized arrays
when converting to SMT2 queries.
1 parent f585e60 commit 80b914e

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

Diff for: src/solvers/smt2/smt2_conv.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -2695,8 +2695,8 @@ void smt2_convt::flatten_array(const exprt &expr)
26952695
PRECONDITION(size_expr.id() == ID_constant);
26962696

26972697
mp_integer size = numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
2698-
CHECK_RETURN_WITH_DIAGNOSTICS(size != 0, "can't convert zero-sized array");
2699-
2698+
if(size == 0)
2699+
return;
27002700
out << "(let ((?far ";
27012701
convert_expr(expr);
27022702
out << ")) ";

0 commit comments

Comments
 (0)