Comment un solveur SMT pourrait-il être implémenté le plus simple possible?

Question

J'essaie de comprendre comment un solveur SMT fonctionne aussi simple que possible. Supposons que nous ayons un programme d'entrée simple avec des valeurs symboliques x et y. Par exemple

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

Ici, nous avons différents chemins, selon les conditions. Atteindre assume(false) Chaque condition doit être vraie, donc notre formule à venir est:

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

Jusqu'ici tout va bien. Que se passe-t-il ensuite, étape par étape?

Je voudrais implémenter, aussi simple que possible, un solveur qui obtient une entrée quelque chose comme la formule ci-dessus et fournit une sortie spécifique pour atteindre la fin du chemin - ici assume(false), c'est à dire x = 2147483647, y = 2147483647 (JFI: x+y serait -2) - pour la détection de débordement ou similaire.

Je sais qu'il y a beaucoup de résolveurs SMT sur Internet, mais je n'ai pas pu trouver un seul auto-exploitant. Dans l'attente d'une suggestion.