тип данных содержит набор в Z3

) как я могу создать тип данных, содержащий набор других объектов. В основном, я делаю следующий код :

(define-sort Set(T) (Array Int T))
(declare-datatypes () ((A f1 (cons (value Int) (b (Set B))))
  (B f2 (cons (id Int) (a  (Set A))))
 ))

Но Z3 сообщает мне неизвестную сортировку для A и B. Если я удалю "Set", он будет работать так, как указано в руководстве. Вместо этого я пытался использовать List, но это не сработало. Кто-нибудь знает, как заставить его работать?