CIL is a front-end for the C programming language that facilitates program analysis and transformation. CIL will parse and typecheck a program, and compile it into a simplified subset of C.
[Z3] is a state-of-the-art SMT solver by Microsoft Research. [Z3]: www.rise4fun.com/Z3
[MLton] is a whole-program optimising Standard ML compiler [MLton]: http://mlton.org/
Z3MLton is an extension for CIL that parses Z3 C API and generates MLton Foreign Function Interface (MLFFI) that enables MLton programs to access Z3 C APIs.