The author of this (Dennis Yurichev) has also written a 200 page "Quick introduction into SAT/SMT solvers and symbolic execution" that is full of examples of how SAT/SMT solvers can be used.
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).
I've only seriously examined the source of Z3, but encoding an SMT problem to multiple SAT instances remains a feature there - just convert any qf_bv problem into bit width * SAT instances / 2!
I recall that many popular simplifications required a problem to be expressible as CNF.
(I also seem to recall there is some strategy to simplify logics over Reals/Ints into BV without encoding logical "bignum circuitry" as well?)
> but encoding an SMT problem to multiple SAT instances remains a feature there
Sure. I'm not arguing that bitblasting should never be done, it's probably still the best way of solving bitvector problems. My point is that the pedagogical objective of an toy SMT solver is lost if doesn't teach DPLL(T) and only focuses on bitblasting.
(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.)
[1]: https://yurichev.com/writings/SAT_SMT_draft-EN.pdf