Does z3 take and produce s-expressions?

[egel-lang]

Hya all. Simple question: Does z3 take and produce s-expressions (as defined per SMT-LIB)?

My reason for asking is that because of reasons^tm I want to interface with z3 but not through C bindings. So, I got into a path where I want to produce z3 scripts and read the output of the solver, the additional advantage that it should then also be possible to interface with other provers.

Of course, writing an s-expression library for input and output would then greatly simplify this task. Hence the question.