Missing (str.to-int s) in Z3 4.5.1

Question

I'm using Z3 4.5.1 successfully with strings and operations such as sub-string, string-length, string-comparisons etc. like this example:

(declare-const s1 String)
(declare-const s2 String)
(declare-const i Int)
(assert (= s1 "97\x00098\x0099###$$"))
(assert (= s2 (str.substr s1 2 (- (str.len s1) 2))))
(assert (= "\x00058\x0099###$$" (str.replace s2 "9" "5")))
(check-sat)
(get-value (s1 s2 i))

However, when I try to add str.to-int:

(declare-const s1 String)
(declare-const s2 String)
(declare-const i Int)
(assert (= s1 "97\x00098\x0099###$$"))
(assert (= s2 (str.substr s1 2 (- (str.len s1) 2))))
(assert (= "\x00058\x0099###$$" (str.replace s2 "9" "5")))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(assert (= 98 (str.to-int "000098")))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(check-sat)
(get-value (s1 s2 i))

I get this error:

(error "line 8 column 35: unknown function/constant str.to-int")

I'm puzzled because "to-int" appears in the documentation along other string operations that are all working perfectly. I'm using this documentation: Z3str3 Input Language. Any help is very much appreciated, thanks!!

Answer 1

Z3 has been using str.to.int and int.to.str for a while. The SMTLIB2 format for strings hasn't been finalized at this point either.