Z3 reports sat for unsatisfiable constraint using a lambda expression

[Joshua27]

Dear Z3 team,
I have potentially found a bug which results in Z3 reporting SAT although the constraint is unsatisfiable.
The constraint in pseudocode is not(#t2.(!(t8).((t8,1) : t2 => 1 >= t8 ) & ran(t2) = {1})), where : is a set membership, # is an existential quantifier, ! is a universal quantifier, and ran is the range of a relation (i.e., a set of pairs such as (1,2)).
Our tool encodes this constraint in SMT-LIB as follows:

(declare-datatypes ((|couple(integer,integer)| 0)) (((|couple(integer,integer)| (get_x_couple_integer_integer Int) (get_y_couple_integer_integer Int)))))
 (assert
 (let (($x18 (exists ((t2 (Array |couple(integer,integer)| Bool)) )(let ((?x19 ((as const (Array Int Bool)) false)))
 (let ((?x22 (store ?x19 1 true)))
 (let ((?x28 (lambda ((_prj2 Int) )(exists ((_prj1 Int) )(let ((?x21 (|couple(integer,integer)| _prj1 _prj2)))
 (select t2 ?x21)))
 )
 ))
 (let (($x32 (= ?x28 ?x22)))
 (let (($x36 (forall ((t8 Int) )(let (($x13 (>= 1 t8)))
 (let ((?x14 (|couple(integer,integer)| t8 1)))
 (let (($x34 (select t2 ?x14)))
 (=> $x34 $x13)))))
 ))
 (and $x36 $x32)))))))
 ))
 (not $x18)))
(check-sat)

Expected result: UNSAT
Actual result: SAT
It should be noted that the lambda expression is the encoding of the relational range operator. The rest of the translation to SMT-LIB is straightforward.

I suspect that the problem is the negation of an existential quantifier that uses a universal quantifier and, in particular, a lambda expression at the top-level.

Z3 mistakenly reports satisfiability for version 4.8.10, 4.8.11, and 4.8.12 as well as up to the latest commit on the master branch using the unreleased version 4.8.13.

This is the smallest constraint that I could find which leads to the wrong result.
I have thoroughly checked the SMT-LIB code and in my opinion it should indeed be unsatisfiable.
I hope that you can reconstruct the fact that the SMT-LIB constraint should be unsatisfiable.
Please let me know if this is not the case.

[NikolajBjorner]

It is fixed, but return unknown because the existing main solver in z3 doesn't know how to handle exists under lambda.