From: Cesar Strauss <cestrauss@gmail.com>
Date: Sat, 23 Jan 2021 09:55:03 +0000 (-0300)
Subject: Use z3 solver instead of yices2 when convenient
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=632a42b327d7e42abf58b66abdcbb336676d8500;p=ieee754fpu.git

Use z3 solver instead of yices2 when convenient
---

diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py
index 6bf39351..fa5d7323 100644
--- a/src/ieee754/part/formal/proof_partition.py
+++ b/src/ieee754/part/formal/proof_partition.py
@@ -587,9 +587,10 @@ class PartitionTestCase(FHDLTestCase):
         def op_xor(obj):
             return obj.xor()
 
-        # 8-bit partitions take a long time, for some reason
-        module = OpDriver(op_xor, nops=1, width=32, mwidth=4)
-        self.assertFormal(module, mode="bmc", depth=1)
+        module = OpDriver(op_xor, nops=1)
+        # yices2 is slow on this test for some reason
+        # use z3 instead
+        self.assertFormal(module, mode="bmc", depth=1, solver="z3")
 
     def test_partsig_add(self):
         style = {
@@ -677,9 +678,10 @@ class PartitionTestCase(FHDLTestCase):
         def op_implies(a, b):
             return a.implies(b)
 
-        # 8 x 8-bit partitions take a long time, for some reason
-        module = OpDriver(op_implies, part_out=False, width=32, mwidth=8)
-        self.assertFormal(module, mode="bmc", depth=1)
+        module = OpDriver(op_implies, part_out=False)
+        # yices2 is slow on this test for some reason
+        # use z3 instead
+        self.assertFormal(module, mode="bmc", depth=1, solver="z3")
 
 
 if __name__ == '__main__':