Equal lists are permutations of one another. Why d

I am trying to verify a sorting algorithm and decided to model lists from the programming language as tuples of (size as Int, contents as Array Int -> Obj) and called them MyList.

Then I came accross the following problem:

l0 and l1 are such MyLists.

When asked (assert (not (permutation l0 l0))), Z3 answers unsat quickly.

When asked (assert (not (permutation l1 l1))), Z3 answers unsat quickly.

But when I ask for

(assert (= l1 l0))
(assert (not (permutation l1 l0)))

It answers unknown after a few seconds. How can that be? Is this query that much more difficult? AFAIK Arrays are extensional in Z3, so equating the two lists should make it boil down to the reflexive case, shoudn't it?

Here is the full code (SMT-LIB2):

(set-option :produce-unsat-cores true)
(set-option :produce-models true)

; --------------- Basic Definitions -------------------

(declare-sort Obj 0)

; --------------- Predicates -------------------------------

(declare-datatypes () ((MyList (mk-pair (size Int) (contents (Array Int Obj))))))

(define-fun size_list ((l MyList) (size Int)) Bool
                      (and
                        (<= 0 size)
                        (= (size l) size)
                      )
)

(define-fun select_list ((l MyList) (index Int) (result Obj)) Bool
                        (and
                          (exists ((sl Int))
                            (and
                              (size_list l sl)
                              (>= index 0)
                              (< index sl)
                            )
                          )
                          (= (select (contents l) index) result)
                        )
)

(define-fun in_list ((o Obj) (l MyList)) Bool
                    (exists ((i Int)) (select_list l i o)))


(define-fun permutation ((l1 MyList) (l2 MyList)) Bool
                        (forall ((o Obj)) (= (in_list o l1) (in_list o l2))))

(declare-const l0 MyList)
(declare-const l1 MyList)

;(assert (not (permutation l0 l0)))  ; unsat
;(assert (not (permutation l1 l1)))  ; unsat

(assert (= l1 l0))
(assert (not (permutation l1 l0)))   ; unknown

; --------------- Verify -------------------
(check-sat)

Also: How do you proceed when the solver answers unknown? Models and Unsat-cores are not available in this case...

Thanks in advance.

Yes, this is a limitation of how quantifiers get handled during pre-processing and Z3 is unable to retrieve the simple congruence.

Maybe you could benefit from the new support for sequences. Then this problem, and probably related ones, become much easier:

(set-option :produce-unsat-cores true)
(set-option :produce-models true)

; --------------- Basic Definitions -------------------

(declare-sort Obj 0)

; --------------- Predicates -------------------------------

(define-sort MyList () (Seq Obj))

(define-fun in_list ((o Obj) (l MyList)) Bool (seq.contains l (seq.unit o)))


(define-fun permutation ((l1 MyList) (l2 MyList)) Bool
                    (forall ((o Obj)) (= (in_list o l1) (in_list o l2))))

(declare-const l0 MyList)
(declare-const l1 MyList)

;(assert (not (permutation l0 l0)))  ; unsat
;(assert (not (permutation l1 l1)))  ; unsat

(assert (= l1 l0))
(assert (not (permutation l1 l0)))   ; unknown

; --------------- Verify -------------------
(check-sat)

See http://rise4fun.com/z3/tutorial/sequences for more details.