From debbugs-submit-bounces@debbugs.gnu.org Wed Apr 23 04:01:13 2025 Received: (at submit) by debbugs.gnu.org; 23 Apr 2025 08:01:13 +0000 Received: from localhost ([127.0.0.1]:52507 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1u7V2e-00007g-Qt for submit@debbugs.gnu.org; Wed, 23 Apr 2025 04:01:13 -0400 Received: from lists.gnu.org ([2001:470:142::17]:50904) by debbugs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.84_2) (envelope-from ) id 1u7V2Z-00006C-6C for submit@debbugs.gnu.org; Wed, 23 Apr 2025 04:01:10 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1u7V2S-0000yP-FE for guix-patches@gnu.org; Wed, 23 Apr 2025 04:01:00 -0400 Received: from layka.disroot.org ([178.21.23.139]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1u7V2P-0005fG-Vu for guix-patches@gnu.org; Wed, 23 Apr 2025 04:01:00 -0400 Received: from mail01.disroot.lan (localhost [127.0.0.1]) by disroot.org (Postfix) with ESMTP id DBC7525D1E; Wed, 23 Apr 2025 10:00:52 +0200 (CEST) X-Virus-Scanned: SPAM Filter at disroot.org Received: from layka.disroot.org ([127.0.0.1]) by localhost (disroot.org [127.0.0.1]) (amavis, port 10024) with ESMTP id DM7AKulbGk7Y; Wed, 23 Apr 2025 10:00:52 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail; t=1745395252; bh=Vuxk1dp4evCFk6luVK8SsTvaiOSe51wHrv0127z+ru0=; h=From:To:Cc:Subject:Date; b=fRrkNoU733y5OcayALLyod9oAhCDUEe62N3OvAmVPqJHuSJ/fk/MQybBBnGytyoTt vmsmpLX5derN5KTTexUbs5Uek4KrC1/cfqgXKNj+NvUpL0DYu3QsGEicgwtwlAWVPq TDfabdKKeBwLRLIQaKtqA0ok0Le1YcP4rTJdXE3fic9uLNNnv6adKbT7ORwQB/bIxf TZ4Lt8pAipWGB7nxzTynWuMA33mCiQazW1wjrtctNXN0J9OVga1aqY+TJD0RQEMWLk JUz/AIQ6Sfmch2Pe2cRHVkyrjeSQcliIb2grUgpRBxI4CN8tzWDpYN1y/1Qgm95iOV NoLlJOzWbKhwA== From: =?UTF-8?q?Nguy=E1=BB=85n=20Gia=20Phong?= To: guix-patches@gnu.org Subject: [PATCH] gnu: z3: Update to 4.14.1. Date: Wed, 23 Apr 2025 17:00:29 +0900 Message-ID: MIME-Version: 1.0 X-Debbugs-Cc: Andreas Enge , Eric Bavier , Sharlatan Hellseher Content-Transfer-Encoding: 8bit Received-SPF: pass client-ip=178.21.23.139; envelope-from=mcsinyx@disroot.org; helo=layka.disroot.org X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, RCVD_IN_VALIDITY_CERTIFIED_BLOCKED=0.001, RCVD_IN_VALIDITY_RPBL_BLOCKED=0.001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no X-Spam_action: no action X-Spam-Score: 0.9 (/) X-Debbugs-Envelope-To: submit Cc: =?UTF-8?q?Nguy=E1=BB=85n=20Gia=20Phong?= X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.1 (/) * 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 From debbugs-submit-bounces@debbugs.gnu.org Sun Apr 27 08:14:36 2025 Received: (at submit) by debbugs.gnu.org; 27 Apr 2025 12:14:36 +0000 Received: from localhost ([127.0.0.1]:40030 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1u90u3-0000F2-TE for submit@debbugs.gnu.org; Sun, 27 Apr 2025 08:14:36 -0400 Received: from lists.gnu.org ([2001:470:142::17]:57392) by debbugs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.84_2) (envelope-from ) id 1u90tr-0000EG-DU for submit@debbugs.gnu.org; Sun, 27 Apr 2025 08:14:23 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1u90tl-0006Zi-VJ for guix-patches@gnu.org; Sun, 27 Apr 2025 08:14:18 -0400 Received: from mira.cbaines.net ([212.71.252.8]) by eggs.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1u90tk-0007up-8z for guix-patches@gnu.org; Sun, 27 Apr 2025 08:14:17 -0400 Received: from localhost (unknown [IPv6:2a02:6b67:e390:8b00::1ce5]) by mira.cbaines.net (Postfix) with ESMTPSA id 4815327BC49; Sun, 27 Apr 2025 13:14:15 +0100 (BST) Received: from fang (localhost [127.0.0.1]) by localhost (OpenSMTPD) with ESMTP id 1d7181b7; Sun, 27 Apr 2025 12:14:14 +0000 (UTC) From: Christopher Baines To: guix-patches--- via Subject: Re: [bug#78007] [PATCH] gnu: z3: Update to 4.14.1. In-Reply-To: (guix-patches@gnu.org's message of "Wed, 23 Apr 2025 17:00:29 +0900") References: User-Agent: mu4e 1.12.9; emacs 29.4 Date: Sun, 27 Apr 2025 13:14:12 +0100 Message-ID: <87bjshg5t7.fsf@cbaines.net> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha512; protocol="application/pgp-signature" Received-SPF: pass client-ip=212.71.252.8; envelope-from=mail@cbaines.net; helo=mira.cbaines.net X-Spam_score_int: -18 X-Spam_score: -1.9 X-Spam_bar: - X-Spam_report: (-1.9 / 5.0 requ) BAYES_00=-1.9, RCVD_IN_VALIDITY_CERTIFIED_BLOCKED=0.001, RCVD_IN_VALIDITY_RPBL_BLOCKED=0.001, SPF_HELO_PASS=-0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no X-Spam_action: no action X-Spam-Score: 0.9 (/) X-Debbugs-Envelope-To: submit Cc: =?utf-8?Q?Nguy=E1=BB=85n?= Gia Phong , Eric Bavier , Sharlatan Hellseher , Andreas Enge , 78007@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.1 (/) --=-=-= Content-Type: text/plain guix-patches--- via 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 --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQKlBAEBCgCPFiEEPonu50WOcg2XVOCyXiijOwuE9XcFAmgOH5RfFIAAAAAALgAo aXNzdWVyLWZwckBub3RhdGlvbnMub3BlbnBncC5maWZ0aGhvcnNlbWFuLm5ldDNF ODlFRUU3NDU4RTcyMEQ5NzU0RTBCMjVFMjhBMzNCMEI4NEY1NzcRHG1haWxAY2Jh aW5lcy5uZXQACgkQXiijOwuE9XeBzw//YVxEVUZLK/PZ5OZTbWDb9wQwdkcLdjcq NPTiP203NZOD9ytewEqLIW7TCUIt4+kSQNki6LhYSG+YrfT1TmVtzyEtP7jj5g4Z WTIwU9OmdVFB6tiEiGT3ra82yGaWQ5oO/1Rf1uWcTJ7OrXrPhwB+1UHyUooqXr85 IRZws9FuWWmwwTvrfw8Axhy3dDMH4pMF2NJ1TC9cmPCrR3Hd+bUE2U0R61XBlByc UfZzFvgjzMd4UME/ZqCvKaocZWICT4qjYxEJA5pp7VqGjvf3uXsyhq3BDojKNSB6 +pKnZ3Yt2OE3Og0hdTYJk0hQ8VHv+SQJE/qTgp2L3qDA2gVMTrcv781YbIDIndFB j+KSZT5r55oFMLLexc3JZM9vHORDq0WtADzN9vbqBR+4soscpYLDREjoEbCes0V/ x+ZXOTqgMve0Jc+K8egaApecR10Ebq6EuQ+ZML8rC7gz5OqvMwZit2RLU7wf08vM Ss44nvUUgq/SfAK2plBLKgrYy4Ow9M8M/h/9Z53/N/nN70wGxbjYx4GvZj3x9qKg kXG3RO5uCk6u67x7805dbLiLZ4gKOY+kprkNtor2hPry5K73tVl8UzNQNHn/hM8P d1M6l4QsEiFzWFF6JF4ONxRDV87qjuwfPN70S/xRYNGjGVMu6uOPKR0sWitxu53w 28WLR2wa3bg= =kIMv -----END PGP SIGNATURE----- --=-=-=-- From debbugs-submit-bounces@debbugs.gnu.org Mon Apr 28 15:02:00 2025 Received: (at 78007) by debbugs.gnu.org; 28 Apr 2025 19:02:01 +0000 Received: from localhost ([127.0.0.1]:35361 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1u9Tjq-00055P-Ek for submit@debbugs.gnu.org; Mon, 28 Apr 2025 15:02:00 -0400 Received: from hera.aquilenet.fr ([185.233.100.1]:43728) by debbugs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.84_2) (envelope-from ) id 1u9Tjk-00053n-Rs for 78007@debbugs.gnu.org; Mon, 28 Apr 2025 15:01:55 -0400 Received: from localhost (localhost [127.0.0.1]) by hera.aquilenet.fr (Postfix) with ESMTP id 2E740806; Mon, 28 Apr 2025 21:01:45 +0200 (CEST) Authentication-Results: hera.aquilenet.fr; none X-Virus-Scanned: Debian amavis at hera.aquilenet.fr Received: from hera.aquilenet.fr ([127.0.0.1]) by localhost (hera.aquilenet.fr [127.0.0.1]) (amavis, port 10024) with ESMTP id PWrn9RsUPwty; Mon, 28 Apr 2025 21:01:43 +0200 (CEST) Received: from jurong (176-179-191-150.abo.bbox.fr [176.179.191.150]) by hera.aquilenet.fr (Postfix) with ESMTPSA id 44FCC1D0; Mon, 28 Apr 2025 21:01:41 +0200 (CEST) Date: Mon, 28 Apr 2025 21:01:39 +0200 From: Andreas Enge To: Christopher Baines Subject: Re: [bug#78007] [PATCH] gnu: z3: Update to 4.14.1. Message-ID: References: <87bjshg5t7.fsf@cbaines.net> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <87bjshg5t7.fsf@cbaines.net> X-Rspamd-Queue-Id: 2E740806 X-Spamd-Result: default: False [-5.60 / 15.00]; NEURAL_HAM(-3.00)[-1.000]; BAYES_HAM(-3.00)[99.99%]; MID_RHS_NOT_FQDN(0.50)[]; MIME_GOOD(-0.10)[text/plain]; FROM_EQ_ENVFROM(0.00)[]; MIME_TRACE(0.00)[0:+]; RCVD_TLS_ALL(0.00)[]; RCVD_COUNT_TWO(0.00)[2]; ARC_NA(0.00)[]; RCPT_COUNT_FIVE(0.00)[5]; FREEMAIL_ENVRCPT(0.00)[gmail.com]; RCVD_VIA_SMTP_AUTH(0.00)[]; TO_MATCH_ENVRCPT_ALL(0.00)[]; FROM_HAS_DN(0.00)[]; TO_DN_SOME(0.00)[]; FREEMAIL_CC(0.00)[debbugs.gnu.org,disroot.org,posteo.net,gmail.com] X-Rspamd-Action: no action X-Spamd-Bar: ----- X-Rspamd-Server: hera X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 78007 Cc: =?utf-8?B?Tmd1eeG7hW4=?= Gia Phong , Eric Bavier , Sharlatan Hellseher , 78007@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) 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