This is, in my opinion, not a "real" SMT solver. It translates an SMT instance into a SAT instance. This is easy to do for the theories the author is considering (bitvectors), but not at all straightforward for integers or reals.

Most SMT solvers today use the DPLL(T) technique which transfers information back and forth between a so-called theory solver (e.g., a simplex solver that handles real constraints) and a SAT solver which handles the "Boolean part" of the problem . I feel that an SMT solver that intends to be educational must implement DPLL(T).