"invalid datatype declaration, unknown sort" when using testers

[coord-e]

The following input causes Hoice to error with "invalid datatype declaration, unknown sort 'D1'". I expect Hoice to return sat without raising an error for this input.

(set-logic HORN)

(declare-datatypes ((D1 0)) (
  (par () (
    (C1)
  ))
))

(declare-datatypes ((D0 0)) (
  (par () (
    (C2 (getD D1))
  ))
))

(assert (forall ((x D1)) (=> true ((_ is C1) x))))

(check-sat)

$ hoice hoice_bug.smt2
(error "
  solver error: "line 2 column 19: invalid datatype declaration, unknown sort 'D1'"
  while running preprocessor simplify
")

This error does not occur if the second datatype D0 does not refer D1 in its declaration, or does not exist at all:

(set-logic HORN)

(declare-datatypes ((D1 0)) (
  (par () (
    (C1)
  ))
))

(assert (forall ((x D1)) (=> true ((_ is C1) x))))

(check-sat)

$ hoice hoice_bug_ok1.smt2
sat

This error does not occur if an operand of the tester is a constant:

(set-logic HORN)

(declare-datatypes ((D1 0)) (
  (par () (
    (C1)
  ))
))

(declare-datatypes ((D0 0)) (
  (par () (
    (C2 (getD D1))
  ))
))

(assert (forall () (=> true ((_ is C1) C1))))

(check-sat)

$ hoice hoice_bug_ok2.smt2
sat

This error does not occur if the referring datatype name is lexicographically larger than the referred one:

(set-logic HORN)

(declare-datatypes ((D1 0)) (
  (par () (
    (C1)
  ))
))

(declare-datatypes ((D2 0)) (
  (par () (
    (C2 (getD D1))
  ))
))

(assert (forall ((x D1)) (=> true ((_ is C1) x))))

(check-sat)

$ hoice hoice_bug_ok3.smt2
sat

Environment

$ z3 --version
Z3 version 4.12.2 - 64 bit

$ hoice --version
hoice 1.10.0