Prototype Python utilisant le solveur Z3 SMT pour encoder et analyser les mesures socio-fiscales françaises. Il permet de répondre à des questions sur le système socio-fiscal sous la forme d'une recherche dichotomique pour maximiser ou minimiser une valeur donnée, en fonction de divers paramètres tels que les revenus, les allocations familiales, les aides au logement, etc.