Fix arithmetic overflow in next_match/next_match_back Kani abstractions

Replace `kani::assume(a + w <= finger_back)` with the overflow-safe
form: assume `a <= finger_back` then `w <= finger_back - a`. This
avoids a usize overflow when a and w are both symbolic (kani::any())
and their sum could wrap around before the comparison.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: jrey8343

library/core/src/str/pattern.rs

@@ -488,8 +488,8 @@ unsafe impl<'a> Searcher<'a> for CharSearcher<'a> {
                 let a: usize = kani::any();
                 let w = self.utf8_size();
                 kani::assume(a >= self.finger);
-                kani::assume(w <= self.finger_back); // avoid overflow
-                kani::assume(a + w <= self.finger_back);
+                kani::assume(a <= self.finger_back); // avoid overflow in a + w
+                kani::assume(w <= self.finger_back - a);
                 self.finger = a + w;
                 Some((a, self.finger))
             } else {
@@ -627,8 +627,8 @@ unsafe impl<'a> ReverseSearcher<'a> for CharSearcher<'a> {
                 let a: usize = kani::any();
                 let w = self.utf8_size();
                 kani::assume(a >= self.finger);
-                kani::assume(w <= self.finger_back);
-                kani::assume(a + w <= self.finger_back);
+                kani::assume(a <= self.finger_back); // avoid overflow in a + w
+                kani::assume(w <= self.finger_back - a);
                 self.finger_back = a;
                 Some((a, a + w))
             } else {