CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.
Commercial Use
Modify
Distribute
Place Warranty
Hold Liable
Use Trademarks
Include Copyright
Include License
These details are provided for information only. No information here is legal advice and should not be used as such.
There are no reported vulnerabilities
30 Day SummaryJan 16 2026 — Feb 15 2026
|
12 Month SummaryFeb 15 2025 — Feb 15 2026
|