En informatique et en logique mathématique, un problème de satisfiabilité modulo des théories ( SMT ) est un problème de décision pour des formules de logique du premier ordre avec égalité (sans quantificateurs), combinées à des théories dans lesquelles sont exprimées certains symbole...