Какова причина предупреждающего сообщения в Z3: «не удалось найти шаблон для квантификатора (идентификатор квантификатора: k! 18)»

) Я обнаружил проблему, показанную в следующей простой программе SMT-LIB.

Код SMT-LIB:

(declare-fun isDigit (Int) Bool)
(assert (forall ((x Int))
    (=>     (isDigit x)
        (and (>= x 0) (< x 10))
    )
  )
) 

(assert (forall ((x Int))   
    (=>     (and (>= x 12) (< x 15))
        (exists ((y Int))
            (and    (>= y 1) (< y 6)
                (isHost (- x y))
            )
        )
    )
  )
)

(check-sat)
(get-model)

Это дает следующее предупреждение:

WARNING: failed to find a pattern for quantifier (quantifier id: k!18)
sat
........
........

Меня интересует предупреждающее сообщение. Я знаю, что что-то упустил, но не могу понять. Может ли кто-нибудь помочь мне в решении этой проблемы?