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

Previous Next

Full log

View this message in rfc822 format

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: [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.