Is verification of pointer arithmetic less difficult than pointer modification?

Question

I was attempting to use WP to verify memchr from musl libc, which fundamentally boils down to:

void *memchr(const void *src, int c, size_t n)
{
  const unsigned char *s = src;
  for (; n && *s != c; s++, n--);
  return n ? (void *)s : 0;
}

I had a number of problems involving anything to do with s. However, when I rewrote the function as:

void *memchr(const void *src, int c, size_t n)
{
  const unsigned char *s = src;
  size_t i = 0;
  for (; i < n && *(s + i) != c; i++);
  return (i < n) ? ((void *) s + i) : 0;
}

all of the necessary properties went through without issue. The only difference between the two is that the first version modifies s and n while the second uses pointer arithmetic on s + i.

Is there a significant difference between how Frama-C or the underlying solvers handle the two cases?