From patchwork Fri Jan 10 12:59:21 2025 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Patchwork-Submitter: tusharhero--- via Guix-patches via X-Patchwork-Id: 38179 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id C116F27BBEA; Sun, 2 Feb 2025 15:09:33 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-6.4 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,MAILING_LIST_MULTI,RCVD_IN_DNSWL_BLOCKED, RCVD_IN_VALIDITY_CERTIFIED,RCVD_IN_VALIDITY_RPBL,RCVD_IN_VALIDITY_SAFE, SPF_HELO_PASS autolearn=ham autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 1D85927BBE2 for ; Sun, 2 Feb 2025 15:09:31 +0000 (GMT) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1tebax-0005tP-46; Sun, 02 Feb 2025 10:09:11 -0500 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 1tebat-0005ng-SA for guix-patches@gnu.org; Sun, 02 Feb 2025 10:09:07 -0500 Received: from debbugs.gnu.org ([2001:470:142:5::43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1tebao-0004KF-SP for guix-patches@gnu.org; Sun, 02 Feb 2025 10:09:07 -0500 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=debbugs.gnu.org; s=debbugs-gnu-org; h=MIME-Version:Date:From:To:In-Reply-To:References:Subject; bh=JVqmnGZUBm0q4pTCSU3bC5phzI+uR8g0Ihrk1TjJQ9g=; b=qCNcqnBw/BqO/uzfocDM3og28WqiziRnp/i1vamvBBsq2sgzlujPY/xWmIYh8ioyz5wIHH3LgyWY5AFG+Yi51T+qpl+RS9LYwq9nl8jJXKJqwlYgllWzpCrFPfr0qPY4Wvj6pk8gWlIhEnAbidPiqsjsyTFNz9oTc0w5co4GT3oBOmixs5Q4rHUq16+vU38zp3gKtokU2Zxr4nrKhTyfcQgIEWCa6KLc7r++2X1BGag5KI2EYaj9ZPtIftpgVwy/g6HU5mDV4P1X7JLFLJyw3F5EEydNrQ0DGgQkM6AjbyshAn4yGz32zURHX4GLI3L3cguJacbnSgwcGxK0lMC+SQ==; Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1tebao-0000Im-LY for guix-patches@gnu.org; Sun, 02 Feb 2025 10:09:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#75476] [PATCH v2] gnu: python-pysmt: Update to 0.9.6. References: <2ed2dee408f62e2498758555d01bb603dfa866f4.1736513961.git.mcsinyx@disroot.org> In-Reply-To: <2ed2dee408f62e2498758555d01bb603dfa866f4.1736513961.git.mcsinyx@disroot.org> Resent-From: ngraves@ngraves.fr Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 02 Feb 2025 15:09:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 75476 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 75476@debbugs.gnu.org Cc: =?utf-8?b?Tmd1eeG7hW4=?= Gia Phong Received: via spool by 75476-submit@debbugs.gnu.org id=B75476.17385089081103 (code B ref 75476); Sun, 02 Feb 2025 15:09:02 +0000 Received: (at 75476) by debbugs.gnu.org; 2 Feb 2025 15:08:28 +0000 Received: from localhost ([127.0.0.1]:35821 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1teba6-0000HV-1L for submit@debbugs.gnu.org; Sun, 02 Feb 2025 10:08:28 -0500 Received: from 3.mo576.mail-out.ovh.net ([188.165.52.203]:34771) by debbugs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.84_2) (envelope-from ) id 1teba0-0000HG-0x for 75476@debbugs.gnu.org; Sun, 02 Feb 2025 10:08:16 -0500 Received: from director6.ghost.mail-out.ovh.net (unknown [10.108.25.63]) by mo576.mail-out.ovh.net (Postfix) with ESMTP id 4YmCgF4Zb7z1rD5 for <75476@debbugs.gnu.org>; Sun, 2 Feb 2025 15:08:09 +0000 (UTC) Received: from ghost-submission-5b5ff79f4f-b6j4t (unknown [10.111.174.38]) by director6.ghost.mail-out.ovh.net (Postfix) with ESMTPS id C085C1FD36; Sun, 2 Feb 2025 15:08:08 +0000 (UTC) Received: from ngraves.fr ([37.59.142.105]) by ghost-submission-5b5ff79f4f-b6j4t with ESMTPSA id HiLXEliKn2f8AwAAnLym/g (envelope-from ); Sun, 02 Feb 2025 15:08:08 +0000 Authentication-Results: garm.ovh; auth=pass (GARM-105G006d88cd71d-36d8-4ee8-b849-0eaf82435def, 0EB4F4ACF34A069A1D12270FF355DD325781616A) smtp.auth=ngraves@ngraves.fr X-OVh-ClientIp: 89.207.171.131 Date: Fri, 10 Jan 2025 21:59:21 +0900 Message-ID: <87plk0l6zs.fsf@ngraves.fr> MIME-Version: 1.0 X-Ovh-Tracer-Id: 9968999253762826820 X-VR-SPAMSTATE: OK X-VR-SPAMSCORE: 21 X-VR-SPAMCAUSE: gggruggvucftvghtrhhoucdtuddrgeefvddrtddtgddugeellecutefuodetggdotefrodftvfcurfhrohhfihhlvgemucfqggfjpdevjffgvefmvefgnecuuegrihhlohhuthemucehtddtnecuffgrthgvuchinhcuphgrshhtucdlvddumdenucfjughrpefhvfevufffkfggtgfgsehtqhertddttdejnecuhfhrohhmpehnghhrrghvvghssehnghhrrghvvghsrdhfrhenucggtffrrghtthgvrhhnpeetleehffefvddtffelkeffveelgeejudevveelkeejteejgfegjedtgedtffehleenucffohhmrghinhepghhithhhuhgsrdgtohhmnecukfhppeduvdejrddtrddtrddupdekledrvddtjedrudejuddrudefuddpfeejrdehledrudegvddruddtheenucevlhhushhtvghrufhiiigvpedtnecurfgrrhgrmhepihhnvghtpeduvdejrddtrddtrddupdhmrghilhhfrhhomhepnhhgrhgrvhgvshesnhhgrhgrvhgvshdrfhhrpdhnsggprhgtphhtthhopedupdhrtghpthhtohepjeehgeejieesuggvsggsuhhgshdrghhnuhdrohhrghdpoffvtefjohhsthepmhhoheejiegmpdhmohguvgepshhmthhpohhuth DKIM-Signature: a=rsa-sha256; bh=JVqmnGZUBm0q4pTCSU3bC5phzI+uR8g0Ihrk1TjJQ9g=; c=relaxed/relaxed; d=ngraves.fr; h=From; s=ovhmo4487190-selector1; t=1738508889; v=1; b=1C3h67eLvy3YfLwvTkqiw2/kmYplWMMO4OutRl/wOSEyw4JYwjiJN7ToXavwN8exORZ7sRwS 6iGKHiunnBsi6T8YGsefkapqJHs6vP7Atn11XLe6MXdDoeRRktxJaLMPgN5V678nUMz92SKmpKR iAOPteT3vLulSg+UruzJGqnTULOneRyBDjTZQe/C2Rmu+vzEOBjUrThnRmMohYswNvKPC5n340f yEIkKsCoZT4yK8pgLzcBzZMMENcxw8xq1DmWCafOMixBMz8tluCzUsATRa+D5S4rVcxlxNZ7q/5 AV/Z5haSztwOeJ7kRcAX/avsFnkFoINbpikfi2ilPEwUw== X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Reply-to: ngraves@ngraves.fr X-ACL-Warn: , ngraves--- via Guix-patches X-Patchwork-Original-From: ngraves--- via Guix-patches via From: tusharhero--- via Guix-patches via Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches * gnu/packages/python-xyz.scm (python-pysmt): Update to 0.9.6. * gnu/packages/patches/python-pysmt-fix-pow-return-type.patch: Remove file. * gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch: Remove file. * gnu/local.mk (dist_patch_DATA): Unregister them. Change-Id: I4ecdad59abbb1c755a5be081cf3bf75992b36fb3 --- gnu/local.mk | 2 - .../python-pysmt-fix-pow-return-type.patch | 258 ------------------ ...-pysmt-fix-smtlib-serialization-test.patch | 86 ------ gnu/packages/python-xyz.scm | 7 +- 4 files changed, 3 insertions(+), 350 deletions(-) delete mode 100644 gnu/packages/patches/python-pysmt-fix-pow-return-type.patch delete mode 100644 gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch -- 2.48.1 -- Best regards, Nicolas Graves diff --git a/gnu/local.mk b/gnu/local.mk index aa91977391..799fcb0aae 100644 --- a/gnu/local.mk +++ b/gnu/local.mk @@ -2109,8 +2109,6 @@ dist_patch_DATA = \ %D%/packages/patches/python-paste-remove-timing-test.patch \ %D%/packages/patches/python-pyan3-fix-absolute-path-bug.patch \ %D%/packages/patches/python-pyan3-fix-positional-arguments.patch \ - %D%/packages/patches/python-pysmt-fix-pow-return-type.patch \ - %D%/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch \ %D%/packages/patches/python-pytorch-fix-codegen.patch \ %D%/packages/patches/python-pytorch-runpath.patch \ %D%/packages/patches/python-pytorch-system-libraries.patch \ diff --git a/gnu/packages/patches/python-pysmt-fix-pow-return-type.patch b/gnu/packages/patches/python-pysmt-fix-pow-return-type.patch deleted file mode 100644 index 0ec2d41b3c..0000000000 --- a/gnu/packages/patches/python-pysmt-fix-pow-return-type.patch +++ /dev/null @@ -1,258 +0,0 @@ -Backport of an upstream patch which fixes a test failure with our -packaged version of the Z3 SMT solver. - -Taken from: https://github.com/pysmt/pysmt/commit/f522e8cd8f3e75ff85f5eae29b427e18a6701859 - -diff --git a/pysmt/formula.py b/pysmt/formula.py -index ea4b46c..6cb9cbf 100644 ---- a/pysmt/formula.py -+++ b/pysmt/formula.py -@@ -252,11 +252,7 @@ class FormulaManager(object): - - if base.is_constant(): - val = base.constant_value() ** exponent.constant_value() -- if base.is_constant(types.REAL): -- return self.Real(val) -- else: -- assert base.is_constant(types.INT) -- return self.Int(val) -+ return self.Real(val) - return self.create_node(node_type=op.POW, args=(base, exponent)) - - def Div(self, left, right): -diff --git a/pysmt/logics.py b/pysmt/logics.py -index ef88dd6..9dc45b1 100644 ---- a/pysmt/logics.py -+++ b/pysmt/logics.py -@@ -495,6 +495,12 @@ QF_NRA = Logic(name="QF_NRA", - real_arithmetic=True, - linear=False) - -+QF_NIRA = Logic(name="QF_NIRA", -+ description="""Quantifier-free integer and real arithmetic.""", -+ quantifier_free=True, -+ integer_arithmetic=True, -+ real_arithmetic=True, -+ linear=False) - - QF_RDL = Logic(name="QF_RDL", - description=\ -@@ -619,41 +625,41 @@ QF_AUFBVLIRA = Logic(name="QF_AUFBVLIRA", - AUTO = Logic(name="Auto", - description="Special logic used to indicate that the logic to be used depends on the formula.") - --SMTLIB2_LOGICS = frozenset([ AUFLIA, -- AUFLIRA, -- AUFNIRA, -- ALIA, -- LRA, -- LIA, -- NIA, -- NRA, -- UFLRA, -- UFNIA, -- UFLIRA, -- QF_ABV, -- QF_AUFBV, -- QF_AUFLIA, -- QF_ALIA, -- QF_AX, -- QF_BV, -- QF_IDL, -- QF_LIA, -- QF_LRA, -- QF_NIA, -- QF_NRA, -- QF_RDL, -- QF_UF, -- QF_UFBV , -- QF_UFIDL, -- QF_UFLIA, -- QF_UFLRA, -- QF_UFNRA, -- QF_UFNIA, -- QF_UFLIRA, -- QF_SLIA -- ]) -- --LOGICS = SMTLIB2_LOGICS | frozenset([ QF_BOOL, BOOL, QF_AUFBVLIRA]) -+SMTLIB2_LOGICS = frozenset([AUFLIA, -+ AUFLIRA, -+ AUFNIRA, -+ ALIA, -+ LRA, -+ LIA, -+ NIA, -+ NRA, -+ UFLRA, -+ UFNIA, -+ UFLIRA, -+ QF_ABV, -+ QF_AUFBV, -+ QF_AUFLIA, -+ QF_ALIA, -+ QF_AX, -+ QF_BV, -+ QF_IDL, -+ QF_LIA, -+ QF_LRA, -+ QF_NIA, -+ QF_NRA, -+ QF_RDL, -+ QF_UF, -+ QF_UFBV, -+ QF_UFIDL, -+ QF_UFLIA, -+ QF_UFLRA, -+ QF_UFNRA, -+ QF_UFNIA, -+ QF_UFLIRA, -+ QF_SLIA -+ ]) -+ -+LOGICS = SMTLIB2_LOGICS | frozenset([QF_BOOL, BOOL, QF_AUFBVLIRA, QF_NIRA]) - - QF_LOGICS = frozenset(_l for _l in LOGICS if _l.quantifier_free) - -@@ -668,8 +674,8 @@ PYSMT_LOGICS = frozenset([QF_BOOL, QF_IDL, QF_LIA, QF_LRA, QF_RDL, QF_UF, QF_UFI - QF_BV, QF_UFBV, - QF_ABV, QF_AUFBV, QF_AUFLIA, QF_ALIA, QF_AX, - QF_AUFBVLIRA, -- QF_NRA, QF_NIA, UFBV, BV, -- ]) -+ QF_NRA, QF_NIA, QF_NIRA, UFBV, BV, -+ ]) - - # PySMT Logics includes additional features: - # - constant arrays: QF_AUFBV becomes QF_AUFBV* -@@ -697,7 +703,6 @@ for l in PYSMT_LOGICS: - ext_logics.add(nl) - - -- - LOGICS = LOGICS | frozenset(ext_logics) - PYSMT_LOGICS = PYSMT_LOGICS | frozenset(ext_logics) - -diff --git a/pysmt/solvers/z3.py b/pysmt/solvers/z3.py -index 3fb42b9..210b771 100644 ---- a/pysmt/solvers/z3.py -+++ b/pysmt/solvers/z3.py -@@ -595,6 +595,8 @@ class Z3Converter(Converter, DagWalker): - None, None, - 0, None, - expr.ast) -+ print("Z3: SMTLIB") -+ print(s) - stream_in = StringIO(s) - r = parser.get_script(stream_in).get_last_formula(self.mgr) - key = (askey(expr), None) -diff --git a/pysmt/test/examples.py b/pysmt/test/examples.py -index 73455ee..b653185 100644 ---- a/pysmt/test/examples.py -+++ b/pysmt/test/examples.py -@@ -898,12 +898,12 @@ def get_full_example_formulae(environment=None): - logic=pysmt.logics.QF_NRA - ), - -- Example(hr="((p ^ 2) = 0)", -- expr=Equals(Pow(p, Int(2)), Int(0)), -+ Example(hr="((p ^ 2) = 0.0)", -+ expr=Equals(Pow(p, Int(2)), Real(0)), - is_valid=False, - is_sat=True, -- logic=pysmt.logics.QF_NIA -- ), -+ logic=pysmt.logics.QF_NIRA -+ ), - - Example(hr="((r ^ 2.0) = 0.0)", - expr=Equals(Pow(r, Real(2)), Real(0)), -diff --git a/pysmt/test/test_back.py b/pysmt/test/test_back.py -index bceb45b..7a0ad63 100644 ---- a/pysmt/test/test_back.py -+++ b/pysmt/test/test_back.py -@@ -55,10 +55,10 @@ class TestBasic(TestCase): - res = msat.converter.back(term) - self.assertFalse(f == res) - -- def do_back(self, solver_name, z3_string_buffer=False): -+ def do_back(self, solver_name, via_smtlib=False): - for formula, _, _, logic in get_example_formulae(): - if logic.quantifier_free: -- if logic.theory.custom_type and z3_string_buffer: -+ if logic.theory.custom_type and via_smtlib: - # Printing of declare-sort from Z3 is not conformant - # with the SMT-LIB. We might consider extending our - # parser. -@@ -67,7 +67,7 @@ class TestBasic(TestCase): - s = Solver(name=solver_name, logic=logic) - term = s.converter.convert(formula) - if solver_name == "z3": -- if z3_string_buffer: -+ if via_smtlib: - res = s.converter.back_via_smtlib(term) - else: - res = s.converter.back(term) -@@ -84,8 +84,8 @@ class TestBasic(TestCase): - - @skipIfSolverNotAvailable("z3") - def test_z3_back_formulae(self): -- self.do_back("z3", z3_string_buffer=False) -- self.do_back("z3", z3_string_buffer=True) -+ self.do_back("z3", via_smtlib=True) -+ self.do_back("z3", via_smtlib=False) - - - if __name__ == '__main__': -diff --git a/pysmt/type_checker.py b/pysmt/type_checker.py -index b700fcf..7ce05aa 100644 ---- a/pysmt/type_checker.py -+++ b/pysmt/type_checker.py -@@ -33,6 +33,8 @@ class SimpleTypeChecker(walkers.DagWalker): - - def __init__(self, env=None): - walkers.DagWalker.__init__(self, env=env) -+ # Return None if the type cannot be computed rather than -+ # raising an exception. - self.be_nice = False - - def _get_key(self, formula, **kwargs): -@@ -42,7 +44,7 @@ class SimpleTypeChecker(walkers.DagWalker): - """ Returns the pysmt.types type of the formula """ - res = self.walk(formula) - if not self.be_nice and res is None: -- raise PysmtTypeError("The formula '%s' is not well-formed" \ -+ raise PysmtTypeError("The formula '%s' is not well-formed" - % str(formula)) - return res - -@@ -114,7 +116,7 @@ class SimpleTypeChecker(walkers.DagWalker): - - def walk_bv_comp(self, formula, args, **kwargs): - # We check that all children are BV and the same size -- a,b = args -+ a, b = args - if a != b or (not a.is_bv_type()): - return None - return BVType(1) -@@ -187,7 +189,7 @@ class SimpleTypeChecker(walkers.DagWalker): - if args[0].is_bool_type(): - raise PysmtTypeError("The formula '%s' is not well-formed." - "Equality operator is not supported for Boolean" -- " terms. Use Iff instead." \ -+ " terms. Use Iff instead." - % str(formula)) - elif args[0].is_bv_type(): - return self.walk_bv_to_bool(formula, args) -@@ -324,10 +326,7 @@ class SimpleTypeChecker(walkers.DagWalker): - def walk_pow(self, formula, args, **kwargs): - if args[0] != args[1]: - return None -- # Exponent must be positive for INT -- if args[0].is_int_type() and formula.arg(1).constant_value() < 0 : -- return None -- return args[0] -+ return REAL - - # EOC SimpleTypeChecker - diff --git a/gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch b/gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch deleted file mode 100644 index eee555f807..0000000000 --- a/gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch +++ /dev/null @@ -1,86 +0,0 @@ -Backport of an upstream patch fixing a test suite failure. - -Taken from: https://github.com/pysmt/pysmt/commit/a246669a487aff69f5da34570ef867841d18508a - -diff --git a/pysmt/test/smtlib/test_parser_examples.py b/pysmt/test/smtlib/test_parser_examples.py -index cca4194..c0852be 100644 ---- a/pysmt/test/smtlib/test_parser_examples.py -+++ b/pysmt/test/smtlib/test_parser_examples.py -@@ -29,6 +29,7 @@ from pysmt.shortcuts import Iff - from pysmt.shortcuts import read_smtlib, write_smtlib, get_env - from pysmt.exceptions import PysmtSyntaxError - -+ - class TestSMTParseExamples(TestCase): - - def test_parse_examples(self): -@@ -41,7 +42,6 @@ class TestSMTParseExamples(TestCase): - buf = StringIO() - script_out = smtlibscript_from_formula(f_out) - script_out.serialize(outstream=buf) -- #print(buf) - - buf.seek(0) - parser = SmtLibParser() -@@ -49,7 +49,6 @@ class TestSMTParseExamples(TestCase): - f_in = script_in.get_last_formula() - self.assertEqual(f_in.simplify(), f_out.simplify()) - -- - @skipIfNoSolverForLogic(logics.QF_BV) - def test_parse_examples_bv(self): - """For BV we represent a superset of the operators defined in SMT-LIB. -@@ -108,7 +107,18 @@ class TestSMTParseExamples(TestCase): - self.assertValid(Iff(f_in, f_out), f_in.serialize()) - - def test_dumped_logic(self): -- # Dumped logic matches the logic in the example -+ # Dumped logic matches the logic in the example. -+ # -+ # There are a few cases where we use a logic -+ # that does not exist in SMT-LIB, and the SMT-LIB -+ # serialization logic will find a logic that -+ # is more expressive. We need to adjust the test -+ # for those cases (see rewrite dict below). -+ rewrite = { -+ logics.QF_BOOL: logics.QF_UF, -+ logics.BOOL: logics.LRA, -+ logics.QF_NIRA: logics.AUFNIRA, -+ } - fs = get_example_formulae() - - for (f_out, _, _, logic) in fs: -@@ -121,14 +131,9 @@ class TestSMTParseExamples(TestCase): - for cmd in script_in: - if cmd.name == "set-logic": - logic_in = cmd.args[0] -- if logic == logics.QF_BOOL: -- self.assertEqual(logic_in, logics.QF_UF) -- elif logic == logics.BOOL: -- self.assertEqual(logic_in, logics.LRA) -- else: -- self.assertEqual(logic_in, logic, script_in) -+ self.assertEqual(logic_in, rewrite.get(logic, logic)) - break -- else: # Loops exited normally -+ else: # Loops exited normally - print("-"*40) - print(script_in) - -@@ -136,7 +141,7 @@ class TestSMTParseExamples(TestCase): - fs = get_example_formulae() - - fdi, tmp_fname = mkstemp() -- os.close(fdi) # Close initial file descriptor -+ os.close(fdi) # Close initial file descriptor - for (f_out, _, _, _) in fs: - write_smtlib(f_out, tmp_fname) - # with open(tmp_fname) as fin: -@@ -197,7 +202,6 @@ class TestSMTParseExamples(TestCase): - f_in = script.get_last_formula() - self.assertSat(f_in) - -- - def test_int_promotion_define_fun(self): - script = """ - (define-fun x () Int 8) diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm index 763b0fee77..dc175d7a49 100644 --- a/gnu/packages/python-xyz.scm +++ b/gnu/packages/python-xyz.scm @@ -161,6 +161,7 @@ ;;; Copyright © 2024 Markku Korkeala ;;; Copyright © 2025 Jordan Moore ;;; Copyright © 2025 Dariqq +;;; Copyright © 2025 Nguyễn Gia Phong ;;; ;;; This file is part of GNU Guix. ;;; @@ -36112,19 +36113,17 @@ (define-public python-claripy (define-public python-pysmt (package (name "python-pysmt") - (version "0.9.5") + (version "0.9.6") (source (origin ;; Fetching from Git as pypi release doesn't include all test files. (method git-fetch) - (patches (search-patches "python-pysmt-fix-pow-return-type.patch" - "python-pysmt-fix-smtlib-serialization-test.patch")) (uri (git-reference (url "https://github.com/pysmt/pysmt") (commit (string-append "v" version)))) (file-name (git-file-name name version)) (sha256 - (base32 "0hrxv23y5ip4ijfx5pvbwc2fq4zg9jz42wc9zqgqm0g0mjc9ckvh")))) + (base32 "0jiw8pa6hfh9ajr953q187qgpdnk3bvaa3wmrxs8ilw5jc41sq8y")))) (build-system pyproject-build-system) (arguments `(#:phases (modify-phases %standard-phases