@@ -80,16 +80,18 @@ SCENARIO(
8080 integer_typet (), from_integer (3 , integer_typet ()));
8181
8282 // int val1[3] = {1, 2, 3}
83- exprt val1 = array_exprt (array_type);
84- val1.operands ().push_back (from_integer (1 , integer_typet ()));
85- val1.operands ().push_back (from_integer (2 , integer_typet ()));
86- val1.operands ().push_back (from_integer (3 , integer_typet ()));
83+ exprt::operandst val1_op;
84+ val1_op.push_back (from_integer (1 , integer_typet ()));
85+ val1_op.push_back (from_integer (2 , integer_typet ()));
86+ val1_op.push_back (from_integer (3 , integer_typet ()));
87+ exprt val1 = array_exprt (val1_op, array_type);
8788
8889 // int val2[3] = {1, 4, 5}
89- exprt val2 = array_exprt (array_type);
90- val2.operands ().push_back (from_integer (1 , integer_typet ()));
91- val2.operands ().push_back (from_integer (4 , integer_typet ()));
92- val2.operands ().push_back (from_integer (5 , integer_typet ()));
90+ exprt::operandst val2_op;
91+ val2_op.push_back (from_integer (1 , integer_typet ()));
92+ val2_op.push_back (from_integer (4 , integer_typet ()));
93+ val2_op.push_back (from_integer (5 , integer_typet ()));
94+ exprt val2 = array_exprt (val2_op, array_type);
9395
9496 // index_exprt for reading from an array
9597 const index_exprt i0 =
@@ -131,9 +133,9 @@ SCENARIO(
131133 REQUIRE_FALSE (modified);
132134 REQUIRE_FALSE (cast_result->is_top ());
133135 REQUIRE_FALSE (cast_result->is_bottom ());
134- REQUIRE (util.read_index (cast_result, i0) == val1.op0 () );
135- REQUIRE (util.read_index (cast_result, i1) == val1.op1 () );
136- REQUIRE (util.read_index (cast_result, i2) == val1.op2 () );
136+ REQUIRE (util.read_index (cast_result, i0) == val1.operands ()[ 0 ] );
137+ REQUIRE (util.read_index (cast_result, i1) == val1.operands ()[ 1 ] );
138+ REQUIRE (util.read_index (cast_result, i2) == val1.operands ()[ 2 ] );
137139
138140 // Is optimal
139141 REQUIRE (result == op1);
@@ -161,7 +163,7 @@ SCENARIO(
161163 REQUIRE (modified);
162164 REQUIRE_FALSE (cast_result->is_top ());
163165 REQUIRE_FALSE (cast_result->is_bottom ());
164- REQUIRE (util.read_index (cast_result, i0) == val1.op0 () );
166+ REQUIRE (util.read_index (cast_result, i0) == val1.operands ()[ 0 ] );
165167 REQUIRE (util.read_index (cast_result, i1) == nil_exprt ());
166168 REQUIRE (util.read_index (cast_result, i2) == nil_exprt ());
167169
@@ -219,9 +221,9 @@ SCENARIO(
219221 REQUIRE_FALSE (modified);
220222 REQUIRE_FALSE (cast_result->is_top ());
221223 REQUIRE_FALSE (cast_result->is_bottom ());
222- REQUIRE (util.read_index (cast_result, i0) == val1.op0 () );
223- REQUIRE (util.read_index (cast_result, i1) == val1.op1 () );
224- REQUIRE (util.read_index (cast_result, i2) == val1.op2 () );
224+ REQUIRE (util.read_index (cast_result, i0) == val1.operands ()[ 0 ] );
225+ REQUIRE (util.read_index (cast_result, i1) == val1.operands ()[ 1 ] );
226+ REQUIRE (util.read_index (cast_result, i2) == val1.operands ()[ 2 ] );
225227
226228 // Is optimal
227229 REQUIRE (result == op1);
@@ -335,9 +337,9 @@ SCENARIO(
335337 REQUIRE (modified);
336338 REQUIRE_FALSE (cast_result->is_top ());
337339 REQUIRE_FALSE (cast_result->is_bottom ());
338- REQUIRE (util.read_index (cast_result, i0) == val1.op0 () );
339- REQUIRE (util.read_index (cast_result, i1) == val1.op1 () );
340- REQUIRE (util.read_index (cast_result, i2) == val1.op2 () );
340+ REQUIRE (util.read_index (cast_result, i0) == val1.operands ()[ 0 ] );
341+ REQUIRE (util.read_index (cast_result, i1) == val1.operands ()[ 1 ] );
342+ REQUIRE (util.read_index (cast_result, i2) == val1.operands ()[ 2 ] );
341343
342344 // Is optimal
343345 REQUIRE (result != op1);
@@ -452,9 +454,9 @@ SCENARIO(
452454 REQUIRE_FALSE (modified);
453455 REQUIRE_FALSE (cast_result->is_top ());
454456 REQUIRE_FALSE (cast_result->is_bottom ());
455- REQUIRE (util.read_index (cast_result, i0) == val1.op0 () );
456- REQUIRE (util.read_index (cast_result, i1) == val1.op1 () );
457- REQUIRE (util.read_index (cast_result, i2) == val1.op2 () );
457+ REQUIRE (util.read_index (cast_result, i0) == val1.operands ()[ 0 ] );
458+ REQUIRE (util.read_index (cast_result, i1) == val1.operands ()[ 1 ] );
459+ REQUIRE (util.read_index (cast_result, i2) == val1.operands ()[ 2 ] );
458460
459461 // Is optimal
460462 REQUIRE (result == op1);
0 commit comments