Skip to content

Commit 15d0bd2

Browse files
committed
Fix support for structs with a single member
Fixes regression/cbmc/Initialization7/test.desc
1 parent af598d9 commit 15d0bd2

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

src/solvers/smt2_incremental/struct_encoding.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,8 @@ typet struct_encodingt::encode(typet type) const
4444

4545
static exprt encode(const struct_exprt &struct_expr)
4646
{
47+
if(struct_expr.operands().size() == 1)
48+
return struct_expr.operands().front();
4749
return concatenation_exprt{struct_expr.operands(), struct_expr.type()};
4850
}
4951

0 commit comments

Comments
 (0)