Z3: Extract array interpretation

Question

How is it possible to extract the function interpretation of an array in Z3 using the C API? When I query Rise4Fun with, say, the following instance:

(declare-fun arr () (Array Int Int))
(assert (= 5 (select arr 3)))
(check-sat)
(get-model)
(exit)

, I get:

sat 
(model 
    (define-fun arr () (Array Int Int) (_ as-array k!0))
    (define-fun k!0 ((x!1 Int)) Int (ite (= x!1 3) 5 5))
)

Is it possible to extract the function interpretation of k!0 using the C API only? I've tried applying Z3_model_get_func_interp on the array constant declaration, and also on the term that is returned for the array in the SAT model, but always get an Error: invalid argument.

Answer 1

Yes, this is possible. A very similar question has been asked recently and the answer with examples can be found here: Read func interp of a z3 array from the z3 model