unsat core insufficient

[MichaelRawson]

Z3 occasionally produces an unsat core that isn't enough to produce unsat. I have the following example, minimised as far as I could from a generated problem:

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

(declare-const k!1 Bool)
(declare-const k!2 Bool)
(declare-const k!4 Bool)
(declare-const k!5 Bool)
(declare-const k!10 Bool)
(declare-const k!11 Bool)
(declare-const k!21 Bool)
(declare-const k!22 Bool)

(assert (and ((_ pbeq 1 1 1) k!4 k!5) ((_ pbeq 1 1 1) k!1 k!2)))
(assert (forall ((a Real) (b Real))
  (=>
    (and (> a 0.0) (> b a))
    (and (=> k!10 (=> k!4 (=> k!11 (>= a b))))
         (=> k!21 (=> (and k!1 k!5) (=> k!22 (>= 0.0 b))))))
  ))

(assert k!1)
(assert k!11)
(assert k!22)

If you append

(check-sat-assuming (k!10 k!21))
(get-unsat-core)

it's unsat with core (k!10), but if you instead append

(check-sat-assuming (k!10))

it's sat. Note that the actual result Z3 produces is fine, just the unsat core is too small. @CEisenhofer was able to reproduce, and of course I'm happy to help too.