An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Try cvc5 online!

View on GitHub
Join the Conversation
Third Party Applications

GitHub LinkedIn Twitter Facebook

License: BSD


Updates are posted every other month, sometimes more frequently.

A Theory of Sequences in cvc5

by Yoni Zohar, 15 Feb 2024

Introduction The theory of sequences in cvc5 is relatively new. In essence, it is meant to model data structures such as List in Java, or std::vector in c++. Unlike the theory of arrays (which is actually a theory of maps), the theory of sequences is very rich, and allows, in addition to array-like read and write operations, to also use operators such as concatenation, sub-list, length, and more. Read More

Adding a New Theory to cvc5

by Alex Ozdemir, 26 Jan 2024

cvc5 is an SMT solver with support for many theories: integers, reals, bit-vectors, algebraic datatypes, separation logic, sets, bags, and more. This means that is can find satisfying solutions for formulas involving these kinds of objects. In this post, I explain the process of adding a new theory to cvc5: the theory of prime-order finite fields. Read More

Partitioning Strategies for Distributed SMT Solving

by Amalee Wilson, 15 Dec 2023

Partitioning is a divide-and-conquer approach where a difficult problem is split into hopefully easier subproblems that can be solved in parallel. This strategy is notoriously difficult to get right with SMT problems. We found that while it’s no panacea, partitioning can be used to diversify solving and reliably improve performance in a portfolio. Read More