cvc5

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 with respect to (combinations of) a variety of useful background theories.It further provides a Syntax-Guided Synthesis (SyGuS) engine to synthesize functions with respect to background theories and their combinations. cvc5 is the successor of CVC4 and is intended to be an open and extensible SMT engine.

homepage: https://cvc5.github.io/

version	toolchain
1.3.2	GCC/14.2.0

(quick links: (all) - 0 - a - b - c - d - e - f - g - h - i - j - k - l - m - n - o - p - q - r - s - t - u - v - w - x - y - z)