Factor out SMT file writing/solver calls (1/N)

Refactor methods in smt.ml to build formulas internally, and then
calling a common file export interface, instead of directly writing
SMT files.