How could an SMT solver be implemented as simple as possible?
What happens next is that we invoke a SMT solver to try to check whether the formula

$$x+y &lt; 20 \quad \land \quad  x &gt; 10 \quad \land \quad y &gt; 10$$

is satisfiable.  The solver tries to find values for $x,y$ that make this formula true.  If it finds such a value, then it knows the assume(false) statement is reachable. (I am guessing you meant to write assert(false), not assume(false).)  If the formula is not satisfiable, then that statement is not reachable.

So basically you are asking: how do SMT solvers work?  That is too broad for this site, but there are lots of places that explain how SAT solvers and SMT solvers work.  I would suggest doing some research; you will find many explanations.  You could start with the DPLL algorithm for SAT.

There is little point in implementing your own solver.  Your solver will probably perform far worse than existing tools.  There has been a lot of research into building effective solvers, and the techniques required are non-trivial.  Instead, I'd recommend you simply use an existing solver, such as Z3.

If you just want to implement one for fun, the most straightforward approach is probably to bit-blast to SAT: treat each bit of (the binary representation of) $x,y$ as a boolean variable, then write down a boolean formula (on those boolean variables) that expresses the requirement that $x+y&lt;20$.  How can you do that?  Write a boolean circuit that computes $x+y$ and compares the sum to 20, then convert that circuit from CircuitSAT to SAT.  Finally, invoke an off-the-shelf SAT solver to check satisfiability of this boolean formula.  You'll need to do some research to understand each of these steps, but there's a lot written on how to do that.