pqffd incorrect answer on formula with declare-datatypes

[muchang]

Hi,
For this formula,

(declare-datatypes ((a 0)) (((b) (c (d a)))))
(declare-fun e () a)
(declare-fun f () a)
(assert (= f e))
(assert (not ((_ is (c (a) a)) f)))
(assert (or ((_ is (c (a) a)) e)))
(check-sat-using pqffd)
(get-model)

z3 incorrectly gives sat and an incorrect model:

  (define-fun f () a
    b)
  (define-fun e () a
    b)

If I feed this model to the formula, z3 reports unsat.

OS: Ubuntu 18.04
Revision: 805ac74

[NikolajBjorner]

don't use qffd on indefinite sorts.