Skip to content

Commit eaa5805

Browse files
Fix typos in compute_inverse_function
1 parent e1b188d commit eaa5805

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/solvers/strings/string_constraint_instantiation.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -157,7 +157,7 @@ static exprt
157157
compute_inverse_function(const exprt &qvar, const exprt &val, const exprt &f)
158158
{
159159
exprt positive, negative;
160-
// number of time the element should be added (can be negative)
160+
// number of times the element should be added (can be negative)
161161
// qvar has to be equal to val - f(0) if it appears positively in f
162162
// (i.e. if f(qvar)=f(0) + qvar) and f(0) - val if it appears negatively
163163
// in f. So we start by computing val - f(0).
@@ -180,7 +180,7 @@ compute_inverse_function(const exprt &qvar, const exprt &val, const exprt &f)
180180
it->second == 0,
181181
string_refinement_invariantt(
182182
"a proper function must have exactly one "
183-
"occurrences after reduction, or it cancelled out, and it does not"
183+
"occurrence after reduction, or it cancelled out, and it does not"
184184
" have one"));
185185
}
186186

0 commit comments

Comments
 (0)