Skip to content

Commit 15ec561

Browse files
Cleanup invariants in remove_vector
1 parent 63e9312 commit 15ec561

File tree

1 file changed

+4
-2
lines changed

1 file changed

+4
-2
lines changed

src/goto-programs/remove_vector.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -88,13 +88,14 @@ static void remove_vector(exprt &expr)
8888
expr.id()==ID_mod || expr.id()==ID_bitxor ||
8989
expr.id()==ID_bitand || expr.id()==ID_bitor)
9090
{
91+
DATA_INVARIANT(
92+
expr.operands().size() == 2, "binary operators have 2 operands");
9193
remove_vector(expr.type());
9294
array_typet array_type=to_array_type(expr.type());
9395

9496
mp_integer dimension;
9597
to_integer(array_type.size(), dimension);
9698

97-
assert(expr.operands().size()==2);
9899
const typet subtype=array_type.subtype();
99100
// do component-wise:
100101
// x+y -> vector(x[0]+y[0],x[1]+y[1],...)
@@ -114,13 +115,14 @@ static void remove_vector(exprt &expr)
114115
}
115116
else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
116117
{
118+
DATA_INVARIANT(
119+
expr.operands().size() == 1, "unary operators have one operands");
117120
remove_vector(expr.type());
118121
array_typet array_type=to_array_type(expr.type());
119122

120123
mp_integer dimension;
121124
to_integer(array_type.size(), dimension);
122125

123-
assert(expr.operands().size()==1);
124126
const typet subtype=array_type.subtype();
125127
// do component-wise:
126128
// -x -> vector(-x[0],-x[1],...)

0 commit comments

Comments
 (0)