veriT: an open, trustable and efficient SMT-solver
Résumé
This article describes the first public version of the satisfiability modulo theory (SMT) solver {\verit}. It is open-source, proof-producing, and complete for quantifier-free formulas with uninterpreted functions and difference logic on real numbers and integers.