Path to this page:
./
math/cvc5,
Automatic theorem prover for SMT (Satisfiability Modulo Theories)
Branch: CURRENT,
Version: 1.4.0,
Package name: cvc5-1.4.0,
Maintainer: pkgsrc-usersAn 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.
Master sites:
Filesize: 9260.9 KB
Version history: (Expand)
- (2026-09-19) Updated to version: cvc5-1.4.0
- (2026-07-25) Updated to version: cvc5-1.3.4nb1
- (2026-07-03) Package added to pkgsrc.se, version cvc5-1.3.4 (created)
CVS history: (Expand)
2026-09-19 00:07:58 by Alexander Nasonov | Files touched by this commit (2) |  |
Log message:
Update math/cvc5 to version 1.4.0.
## Changes
- We now require GCC >= 10 and Clang >= 12.
- Update SymFPU. Issue with divider encoding now fixed in SymFPU (related
issues: #9505, #11139, #12335).
- Fixes parsing issues related to unchecked overflowing of indexed
bit-vector operators. This impacts bit-vector operators having width
that is greater than or equal to `2^32`.
- Fixes a bug where the character code point `\u{30000}` was incorrectly
treated as a valid code point.
- Fixes a parsing bug with option `--parse-skolem-definitions`.
- Fixes a soundness bug in the `--learned-rewrite` preprocessing pass.
- We now allow using option `--solve-bv-as-int` with quantifiers, even if the
quantified variables occur under UFs.
- Fixes an issue where the parser would abort prematurely when `get-value` was
called after an unsat response when uninterpreted sorts are present.
- Fixes issues related to theory combination with arrays and non-linear
arithmetic.
- Added full proof support in CaDiCaL, meaning `--sat-solver=cadical` can now be
used in combination with proofs `--produce-proofs`.
- Improved proof support for Alethe: full translation for CPC fragment for
logics in AUFNIRA.
- Minor updates and fixes to the CPC proof signature. The current CPC proofs are
checkable by Ethos 0.2.3 (`./contrib/get-ethos-checker`).
--
View it on GitHub:
https://github.com/cvc5/cvc5/releases/tag/cvc5-1.4.0
|
| 2026-07-25 20:58:36 by Alexander Nasonov | Files touched by this commit (1) |
Log message:
math/cadical is build-only dep, bump pkgrev.
|
| 2026-07-04 00:03:50 by Alexander Nasonov | Files touched by this commit (1) |
Log message:
TEST_TARGET=check is better.
|
| 2026-07-03 22:36:34 by Alexander Nasonov | Files touched by this commit (1) |
Log message:
Pass LD_LIBRARY_PATH to TEST_ENV.
|
| 2026-07-03 01:52:13 by Alexander Nasonov | Files touched by this commit (1) |
Log message:
Add LD_LIBRARY_PATH to testing instruction.
This improves success rate to 99%.
$ export LD_LIBRARY_PATH=$(pwd)/src:$(pwd)/src/parser:$(pwd)/src/main
$ ctest -j32
...
99% tests passed, 1 tests failed out of 4291
Label Time Summary:
api capi = 0.18 sec*proc (7 tests)
api cppapi = 4.69 sec*proc (70 tests)
regress0 = 815.38 sec*proc (2540 tests)
regress1 = 709.94 sec*proc (1468 tests)
regress2 = 211.87 sec*proc (145 tests)
regress3 = 1082.17 sec*proc (51 tests)
regress4 = 663.37 sec*proc (10 tests)
Total Test time (real) = 347.30 sec
The following tests did not run:
... 52 skipped regress0 tests ...
The following tests FAILED:
4157 - regress3/bags/reduce_constants_dup.smt2 (Failed) regress3
|
| 2026-07-03 01:20:47 by Alexander Nasonov | Files touched by this commit (4) |
Log message:
Initial import of math/cvc5 version 1.3.4.
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.
|