Skip to content

Commit 787f76e

Browse files
committed
Refactor array overload of get_expr
So that the call for getting the index term can more easily be distinguished from the rest of the expression.
1 parent 9909511 commit 787f76e

File tree

1 file changed

+7
-9
lines changed

1 file changed

+7
-9
lines changed

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -382,16 +382,14 @@ array_exprt smt2_incremental_decision_proceduret::get_expr(
382382
elements.reserve(*size);
383383
for(std::size_t index = 0; index < size; ++index)
384384
{
385+
const auto index_term = ::convert_expr_to_smt(
386+
from_integer(index, index_type),
387+
object_map,
388+
pointer_sizes_map,
389+
object_size_function.make_application,
390+
is_dynamic_object_function.make_application);
385391
elements.push_back(get_expr(
386-
smt_array_theoryt::select(
387-
array,
388-
::convert_expr_to_smt(
389-
from_integer(index, index_type),
390-
object_map,
391-
pointer_sizes_map,
392-
object_size_function.make_application,
393-
is_dynamic_object_function.make_application)),
394-
type.element_type()));
392+
smt_array_theoryt::select(array, index_term), type.element_type()));
395393
}
396394
return array_exprt{elements, type};
397395
}

0 commit comments

Comments
 (0)