1 files changed, 86 insertions, 0 deletions
diff --git a/gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch b/gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch
new file mode 100644
index 0000000000..eee555f807
--- /dev/null
+++ b/gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch
@@ -0,0 +1,86 @@
+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)