kissat is an SMT solver written by Armin Biere on a plain C. Simple enough for understanding.
SATurne - is a simple, purely functional SAT solver written and verified in Coq. It's a tiny solver, absolutely not designed for performances nor scalability. It is, however, intended to be well-documented, easy to understand and extremely trustworthy.
Modulus - building an SMT solver from the ground up.
https://github.com/zutshi/ToySMT - is a small SMT solver made by Denis Yurichev. It supports only booleans and bitvecs. No integers, let alone reals and arrays and tuples and whatever.
Semantics and application to program verification. The goal of the project is to implement a small static analyzer by abstract interpretation for a simple language. Slides, Project page