Z3_OP_DT_CONSTRUCTOR is not supported

[jespera]

I have a use-case of ksmt where I would like to use it as a convenient way to use Z3 to check for satisfiability of boolean expressions.

The expression language is a variant of simply typed lambda calculus with non-recursive algebraic datatypes and the expressions to check are guaranteed to not require asserting equality of functions.

I had hoped that the Kotlin DSL for definition expressions with ksmt could be used, but I didn't find anything. Instead, I tried making use of the parsing functionality:

I have following Kotlin snippet of code:

            val formula = """
(declare-datatype Lst
  (par (E)
    ( (nil)
      (cons (car E) (cdr (Lst E))))
    ))
(declare-const l1 (Lst Int))
(assert (= l1 nil))

(check-sat)
(get-model)
            """.trimIndent()
            val parsed = KZ3SMTLibParser(this).parse(formula)

And running the snippet I get an exception throw from the call to parse:

io.ksmt.solver.KSolverUnsupportedFeatureException: Z3_OP_DT_CONSTRUCTOR is not supported
	at io.ksmt.solver.z3.KZ3ExprConverter.convertApp-h_aMM1A(KZ3ExprConverter.kt:420)
	at io.ksmt.solver.z3.KZ3ExprConverter.convertNativeExpr-h_aMM1A(KZ3ExprConverter.kt:164)
	at io.ksmt.solver.util.KExprLongConverterBase.convertFromNative(KExprLongConverterBase.kt:27)
	at io.ksmt.solver.z3.KZ3ExprConverter.convertExpr(KZ3ExprConverter.kt:86)
	at io.ksmt.solver.z3.KZ3SMTLibParser.convertAssertions(KZ3SMTLibParser.kt:45)
	at io.ksmt.solver.z3.KZ3SMTLibParser.parse(KZ3SMTLibParser.kt:37)
	at io.ksmt.solver.z3.KZ3SMTLibParser.parse(KZ3SMTLibParser.kt:25)

I suppose this means (user defined) algebraic datatypes are not really supported in ksmt or is there a way that I'm just not seeing?