(i.e., use 'system' to shell out to an already existing solver, which is at least documented in the readme).
(To be clear, it shells out to an existing SAT solver. If I understand correctly, the 1500 lines of C implement the "modulo theory" part of "satisfiable modulo theory" — that is, they "compile" things like bitvector addition into pure boolean circuits.)