Skip to content

Commit e12c7ee

Browse files
tautschnigDaniel Kroening
authored and
Daniel Kroening
committed
Use disjunction instead of deprecated or_exprt constructor
This is more efficient, type safe, and supports even more cleanup here.
1 parent 85cb6dc commit e12c7ee

File tree

1 file changed

+5
-10
lines changed

1 file changed

+5
-10
lines changed

src/goto-programs/goto_convert.cpp

+5-10
Original file line numberDiff line numberDiff line change
@@ -1151,18 +1151,13 @@ exprt goto_convertt::case_guard(
11511151
return equal_exprt(value, case_op.at(0));
11521152
else
11531153
{
1154-
exprt dest = exprt(ID_or, bool_typet());
1155-
dest.reserve_operands(case_op.size());
1154+
exprt::operandst disjuncts;
1155+
disjuncts.reserve(case_op.size());
11561156

1157-
forall_expr(it, case_op)
1158-
{
1159-
dest.add_to_operands(equal_exprt(value, *it));
1160-
}
1161-
INVARIANT(
1162-
case_op.size() == dest.operands().size(),
1163-
"case guard conversion should preserve the number of cases");
1157+
for(const auto &op : case_op)
1158+
disjuncts.push_back(equal_exprt(value, op));
11641159

1165-
return dest;
1160+
return disjunction(disjuncts);
11661161
}
11671162
}
11681163

0 commit comments

Comments
 (0)