cvc5 Documentation

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems that supports a large number of theories and their combination. It is the successor of CVC4 and is intended to be an open and extensible SMT engine.

This space provides all documentation related to using cvc5.

Table of Contents