Skip to content

Commit f76ffdc

Browse files
author
Joel Allred
committed
TEMP FIX TO REMOVE WHEN REBASING ON diffblue#4546
1 parent 4baeac9 commit f76ffdc

File tree

1 file changed

+9
-3
lines changed

1 file changed

+9
-3
lines changed

src/solvers/strings/string_constraint_generator_comparison.cpp

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -206,12 +206,18 @@ string_constraint_generatort::add_axioms_for_hash_code(
206206
{
207207
const symbol_exprt i = fresh_symbol("index_hash", index_type);
208208
const equal_exprt c1(it.second, hash);
209-
const notequal_exprt c2(it.first.length(), str.length());
209+
const notequal_exprt c2(
210+
array_pool.get_or_create_length(it.first),
211+
array_pool.get_or_create_length(str));
210212
const and_exprt c3(
211-
equal_exprt(it.first.length(), str.length()),
213+
equal_exprt(
214+
array_pool.get_or_create_length(it.first),
215+
array_pool.get_or_create_length(str)),
212216
and_exprt(
213217
notequal_exprt(str[i], it.first[i]),
214-
and_exprt(greater_than(str.length(), i), is_positive(i))));
218+
and_exprt(
219+
greater_than(array_pool.get_or_create_length(str), i),
220+
is_positive(i))));
215221
hash_constraints.existential.push_back(or_exprt(c1, or_exprt(c2, c3)));
216222
}
217223
return {hash, std::move(hash_constraints)};

0 commit comments

Comments
 (0)