Skip to content

Commit 784edde

Browse files
author
Joel Allred
committed
Improve doc at creation of array if-exprt
1 parent 860a438 commit 784edde

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

src/solvers/strings/array_pool.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -93,7 +93,9 @@ array_string_exprt array_poolt::make_char_array_for_char_pointer(
9393
to_array_type(t.type()).size(),
9494
to_array_type(f.type()).size()));
9595
// BEWARE: this expression is possibly type-inconsistent and must not be
96-
// used for any purposes other than passing it to concretisation
96+
// used for any purposes other than passing it to concretization.
97+
// Array if-exprts must be replaced (using substitute_array_access) before
98+
// passing the lemmas to the solver.
9799
return to_array_string_expr(if_exprt(if_expr.cond(), t, f, array_type));
98100
}
99101
const bool is_constant_array =

0 commit comments

Comments
 (0)