Why is this result sat? I expected it to be unsat

[sengxin]

path = z3.String("path")
allowed_chars = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789/"
allowed_chars_re = z3.Re('[' + allowed_chars + ']+')
# any_allowed_char = z3.Or([z3.Re(f'({c})') for c in allowed_chars])
s1 = z3.InRe(path, z3.Concat(z3.Re('/test/v1/olc/include'), z3.Star(allowed_chars_re)))
s2 = z3.InRe(path, z3.Concat(z3.Re('/test/v1/olc'), z3.Star(allowed_chars_re)))
solver = z3.Solver()
solver.add(s1, z3.Not(s2))
result = solver.check()
print(result)