I'm trying to use suffix API function in Z3 in the following script, but Z3 complains it does not know str.suffix. Since I see it in the API here I guess it exists but only called different (?) Thanks!
(declare-const s String)
(declare-const s00 String)
(declare-const s1 String)
(declare-const s2 String)
(declare-const i Int)
(assert (= s "X2a2@@aDD\x00444ppa800"))
(assert (= s00 (str.substr s 0 (str.indexof s "\x00" 0))))
(assert (str.suffixof s1 s00))
(assert (str.suffixof s2 s1))
(assert (= (str.len s1) (+ (str.len s2) 1)))
(assert (or (and (str.contains s00 "a")
(str.contains s1 "a"))
(not (str.contains s00 "a"))))
(assert (not (str.contains s2 "a")))
(assert (= i (ite (not (str.contains s00 "a")) -1
(- (str.len s00) (str.len s1)))))
(check-sat)
(get-value (s s00 s1 s2 i))
EDIT:
The script was fixed according to the answer. Here is the output from z3:
sat
((s "X2a2@@aDD\x00444ppa800")
(s00 "X2a2@@aDD")
(s1 "aDD")
(s2 "DD")
(i 6))
The correct call is: str.suffixof
(PS. Your file still doesn't load even with that fix since it has other issues; but that's besides the point of this question.)