Skip to content


Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?


Failed to load latest commit information.
Latest commit message
Commit time
March 22, 2023 15:19
September 6, 2019 20:52
April 20, 2016 14:43

License: BSD CI Coverage


cvc5 is a tool for determining the satisfiability of a first order formula modulo a first order theory (or a combination of such theories). It is the fifth in the Cooperating Validity Checker family of tools (CVC, CVC Lite, CVC3, CVC4) but does not directly incorporate code from any previous version prior to CVC4.

If you are using cvc5 in your work, or incorporating it into software of your own, we invite you to send us a description and link to your project/software, so that we can link it on our Third Party Applications page.

cvc5 is intended to be an open and extensible SMT engine. It can be used as a stand-alone tool or as a library. It has been designed to increase the performance and reduce the memory overhead of its predecessors. It is written entirely in C++ and is released under an open-source software license (see file COPYING).


cvc5's website is available at:


Documentation for users of cvc5 is available at:

Documentation for developers is available at:


The latest version of cvc5 is available on GitHub:

Source tar balls and binaries for releases of the main branch can be found here. Nightly builds are available here.

Build and Dependencies

cvc5 can be built on Linux and macOS. For Windows, cvc5 can be cross-compiled using Mingw-w64.

For detailed build and installation instructions on these platforms, see file INSTALL.rst.

Bug Reports

If you need to report a bug with cvc5, or make a feature request, please visit our bugtracker at our GitHub issues page. We are very grateful for bug reports, as they help us improve cvc5.


Please refer to our contributing guidelines.


For a full list of authors, please refer to the AUTHORS file.