PV6 ⊧ veriTproduces a proof for satisfiability of a formula

SMT solver

Application domain/field

• Satisfiability Modulo Theories (SMT)
• Proof-producing
• SMT solving

Type of tool

SMT solver

Expected input

SMT problem

Format:

SMT-LIB 2.0 or DIMACS

Expected output

unsat, sat or an error (in case of e.g. a timeout) veriT can also produces a proof that can be checked with an external tool if the input problem deduced to be unsatisfiable. This proof is presented in veriT's own format.

Internals

veriT is complete for quantifier-free formulas with uninterpreted functions and linear arithmetic on real numbers and integers. It also offers good support for quantifiers. veriT can produce a proof that can be checked with external tools.

Comments

License: BSD License