cvc4 - Automatic theorem prover for SMT problems

Property Value
Distribution Fedora 25
Repository Fedora x86_64
Package name cvc4
Package version 1.4
Package release 11.fc25
Package architecture x86_64
Package type rpm
Installed size 861.99 KB
Download size 279.08 KB
Official Mirror
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.
CVC4 is the fourth in the Cooperating Validity Checker family of tools
(CVC, CVC Lite, CVC3) but does not directly incorporate code from any
previous version.  A joint project of NYU and U Iowa, CVC4 aims to
support the  features of CVC3 and SMT-LIBv2 while optimizing the design
of the core system architecture and decision procedures to take
advantage of recent engineering and algorithmic advances.
CVC4 is intended to be an open and extensible SMT engine, and 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.


Package Version Architecture Repository
cvc4-1.4-11.fc25.i686.rpm 1.4 i686 Fedora
cvc4 - - -


Name Value
cvc4-libs(x86-64) = 1.4-11.fc25 - - - - - - - - - - - - - - - - - - - - -
rtld(GNU_HASH) -


Name Value
cvc4 = 1.4-11.fc25
cvc4(x86-64) = 1.4-11.fc25
lfsc = 1.4-11.fc25


Name Value
lfsc < 1.0-1.fc25


Type URL
Binary Package cvc4-1.4-11.fc25.x86_64.rpm
Source Package cvc4-1.4-11.fc25.src.rpm

Install Howto

Install the cvc4 rpm package:

# dnf install cvc4




2016-05-17 - Jonathan Wakely <> - 1.4-11
- Rebuilt for linker errors in boost (#1331983)
2016-02-03 - Fedora Release Engineering <> - 1.4-10
- Rebuilt for
2016-01-15 - Jonathan Wakely <> - 1.4-9
- Rebuilt for Boost 1.60
2015-08-27 - Jonathan Wakely <> - 1.4-8
- Rebuilt for Boost 1.59
2015-07-29 - Fedora Release Engineering <> - 1.4-7
- Rebuilt for
2015-07-22 - David Tardon <> - 1.4-6
- rebuild for Boost 1.58
2015-06-17 - Fedora Release Engineering <> - 1.4-5
- Rebuilt for
2015-05-02 - Kalev Lember <> - 1.4-4
- Rebuilt for GCC 5 C++11 ABI change
2015-03-20 - Jerry James <> - 1.4-3
- Don't use perftools at all due to random weirdness on multiple platforms
- Also Obsoletes/Provides lfsc-devel
2015-03-11 - Jerry James <> - 1.4-2
- Add -boolean, -minisat, and -signed patches to fix test failures
- Fix boost detection with g++ 5.0
- Fix access to an uninitialized variable
- Help the documentation generator find COPYING
- Build with -fsigned-char to fix the arm build
- Prevent rebuilds while running checks
- Remove i686 from have_perftools due to test failures

See Also

Package Description
cvc4-devel-1.4-11.fc25.i686.rpm Headers and other files for developing with cvc4
cvc4-devel-1.4-11.fc25.x86_64.rpm Headers and other files for developing with cvc4
cvc4-doc-1.4-11.fc25.x86_64.rpm Interface documentation for cvc4
cvc4-java-1.4-11.fc25.i686.rpm Java interface to cvc4
cvc4-java-1.4-11.fc25.x86_64.rpm Java interface to cvc4
cvc4-libs-1.4-11.fc25.i686.rpm Library containing an automatic theorem prover for SMT problems
cvc4-libs-1.4-11.fc25.x86_64.rpm Library containing an automatic theorem prover for SMT problems
cvs-1.11.23-40.fc24.x86_64.rpm Concurrent Versions System
cvs-contrib-1.11.23-40.fc24.noarch.rpm Unsupported contributions collected by CVS developers
cvs-doc-1.11.23-40.fc24.noarch.rpm Additional documentation for Concurrent Versions System
cvs-inetd-1.11.23-40.fc24.noarch.rpm CVS server configuration for xinetd
cvs2cl-2.73-11.fc24.noarch.rpm Generate ChangeLogs from CVS working copies
cvsgraph-1.6.1-18.fc24.x86_64.rpm CVS/RCS repository grapher
cvsplot-1.7.4-16.fc24.noarch.rpm Collect statistics from CVS controlled files
cvsps-2.2-0.17.b1.fc24.x86_64.rpm Patchset tool for CVS