Invalid regression test generated for hash algorithm

[operasfantom]

Code

#include <inttypes.h>
#include <stdio.h>

/**
 * @brief 8-bit XOR algorithm implementation
 *
 * @param s NULL terminated ASCII string to hash
 * @return 8-bit hash result
 */
uint8_t xor8(const char* s)
{
    uint8_t hash = 0;
    size_t i = 0;
    while (s[i] != '\0')
    {
        hash = (hash + s[i]) & 0xff;
        i++;
    }
    return (((hash ^ 0xff) + 1) & 0xff);
}

KLEE file

int klee_entry__hash_hash_xor8_xor8(int utbot_argc, char ** utbot_argv, char ** utbot_envp) {
    char s[10];
    klee_make_symbolic(s, sizeof(s), "s");
    for (int it_1_0 = 0; it_1_0 < 10; it_1_0 ++) {
        if (it_1_0 == 9) {
            s[9] = '\0';
            break;
        }
        klee_prefer_cex(s, s[it_1_0] >= 'a' & s[it_1_0] <= 'z' & s[it_1_0] != '\0');
    }
    //////////////////////////////////////////// 
    unsigned char utbot_result;
    klee_make_symbolic(&utbot_result, sizeof(utbot_result), "utbot_result");
    unsigned char utbot_tmp = xor8(s);
    klee_assume(utbot_tmp == utbot_result);
    return 0;
}

Wrong test that fails

TEST(regression, xor8_test_2)
{
    char s[] = "aaphpabpaa";
    unsigned char actual = xor8(s);
    EXPECT_EQ(98, actual);
}

Test console

Running main() from /utbot_distr/gtest/googletest/src/gtest_main.cc
Note: Google Test filter = *.xor8_test_2
[==========] Running 1 test from 1 test suite.
[----------] Global test environment set-up.
[----------] 1 test from regression
[ RUN      ] regression.xor8_test_2
/home/utbot/projects/C/utbot_tests/hash/hash_xor8_test.cpp:25: Failure
Expected equality of these values:
  98
  actual
    Which is: '\x1' (1)
[  FAILED  ] regression.xor8_test_2 (0 ms)
[----------] 1 test from regression (0 ms total)

[----------] Global test environment tear-down
[==========] 1 test from 1 test suite ran. (0 ms total)
[  PASSED  ] 0 tests.
[  FAILED  ] 1 test, listed below:
[  FAILED  ] regression.xor8_test_2

 1 FAILED TEST

My thoughts

String s in the test has 10 symbols within, although the 10th symbol must be '\0' in accordance with the KLEE file. So, if I remove the last symbol, the test passes. Or if I change s[9] = '\0'; to klee_assume(s[9] == '\0'), then KLEE generates the correct test with 9 symbols. Either way, this case must be fixed, but why does that even happen?