riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #2282 from YosysHQ/claire/satunsat 

Only allow "sat" and "unsat" smt solver responses in yosys-smtbmc
This commit is contained in:
clairexen 2020-07-20 23:06:36 +02:00 committed by GitHub
parent 3cb401db8c a207cb362c
commit 856d40973d
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
backends/smt2/smtbmc.py
View File

@ -1275,10 +1275,10 @@ def smt_pop():
asserts_consequent_cache.pop() asserts_consequent_cache.pop()
smt.write("(pop 1)") smt.write("(pop 1)")
def smt_check_sat(): def smt_check_sat(expected=["sat", "unsat"]):
if asserts_cache_dirty: if asserts_cache_dirty:
smt_forall_assert() smt_forall_assert()
return smt.check_sat() return smt.check_sat(expected=expected)
if tempind: if tempind:
retstatus = "FAILED" retstatus = "FAILED"

4
backends/smt2/smtio.py
View File

@ -653,7 +653,7 @@ class SmtIo:
return stmt return stmt
def check_sat(self): def check_sat(self, expected=["sat", "unsat", "unknown", "timeout", "interrupted"]):
if self.debug_print: if self.debug_print:
print("> (check-sat)") print("> (check-sat)")
if self.debug_file and not self.nocomments: if self.debug_file and not self.nocomments:
@ -740,7 +740,7 @@ class SmtIo:
print("(check-sat)", file=self.debug_file) print("(check-sat)", file=self.debug_file)
self.debug_file.flush() self.debug_file.flush()
if result not in ["sat", "unsat", "unknown", "timeout", "interrupted"]: if result not in expected:
if result == "": if result == "":
print("%s Unexpected EOF response from solver." % (self.timestamp()), flush=True) print("%s Unexpected EOF response from solver." % (self.timestamp()), flush=True)
else: else: