How could an SMT solver be implemented as simple as possible?

Question

I'm trying to figure out how an SMT solver works as simple as possible. Let's assume we have a simple input program with symbolic values x and y. E.g.

if (x+y < 20) {
   if (x > 10) {
      if (y > 10) {
        assume(false);
      }
   }
}

Here we have different paths, depending on the conditions. To reach assume(false) each condition has to be true, so our outcoming formula is:

$x+y < 20 \,\,\,\,\,\wedge \,\,\,\,\, x > 10 \,\,\,\,\, \wedge \,\,\,\,\, y > 10$

So far, so good. What happens next, step by step?

I would like to implement, as simple as possible, a solver which gets as input something like the formula above and delivers specific output to reach the end of the path - here assume(false), i.e. x = 2147483647, y = 2147483647 (jfi: x+y would be -2) - for overflow detection or similar.

I know there are a lot of SMT solvers on the internet, but I couldn't find a really simple self-explaining one. Looking forward to a suggestion.