At one point I wrote a Common Lisp interface to Z3. The syntax was nice, except that empty lists have to be printed as () rather than NIL. So close to working with no tweaks.

The hardest part is getting the model back at the end (well, and making problems that don't scale too badly with N).