File tree 1 file changed +4
-4
lines changed
1 file changed +4
-4
lines changed Original file line number Diff line number Diff line change @@ -162,8 +162,8 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
162
162
// a4 && a5 <=> a6:
163
163
// forall n:[from_index,|haystack|-|needle|].
164
164
// !contains || n < offset ==>
165
- // haystack[n] != needle[0] || ... ||
166
- // haystack[n+|needle|-1] != needle[|needle|-1]
165
+ // haystack[n] != needle[0] || ... ||
166
+ // haystack[n+|needle|-1] != needle[|needle|-1]
167
167
symbol_exprt qvar2=fresh_univ_index (" QA_index_of_string_2" , index_type);
168
168
mp_integer sub_length;
169
169
assert (!to_integer (needle.length (), sub_length));
@@ -284,8 +284,8 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
284
284
// a4 && a5 <=> a6:
285
285
// forall n:[0, min(from_index,|haystack|-|needle|)].
286
286
// !contains || n > offset ==>
287
- // haystack[n] != needle[0] || ... ||
288
- // haystack[n+|substring|-1] != needle[|substring|-1]
287
+ // haystack[n] != needle[0] || ... ||
288
+ // haystack[n+|substring|-1] != needle[|substring|-1]
289
289
symbol_exprt qvar2=fresh_univ_index (" QA_index_of_string_2" , index_type);
290
290
mp_integer sub_length;
291
291
assert (!to_integer (needle.length (), sub_length));
You can’t perform that action at this time.
0 commit comments