arrays - Z3 の奇妙な配列動作

Question

Z3 で配列を操作しようとすると、説明できない奇妙な動作に気付きました。最初に、 を操作するいくつかの関数を定義しました(Array Int Object)。後で(Array Int Real)、他の関数と混同してはならない型の Array を定義します。これらの関数は型が異なるためです。次に、配列に数値を追加し始めます。最初はすべて問題ありませんが、配列に 3 番目の要素を追加すると、仕様が壊れてしまいます。さらに、すべてを操作する関数の公理を削除すると、(Array Int Object)再び機能します。なぜこれが起こるのか、私にはわかりませんが、誰かがそれについて考えていることを願っています.

; Declaration of concepts
(declare-datatypes () ((Object ObjectA ObjectB ObjectC)))

; Be aware that the following functions work on (Array Int Object) and we define an array of type (Array Int Real) later
(declare-fun Length ( (Array Int Object) ) Int)   ; The concrete length will be assert for each array of the type (Array Int Object)
(define-fun SameArray ( (array1 (Array Int Object)) (array2 (Array Int Object))) Bool
  (ite 
    (and
      (= (Length array1) (Length array2))
      (forall ((i Int)) (or (< i 0) (>= i (Length array1)) (= (select array1 i) (select array2 i) )) ) 
    )
    true
    false
  )
)

(declare-fun Match ((Array Int Object) (Array Int (Array Int Object))) Int) ; The concrete behavior for Match will be asserted for each necessary array.

; If the following axiom is deleted everything works fine
; Axioms: Equal arrays should behave equal for the Match function.
(assert (forall ( (array1 (Array Int Object)) (array2 (Array Int Object)) (list (Array Int (Array Int Object))))
  (ite
    (SameArray array1 array2)
    (= (Match array1 list) (Match array2 list))
    (not (= (Match array1 list) (Match array2 list)))
  )
))

(echo "General Definitions:")
(check-sat) ; Everything is OK here

(declare-const arr-Lookup-1 (Array Int Real))
(echo "Array Declaration:")
(check-sat) ; Everything is OK here

(assert (= (store arr-Lookup-1 0 0.0) arr-Lookup-1))
(echo "Array1 Definition 1:")
(check-sat) ; Everything is OK here

(assert (= (store arr-Lookup-1 1 100.0) arr-Lookup-1))
(echo "Array1 Definition 2:")
(check-sat) ; Everything is OK here

(assert (= (store arr-Lookup-1 2 1000.0) arr-Lookup-1))
(echo "Array1 Definition 3:")
(check-sat) ; This gives us an unknown 

(assert (= (store arr-Lookup-1 3 10000.0) arr-Lookup-1))
(echo "Array1 Definition 4:")
(check-sat)