Эквивалент define-fun в Z3 API

Используя Z3 с текстовым форматом, я можно использовать define-fun для определения функций для повторного использования позже. Например:

(define-fun mydiv ((x Real) (y Real)) Real
  (if (not (= y 0.0))
      (/ x y)
      0.0))

Мне интересно, как создать define-fun с Z3 API (я использую F #) вместо того, чтобы везде повторять тело функции. Я хочу использовать его, чтобы избежать дублирования и упростить отладку формул. Я пробовал использовать Context.MkFuncDecl , но, похоже, он генерирует только неинтерпретируемые функции.