Skip to content

Commit a2a4feb

Browse files
committed
Use instantiate() when flattening array_comprehension_exprt
Uses the capabilities of binding_exprt instead of relying on the unrelated replace_exprt to do the right thing.
1 parent 65c42a3 commit a2a4feb

File tree

1 file changed

+1
-3
lines changed

1 file changed

+1
-3
lines changed

src/solvers/flattening/boolbv.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,6 @@ Author: Daniel Kroening, [email protected]
1818
#include <util/floatbv_expr.h>
1919
#include <util/magic.h>
2020
#include <util/mp_arith.h>
21-
#include <util/replace_expr.h>
2221
#include <util/simplify_expr.h>
2322
#include <util/std_expr.h>
2423
#include <util/string2int.h>
@@ -258,8 +257,7 @@ bvt boolbvt::convert_array_comprehension(const array_comprehension_exprt &expr)
258257
{
259258
exprt counter=from_integer(i, counter_type);
260259

261-
exprt body = expr.body();
262-
replace_expr(expr.arg(), counter, body);
260+
exprt body = expr.instantiate({counter});
263261

264262
const bvt &tmp = convert_bv(body);
265263

0 commit comments

Comments
 (0)