What is veriT?
veriT is a SMT (Satisfiability Modulo Theories) solver. It is open-source, proof-producing, and complete for quantifier-free formulas with uninterpreted functions and difference logic on real numbers and integers.
The ancestor of veriT is haRVey. Its web page can still be reached here.
The input format is the SMT-LIB language, but veriT can also be used as a standalone library and incorporated in third-party software. The tool is open-source and distributed under the BSD licence.
veriT is complete for the logic of unquantified formulas over uninterpreted symbols, difference logic over integers and real numbers, and the combination thereof. This corresponds to the logics identified as QF_IDL, QF_RDL, QF_UF and QF_UFIDL in the SMT-LIB benchmarks. veriT also includes quantifier reasoning capabilities through the integration of a first-order prover and quantifier instantiation heuristics.
veriT has proof-production capabilities that may be used or checked by external tools. veriT is incremental, i.e. after each satisfiability check, new formulas can be added conjunctively to the already checked set of formulas. Although not (yet) as fast as the solvers performing best in the SMT competition, veriT has a decent efficiency.
