cerc-io/solidity
11
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Add CI job for optimization proofs

Browse Source
This commit is contained in:
Leonardo Alt
2019-06-19 22:29:23 +02:00
parent fc64de6d90
commit 51ba7f5f17
3 changed files with 58 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files
test/formal/rule.py
+10 -4
View File
@@ -1,3 +1,5 @@
import sys
from z3 import *
class Rule:
@@ -21,9 +23,9 @@ class Rule:
result = self.solver.check()
if result == unknown:
raise BaseException('Unable to satisfy requirements.')
self.error('Unable to satisfy requirements.')
elif result == unsat:
raise BaseException('Requirements are unsatisfiable.')
self.error('Requirements are unsatisfiable.')
self.solver.push()
self.solver.add(self.constraints)
@@ -31,8 +33,12 @@ class Rule:
result = self.solver.check()
if result == unknown:
raise BaseException('Unable to prove rule.')
self.error('Unable to prove rule.')
elif result == sat:
m = self.solver.model()
raise BaseException('Rule is incorrect.\nModel: ' + str(m))
self.error('Rule is incorrect.\nModel: ' + str(m))
self.solver.pop()
def error(self, msg):
print(msg)
sys.exit(1)