Skip to content

Commit

Permalink
Remove mention of size in eval_string
Browse files Browse the repository at this point in the history
The length field is not actually used and maybe incorrect since
constraints are not necessarily added.
  • Loading branch information
romainbrenguier committed Mar 22, 2018
1 parent 4cca831 commit 71983b3
Showing 1 changed file with 1 addition and 4 deletions.
5 changes: 1 addition & 4 deletions src/solvers/refinement/string_builtin_function.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -96,15 +96,12 @@ optionalt<std::vector<mp_integer>> eval_string(
: eval_string(to_array_string_expr(ite.false_case()), get_value);
}

const auto size = numeric_cast<std::size_t>(get_value(a.length()));
const exprt content = get_value(a.content());
const auto &array = expr_try_dynamic_cast<array_exprt>(content);
if(!size || !array)
if(!array)
return {};

const auto &ops = array->operands();
INVARIANT(*size == ops.size(), "operands size should match string size");

std::vector<mp_integer> result;
const mp_integer unknown('?');
const auto &insert = std::back_inserter(result);
Expand Down

0 comments on commit 71983b3

Please sign in to comment.