Квантификаторы и шаблоны (формула QBF)

Я пытаюсь закодировать QBF в синтаксисе smt-lib 2 для z3. Запуск z3 приводит к предупреждению

ПРЕДУПРЕЖДЕНИЕ: не удалось найти шаблон для квантификатора (идентификатор квантификатора: k!14)

, и результат выполнимости "неизвестен".

Код выглядит следующим образом:

(declare-fun R (Bool Bool Bool Bool) Bool)
(assert
  (forall ((x2 Bool) (x3 Bool)) 
    (exists ((y Bool))
      (forall ((x1 Bool))
        (R x1 x2 x3 y)
      )
    )
  )
)
(check-sat)

Я избавился от предупреждения, переписав код на

(set-option :auto-config false)
(set-option :mbqi false)
(declare-fun R (Bool Bool Bool Bool) Bool)
(declare-fun x1 () Bool)
(declare-fun x2 () Bool)
(declare-fun x3 () Bool)
(declare-fun y () Bool)
(assert
  (forall ((x2 Bool) (x3 Bool)) 
  (!
    (exists ((y Bool))
    (!
      (forall ((x1 Bool))
      (!
        (R x1 x2 x3 y)
      :pattern((R x1 x2 x3 y)))
      )
    :pattern((R x1 x2 x3 y)))
    )
  :pattern((R x1 x2 x3 y)))
  )
)
(check-sat)

Результат для sat-запроса, однако, остается "неизвестным".

Я предполагаю, что мне нужно получить правильные шаблоны? Как мне указать их для вложенных квантификаторов? Простые примеры с квантификаторами, кажется, работают без аннотации шаблона.

Ответ на В чем причина предупреждающего сообщения в Z3: «не удалось найти шаблон для квантификатора : k!18) "и руководство по z3, к сожалению, не очень мне помогло.