PV4 cvc5produces a satisfiability result for a formula

Application domain/field

SMT solving

Type of tool

SMT solver

Expected input

SMT formula

Format:

SMT-LIB

Expected output

sat or unsat

Internals

cvc5 can be used as a stand-alone tool or as a library. There is an API available for C++, Java and Python.
SMT

Links

Related papers

Last publication date

2022

Related tools

From the same 'family' of tools: CVC, CVC Lite, CVC3, CVC4

ProVerB specific

Markdown description: view/edit



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