For example take a look at the Python API for Z3. Because of operator overloading it is just beautiful. Much better then raw SMT2.

https://ericpony.github.io/z3py-tutorial/guide-examples.htm