Skip to content

Commit fcbc914

Browse files
committed
Do not shadow "constraints"
Rename the method-local ones "intern_constraints" and "hash_constraints."
1 parent 04493f3 commit fcbc914

File tree

1 file changed

+7
-7
lines changed

1 file changed

+7
-7
lines changed

src/solvers/refinement/string_constraint_generator_comparison.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -191,7 +191,7 @@ string_constraint_generatort::add_axioms_for_hash_code(
191191
array_poolt &pool)
192192
{
193193
PRECONDITION(f.arguments().size() == 1);
194-
string_constraintst constraints;
194+
string_constraintst hash_constraints;
195195
const array_string_exprt str = get_string_expr(pool, f.arguments()[0]);
196196
const typet &return_type = f.type();
197197
const typet &index_type = str.length().type();
@@ -210,9 +210,9 @@ string_constraint_generatort::add_axioms_for_hash_code(
210210
and_exprt(
211211
notequal_exprt(str[i], it.first[i]),
212212
and_exprt(length_gt(str, i), is_positive(i))));
213-
constraints.existential.push_back(or_exprt(c1, or_exprt(c2, c3)));
213+
hash_constraints.existential.push_back(or_exprt(c1, or_exprt(c2, c3)));
214214
}
215-
return {hash, std::move(constraints)};
215+
return {hash, std::move(hash_constraints)};
216216
}
217217

218218
/// Lexicographic comparison of two strings
@@ -308,7 +308,7 @@ string_constraint_generatort::add_axioms_for_intern(
308308
const function_application_exprt &f)
309309
{
310310
PRECONDITION(f.arguments().size() == 1);
311-
string_constraintst constraints;
311+
string_constraintst intern_constraints;
312312
const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]);
313313
// For now we only enforce content equality and not pointer equality
314314
const typet &return_type=f.type();
@@ -326,14 +326,14 @@ string_constraint_generatort::add_axioms_for_intern(
326326
exprt::operandst disj;
327327
for(auto it : intern_of_string)
328328
disj.push_back(equal_exprt(intern, it.second));
329-
constraints.existential.push_back(disjunction(disj));
329+
intern_constraints.existential.push_back(disjunction(disj));
330330

331331
// WARNING: the specification may be incomplete or incorrect
332332
for(auto it : intern_of_string)
333333
if(it.second!=str)
334334
{
335335
symbol_exprt i = fresh_symbol("index_intern", index_type);
336-
constraints.existential.push_back(or_exprt(
336+
intern_constraints.existential.push_back(or_exprt(
337337
equal_exprt(it.second, intern),
338338
or_exprt(
339339
notequal_exprt(str.length(), it.first.length()),
@@ -344,5 +344,5 @@ string_constraint_generatort::add_axioms_for_intern(
344344
and_exprt(length_gt(str, i), is_positive(i)))))));
345345
}
346346

347-
return {intern, std::move(constraints)};
347+
return {intern, std::move(intern_constraints)};
348348
}

0 commit comments

Comments
 (0)