cvc5 is an efficient open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It can be used to prove the satisfiability (or, dually, the validity) of first-order formulas in a large number of theories and their combination. It further provides a Syntax-Guided Synthesis (SyGuS) engine to synthesize functions with respect to background theories and their combination.
cvc5 is the successor of CVC4 and is intended to be an open and extensible SMT engine. It can be used as a stand-alone tool or as a library, with essentially no limit on its use for research or commercial purposes (see license). To contribute to cvc5, please refer to our contribution guidelines.
cvc5 is a joint project led by Stanford University and the University of Iowa.
The development team of cvc5 is committed to ensure that its core usage model (without experimental options) is extremely robust. At the same time, our team is small and we have to set priorities, including prioritizing user bugs over fuzzer bugs.
For fuzzing bugs, we ask you to follow this guidelines.
For bug reports, please use the cvc5 issue tracker.
If you have a question, a feature request, or if you would like to contribute in some way, please contact one of the project leaders. The CVC-USERS list is for users of cvc5. We will make periodic announcements to this list and users are also encouraged to use it for discussion.