Program
Verification
Book

PV4 ⊧ CVC4produces a satisfiability result for a formula

Application domain/field

SMT solving

Type of tool

SMT solver

Expected input

SMT formula

Format:

One of the following:

CVC4 native input language
SMT-LIB (v2)
SyGuS-IF
TPTP

Expected output

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

Comments

CVC4 is now succeeded by cvc5.

Links

Repository: https://github.com/CVC4/CVC4-archived
- Last commit date: 05 May 2021 (default branch)
- Last commit date: 06 May 2021 (last activity)
Project page: https://cvc4.github.io/

Related papers

Last publication date

12 July 2019

Related tools

Predecessors: CVC, CVC Lite, CVC3.
Successor: cvc5

ProVerB specific

Markdown description: view/edit

ProVerB is a part of SLEBoK. Last updated: February 2023.