GNU bug report logs - #78007
[PATCH] gnu: z3: Update to 4.14.1.

Previous Next

To reply to this bug, email your comments to 78007 AT debbugs.gnu.org.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Nguyễn Gia Phong <mcsinyx <at> disroot.org>
To: guix-patches <at> gnu.org
Cc: Nguyễn Gia Phong <mcsinyx <at> disroot.org>
Subject: [PATCH] gnu: z3: Update to 4.14.1.
Date: Wed, 23 Apr 2025 17:00:29 +0900

* gnu/packages/maths.scm (z3): Update to 4.14.1.

Change-Id: Ica7152f3bc94a32444d1831dc2154df4239c1229
---
 gnu/packages/maths.scm | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index b0c5b8685c26..debdbac85bdf 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -8281,7 +8281,7 @@ (define-public yices
 (define-public z3
   (package
     (name "z3")
-    (version "4.13.0")
+    (version "4.14.1")
     (home-page "https://github.com/Z3Prover/z3")
     (source (origin
               (method git-fetch)
@@ -8290,7 +8290,7 @@ (define-public z3
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "0j46lckf3zgx2xjay7z6nvlgh47gisbbl4s3m5zn280a13fwz1ih"))))
+                "1gdknrqnnigfh1h833ks3vbrp4j74mfg6188c0k4xbl5zv6h6fx5"))))
     (build-system cmake-build-system)
     (arguments
      (list

base-commit: b12d44dd5e35ac236bf3fbb5619b9c8c2f42c902
-- 
2.49.0

Message #8 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Christopher Baines <mail <at> cbaines.net>
To: guix-patches--- via <guix-patches <at> gnu.org>
Cc: Nguyễn Gia Phong <mcsinyx <at> disroot.org>,
 Eric Bavier <bavier <at> posteo.net>, Sharlatan Hellseher <sharlatanus <at> gmail.com>,
 Andreas Enge <andreas <at> enge.fr>, 78007 <at> debbugs.gnu.org
Subject: Re: [bug#78007] [PATCH] gnu: z3: Update to 4.14.1.
Date: Sun, 27 Apr 2025 13:14:12 +0100

[Message part 1 (text/plain, inline)]

guix-patches--- via <guix-patches <at> gnu.org> writes:

> * gnu/packages/maths.scm (z3): Update to 4.14.1.
>
> Change-Id: Ica7152f3bc94a32444d1831dc2154df4239c1229
> ---
>  gnu/packages/maths.scm | 4 ++--
>  1 file changed, 2 insertions(+), 2 deletions(-)
>
> diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
> index b0c5b8685c26..debdbac85bdf 100644
> --- a/gnu/packages/maths.scm
> +++ b/gnu/packages/maths.scm
> @@ -8281,7 +8281,7 @@ (define-public yices
>  (define-public z3
>    (package
>      (name "z3")
> -    (version "4.13.0")
> +    (version "4.14.1")
>      (home-page "https://github.com/Z3Prover/z3")
>      (source (origin
>                (method git-fetch)
> @@ -8290,7 +8290,7 @@ (define-public z3
>                (file-name (git-file-name name version))
>                (sha256
>                 (base32
> -                "0j46lckf3zgx2xjay7z6nvlgh47gisbbl4s3m5zn280a13fwz1ih"))))
> +                "1gdknrqnnigfh1h833ks3vbrp4j74mfg6188c0k4xbl5zv6h6fx5"))))
>      (build-system cmake-build-system)
>      (arguments
>       (list
>
> base-commit: b12d44dd5e35ac236bf3fbb5619b9c8c2f42c902

This seems to break python-pysmt according to QA, do you see that
failure locally?

Thanks,

Chris

[signature.asc (application/pgp-signature, inline)]

Message #14 received at 78007 <at> debbugs.gnu.org (full text, mbox):

From: Andreas Enge <andreas <at> enge.fr>
To: Christopher Baines <mail <at> cbaines.net>
Cc: Nguyễn Gia Phong <mcsinyx <at> disroot.org>,
 Eric Bavier <bavier <at> posteo.net>, Sharlatan Hellseher <sharlatanus <at> gmail.com>,
 78007 <at> debbugs.gnu.org
Subject: Re: [bug#78007] [PATCH] gnu: z3: Update to 4.14.1.
Date: Mon, 28 Apr 2025 21:01:39 +0200

Hello,

Am Sun, Apr 27, 2025 at 01:14:12PM +0100 schrieb Christopher Baines:
> This seems to break python-pysmt according to QA, do you see that
> failure locally?

I can confirm the problem, with the following error message:
=========================== short test summary info ============================
FAILED pysmt/test/test_back.py::TestBasic::test_z3_back_formulae - NotImplementedError: Unknown function 'ubv_to_int'
====== 1 failed, 480 passed, 91 skipped, 65 warnings in 191.48s (0:03:11) ======

This indeed seems to indicate that the z3 API has changed in an
incompatible way.

Andreas

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.