I know that both bv2int and int2bv are handled as uninterpreted functions in Z3. Still, I am looking for a best practice in solving the following problem: given a "small" (< 10 bits) bitvector index, how to efficiently cast it to Int, and use in queries like this one:
(declare-const s String)
(declare-const someInt Int)
(declare-const someBitVec10 (_ BitVec 10))
(assert (= s "74g\x00!!#2#$$"))
;(assert (str.in.re (str.at s someBitVec10) (re.range "a" "z")))
( assert (str.in.re (str.at s someInt ) (re.range "1" "3")))
(check-sat)
(get-value (s someInt))
Output:
sat
((s "74g\x00!!#2#$$")
(someInt 7))
Thanks!
