Les solveurs SMT comme Z3 nous permettent de résoudre rapidement divers problèmes complexes. Pour utiliser un solveur SMT, une étape importante consiste à générer le code exprimant votre problème au format SMT-LIB.
Le but de ce projet est d'automatiser la génération du code SMT-LIB pour le problème de synthèse d'invariants de programme.