Wrong result when using Lambda functions with the option smt.pull_nested_quantifiers

[Joshua27]

We use Lambda functions with an existential quantifier at the top-level.

(set-option :smt.pull_nested_quantifiers true)
(declare-datatypes ((|couple(integer,integer)| 0)) (((|couple(integer,integer)| (get_x_couple_integer_integer Int) (get_y_couple_integer_integer Int)))))
 (assert
 (let ((?x21 (lambda ((prj2_couple_cst Int) )(exists ((prj1_couple_cst Int) )(let ((?x8 (|couple(integer,integer)| 1 1)))
 (let ((?x10 (store ((as const (Array |couple(integer,integer)| Bool)) false) ?x8 true)))
 (select ?x10 (|couple(integer,integer)| prj1_couple_cst prj2_couple_cst)))))
 )
 ))
 (let ((?x7 (store ((as const (Array Int Bool)) false) 1 true)))
 (let (($x12 (= ?x7 ?x21)))
 (not $x12)))))
(check-sat)
(exit)

Expected result: unsat
Actual result: sat
Z3 returns unsat when setting the option :smt.pull_nested_quantifiers to false.
We tested this on Linux and Mac with Z3 version 4.8.9 and 4.8.10.