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.