For anyone wondering how you could write a solver in 1500 lines of C, the answer is here: https://github.com/DennisYurichev/ToySMT/blob/master/ToySMT....

(i.e., use 'system' to shell out to an already existing solver, which is at least documented in the readme).