Wrong solution for subset and Bool Set

[leuschel]

I would have expected that the following constraint is unsat (there is no strict superset of Bool).
However, I do get a solution

; when replacing Bool by Int the formula becomes unsat (cns3)
; z3 says (wrongly?!) that this constraint below is sat; i.e., there exists a strict superset of Bool
; tested with 4.13.3 and 4.13.4
(set-info :status unknown)
(declare-fun id5 () (Set Bool))
(declare-fun id4 () (Set Bool))
(assert (= id4 ((as const (Set Bool)) true )))
(assert (subset id4 id5))
(assert (not (= id4 id5)))
(check-sat)
(get-model)

I do get this result:

$ z3 subset_ticket-cns5.smt2 
sat
(
  (define-fun id5 () (Set Bool)
    (lambda ((x!1 Bool)) x!1))
  (define-fun id4 () (Set Bool)
    ((as const (Set Bool)) true))
)

Am I using subset/Set incorrectly or is this a bug?
I get the same result when using Arrays rather than Sets:

(set-info :status unknown)
(declare-fun id5 () (Array (Array Bool Bool) Bool))
(assert
 (let ((?x7 (lambda ((id4 (Array Bool Bool)) )true)
))
(let (($x10 (subset ?x7 id5)))
(let (($x8 (= ?x7 id5)))
(let (($x9 (not $x8)))
(and $x9 $x10))))))
(check-sat)
(get-model)

[leuschel]

Here is a related SMTLib file where the result is also unexpected to my eyes:

; Context 0x600003690468 Translation type: 1
; 
(set-info :status unknown)
(declare-datatypes ((|couple(integer,integer)| 0)) (((|couple(integer,integer)| (get_x_couple_integer_integer Int) (get_y_couple_integer_integer Int)))))
(declare-fun id0 () (Array |couple(integer,integer)| Bool))
(assert
 (let ((?x16 ((as const (Array |couple(integer,integer)| Bool)) false)))
(let ((?x10 (lambda ((_couple_cst |couple(integer,integer)|) )(exists ((_pred_ Int) )(and true (= _couple_cst (|couple(integer,integer)| _pred_ (- _pred_ 1)))))
)
))
(let ((?x9 ((as union (Array |couple(integer,integer)| Bool)) ?x10 id0)))
(= ?x9 ?x16)))))
(check-sat)
(get-model)

I would have expected unsat (the union of an infinite set with another one cannot yield the empty set?):

$ z3 union_ticket_cns.smt2 
sat
(
  (define-fun id0 () (Array |couple(integer,integer)| Bool)
    ((as const (Array |couple(integer,integer)| Bool)) false))
)