Значения терминов массива в моделях z3

Я использую z3 для своих исследований, и у меня есть следующая проблема. Я анализирую модель выполнимой формулы, которая содержит массивы и неинтерпретируемые функции. Я хотел бы проверить определенные записи массива.

В примерах руководства по z3 можно получить доступ к таким значениям.
Например, для таких вопросов, как

(get-value ((select my_array 0)))

человек получает ответы, как

(((select my_array 0) 1)) 

указывая, что значение my_array в позиции 0 равно 1.

Однако ответ, который я получаю, выглядит так

(((select my_array 0) (select Array!val!0 0)))

что совсем не полезно.

Также в начале модели я получаю блок, который выглядит так:

  ;; universe for (Array Int Int):
  ;;   Array!val!10 Array!val!6 Array!val!0 Array!val!5 Array!val!9 Array!val!1 Array!val!11 Array!val!4 Array!val!2 Array!val!7 Array!val!3 Array!val!8 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun Array!val!10 () (Array Int Int))
  (declare-fun Array!val!6 () (Array Int Int))
  (declare-fun Array!val!0 () (Array Int Int))
  (declare-fun Array!val!5 () (Array Int Int))
  (declare-fun Array!val!9 () (Array Int Int))
  (declare-fun Array!val!1 () (Array Int Int))
  (declare-fun Array!val!11 () (Array Int Int))
  (declare-fun Array!val!4 () (Array Int Int))
  (declare-fun Array!val!2 () (Array Int Int))
  (declare-fun Array!val!7 () (Array Int Int))
  (declare-fun Array!val!3 () (Array Int Int))
  (declare-fun Array!val!8 () (Array Int Int))
  ;; cardinality constraint:
  (forall ((x (Array Int Int)))
          (and (= x Array!val!10)
               (= x Array!val!6)
               (= x Array!val!0)
               (= x Array!val!5)
               (= x Array!val!9)
               (= x Array!val!1)
               (= x Array!val!11)
               (= x Array!val!4)
               (= x Array!val!2)
               (= x Array!val!7)
               (= x Array!val!3)
               (= x Array!val!8)))
  ;; -----------

Я не совсем понимаю, что это значит, но каким-то образом это связано с моей проблемой, так как подобный блок не появляется для простых примеров в руководстве. Кто-нибудь знает, что вызывает такое поведение z3 или как его можно избежать?

После некоторых экспериментов я нашел «минимальный» пример, демонстрирующий нежелательное поведение. Кажется, это как-то связано с использованием неинтерпретируемых функций в индексных выражениях.

(declare-fun my_function ((Int)(Int)) Int)
(declare-fun my_array () (Array Int Int))

(assert
  (=
    (select my_array (my_function 0 1))
    (select my_array (my_function 1 0))
  )
)

(check-sat)  
(get-model)
(get-value ((select my_array (my_function 0 1))))
(get-value ((my_function 0 1)))

Ответ z3 на это:

sat 
(model
 ;; universe for (Array Int Int):
 ;; Array!val!0
 ;; -----------
 ;; definitions for universe elements:
 (declare-fun Array!val!0 () (Array Int Int))
 ;; cardinality constraint:
 (forall ((x (Array Int Int))) (= x Array!val!0))
 ;; -----------
 (define-fun my_array () (Array Int Int)
 Array!val!0)
 (define-fun my_function ((x!1 Int) (x!2 Int)) Int
 (ite (and (= x!1 0) (= x!2 1)) 2
 (ite (and (= x!1 1) (= x!2 0)) 3
 2)))
 )
 (((select my_array (my_function 0 1)) (select Array!val!0 2)))
 (((my_function 0 1) 2))