./math/cvc5, Automatic theorem prover for SMT (Satisfiability Modulo Theories)

[ Image CVSweb ] [ Image Homepage ] [ Image RSS ] [ Image Required by ]


Branch: CURRENT, Version: 1.3.4nb1, Package name: cvc5-1.3.4nb1, Maintainer: pkgsrc-users

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.


Master sites:

Filesize: 9053.826 KB

Version history: (Expand)


CVS history: (Expand)


   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.