Incorrect results yet no errors reported (with Datatypes and contexts)

[Swire42]

The following input:

(push)
(declare-datatype Pair ((mkPair (fst Bool) (snd Bool))))
(assert (= (fst (mkPair true false)) (fst (mkPair false false))))
(check-sat)
(pop)
(push)
(declare-datatype Pair ((mkPair (snd Bool) (fst Bool))))
(assert (= (fst (mkPair true false)) (fst (mkPair false false))))
(check-sat)
(pop)

Produces:

unsat
unsat

Instead of the expected:

unsat
sat

Note that without the push/pop, an error is reported:

(error "line 4 column 24: sort already defined Pair")

But with push/pop, no errors are reported and the result is incorrect.

z3 version: v4.13.0