Как можно использовать конструкцию match в smtlib2 через C API в z3?

Question

В стандартной версии SMT-LIB 2.6 была введена конструкция match, которую можно использовать следующим образом:

; Axiom for list append : version 1
; List is a parametric datatype
; with constructors " nil " and " cons "
;
(forall ((l1 (List Int)) (l2 (List Int)))
  (= (append l1 l2)
    (match l1 (
      (nil l2)
      ((cons h t) (cons h (append t l2)))))))

Как правильно написать этоиспользуя C API вместо этого?Или это просто переведено в серию ite и let привязок?