(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

(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.)