projects
/
ieee754fpu.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
55da2d5
)
Use z3 solver instead of yices2 when convenient
author
Cesar Strauss
<cestrauss@gmail.com>
Sat, 23 Jan 2021 09:55:03 +0000
(06:55 -0300)
committer
Cesar Strauss
<cestrauss@gmail.com>
Sat, 23 Jan 2021 09:55:03 +0000
(06:55 -0300)
src/ieee754/part/formal/proof_partition.py
patch
|
blob
|
history
diff --git
a/src/ieee754/part/formal/proof_partition.py
b/src/ieee754/part/formal/proof_partition.py
index 6bf39351dcec61ef14a0132d079284c2be6bafdd..fa5d73234ec44536b715ecfdafec426a48673b43 100644
(file)
--- 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()
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 = {
def test_partsig_add(self):
style = {
@@
-677,9
+678,10
@@
class PartitionTestCase(FHDLTestCase):
def op_implies(a, b):
return a.implies(b)
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__':
if __name__ == '__main__':