z3py's LastIndexOf is supposed to return the "last index of substring within a string". However, it seems to return the wrong results when the substring is located at the end of the string, for example:
>>> import z3
>>> def check_lastindexof(s, sub_list):
... for c in sub_list:
... z_index = z3.simplify(z3.LastIndexOf(s, c))
... v_index = s.rindex(c)
... try:
... assert z_index == v_index
... except Exception as e:
... print(f'{c: <6} FAILED expected: {v_index: >2}, got: {z_index}')
...
>>>
>>> s = 'abcdefabcdef'
>>> tests = ['a', 'abc', 'f', 'ef', 'abcdef']
>>> check_lastindexof(s, tests)
f FAILED expected: 11, got: 5
ef FAILED expected: 10, got: 4
abcdef FAILED expected: 6, got: 0
Notably, LastIndexOf returns -1 if the substring exists only once in the string, which is clearly wrong as far as I know:
>>> s = 'abcdef'
>>> check_lastindexof(s, tests)
f FAILED expected: 5, got: -1
ef FAILED expected: 4, got: -1
abcdef FAILED expected: 0, got: -1
Am I misunderstanding how z3.LastIndexOf is supposed to work or is there maybe a bug somewhere?
z3-solver version: 4.8.14.0 (installed via pip)
This looks like a bug indeed. Please report it at https://github.com/Z3Prover/z3/issues