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.<p>[1]: <a href="https://yurichev.com/writings/SAT_SMT_draft-EN.pdf" rel="nofollow">https://yurichev.com/writings/SAT_SMT_draft-EN.pdf</a>
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.<p>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).