(I moved this from my old blog.) I was working on integrating two SMT solvers with Wenxin Feng, therefore it is necessary to understand the SMT-LIB »