PV4 ⊧ Cooperating Validity Checker (CVC3)produces a validity/satisfiability result for a formula

Application domain/field

SMT solving

Type of tool

SMT solver

Expected input

SMT formula

Expected output

sat or unsat which indicates whether the SMT formula was satisfiable or not.

Comments

CVC3 is succeeded by CVC4 and cvc5.