python - z3 固定小数点ソルバーのリレーションに対するパラメーターとしての配列

Question

z3 固定小数点ソルバーの関係へのパラメーターとして配列を使用しています。クエリを満たす証明書の配列値を取得しようとしています。これを z3 で実行すると、Uninterpreted 'a1' in A(#1,#0,#3)というエラーがスローされます。

配列が解釈されないものとして扱われるのはなぜですか? これは、解釈されていない関数を固定小数点ソルバーの関係への引数として使用できないことを意味しますか?

(declare-rel A (Int Int (Array Int Int)))
(declare-rel q1 (Int Int  (Array Int Int)))
(declare-const a1 (Array Int Int))
(declare-var a Int) 
(declare-var b Int)
(declare-var i Int)

(rule (=> (A (+ a 1) b (store a1 i 2)) (A a b a1)))

(rule (=> (= a b) (A a b a1)))

(rule (=> (and (A a b a1) (= a 0) (= b 1)) (q1 a b  a1)))

(query q1 :print-certificate true)