Uses Clang.jl to wrap around Z3's C API, and BinaryBuilder.jl to build the Z3 binary (build script here).
Design follows Z3Py.
In particular, we provide an implicit global Context
, and overload operators (like +
,-
,*
, /
)
to create Z3 expressions.