CVS commit: pkgsrc/math/cvc5

["Alexander Nasonov" <alnsn%netbsd.org@localhost>]

Module Name:    pkgsrc
Committed By:   alnsn
Date:           Fri Sep 18 22:07:58 UTC 2026

Modified Files:
        pkgsrc/math/cvc5: Makefile distinfo

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


To generate a diff of this commit:
cvs rdiff -u -r1.5 -r1.6 pkgsrc/math/cvc5/Makefile
cvs rdiff -u -r1.1 -r1.2 pkgsrc/math/cvc5/distinfo

Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.

Modified files:

Index: pkgsrc/math/cvc5/Makefile
diff -u pkgsrc/math/cvc5/Makefile:1.5 pkgsrc/math/cvc5/Makefile:1.6
--- pkgsrc/math/cvc5/Makefile:1.5       Sat Jul 25 18:58:36 2026
+++ pkgsrc/math/cvc5/Makefile   Fri Sep 18 22:07:57 2026
@@ -1,7 +1,6 @@
-# $NetBSD: Makefile,v 1.5 2026/07/25 18:58:36 alnsn Exp $
+# $NetBSD: Makefile,v 1.6 2026/09/18 22:07:57 alnsn Exp $
 
-DISTNAME=      cvc5-1.3.4
-PKGREVISION=   1
+DISTNAME=      cvc5-1.4.0
 CATEGORIES=    math
 MASTER_SITES=  ${MASTER_SITE_GITHUB:=cvc5/}
 GITHUB_TAG=    cvc5-${PKGVERSION_NOREV}
@@ -19,6 +18,7 @@ CMAKE_CONFIGURE_ARGS+=        -DCMAKE_PREFIX_PA
 CMAKE_CONFIGURE_ARGS+= -DBUILD_SHARED_LIBS=ON
 CMAKE_CONFIGURE_ARGS+= -DUSE_PYTHON_VENV=OFF
 CMAKE_CONFIGURE_ARGS+= -DUSE_POLY=ON
+CMAKE_CONFIGURE_ARGS+= -DUSE_MPFR=ON
 
 DEPENDS+=      ${PYPKGPREFIX}-pyparsing>=3.0.9:../../devel/py-pyparsing
 
@@ -33,5 +33,6 @@ TEST_ENV+=    LD_LIBRARY_PATH=${CVC5_BUILD_
 .include "../../devel/gmp/buildlink3.mk"
 .include "../../math/cadical/buildlink3.mk"
 .include "../../math/libpoly/buildlink3.mk"
+.include "../../math/mpfr/buildlink3.mk"
 .include "../../math/symfpu/buildlink3.mk"
 .include "../../mk/bsd.pkg.mk"

Index: pkgsrc/math/cvc5/distinfo
diff -u pkgsrc/math/cvc5/distinfo:1.1 pkgsrc/math/cvc5/distinfo:1.2
--- pkgsrc/math/cvc5/distinfo:1.1       Thu Jul  2 23:20:47 2026
+++ pkgsrc/math/cvc5/distinfo   Fri Sep 18 22:07:57 2026
@@ -1,5 +1,5 @@
-$NetBSD: distinfo,v 1.1 2026/07/02 23:20:47 alnsn Exp $
+$NetBSD: distinfo,v 1.2 2026/09/18 22:07:57 alnsn Exp $
 
-BLAKE2s (cvc5-1.3.4.tar.gz) = 11f158543cb7183b5d40039f56bf49e90a4f4a5288b508555bf29dae93ecad4f
-SHA512 (cvc5-1.3.4.tar.gz) = 6e65593e9493dd2db1acc38cdf38fe3285a9ca966ded7f4ecb349927e6fce17b6d4f6cb7f9d950ab5f48f50eb59f4f7a995b74f9d244455f5f460ac66e1a6dd9
-Size (cvc5-1.3.4.tar.gz) = 9271118 bytes
+BLAKE2s (cvc5-1.4.0.tar.gz) = 44c8e4df3f32cd0877a1426045767e4371a9520a3412cf742a2c2318642afefb
+SHA512 (cvc5-1.4.0.tar.gz) = ee9578878c7e541f82a5f6c9535cd4ba764fb6d5dcdc0bf69e50cd360b2b56bc66adca1f6babd5971c5175818b3e716cb7b411488adcbf207e21ac59d0fd6d84
+Size (cvc5-1.4.0.tar.gz) = 9483162 bytes