Incorrect model when quantifying over polymorphic type

[dewert99]

Running the following smt2 file

(declare-type-var T)
(declare-fun f (T) Bool)
(declare-var b Bool)
(assert (forall ((x T)) (f x)))
(assert (= b (f 0)))
(check-sat)
(get-model)
(assert (not b))
(check-sat)

produces the output:

sat
(
  ;; universe for T:
  ;;   T!val!0 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun T!val!0 () T)
  ;; cardinality constraint:
  (forall ((x T)) (= x T!val!0))
  ;; -----------
  (define-fun b () Bool
    false)
  (define-fun f ((x!0 T)) Bool
    true)
  (define-fun f ((x!0 Int)) Bool
    false)
)
unsat

In particular the model produced for b is false even though after the first check-sat, b must be true. Interestingly after asserting (not b) (which agrees with the previous model) z3 correctly reports unsat.

z3 also gives the expected model when the quatifier is (forall ((x Int)) (f x)) instead of (forall ((x T)) (f x))

This is with Z3 version 4.12.5 - 64 bit