diff options
| author | clairexen <claire@symbioticeda.com> | 2020-07-20 23:06:36 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-20 23:06:36 +0200 |
| commit | 856d40973dce06e13fcded3388562341d82c092d (patch) | |
| tree | 9431daaaf82f2d862e229f4190bea0506ba07735 | |
| parent | 3cb401db8c77035e88163b0d5d46f51a9510db77 (diff) | |
| parent | a207cb362cc4b682a37060f380362b23c927805e (diff) | |
| download | yosys-856d40973dce06e13fcded3388562341d82c092d.tar.gz yosys-856d40973dce06e13fcded3388562341d82c092d.tar.bz2 yosys-856d40973dce06e13fcded3388562341d82c092d.zip | |
Merge pull request #2282 from YosysHQ/claire/satunsat
Only allow "sat" and "unsat" smt solver responses in yosys-smtbmc
| -rw-r--r-- | backends/smt2/smtbmc.py | 4 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 03f001bfd..69dab5590 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -1275,10 +1275,10 @@ def smt_pop(): asserts_consequent_cache.pop() smt.write("(pop 1)") -def smt_check_sat(): +def smt_check_sat(expected=["sat", "unsat"]): if asserts_cache_dirty: smt_forall_assert() - return smt.check_sat() + return smt.check_sat(expected=expected) if tempind: retstatus = "FAILED" diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 72ab39d39..4ac437c36 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -653,7 +653,7 @@ class SmtIo: return stmt - def check_sat(self): + def check_sat(self, expected=["sat", "unsat", "unknown", "timeout", "interrupted"]): if self.debug_print: print("> (check-sat)") if self.debug_file and not self.nocomments: @@ -740,7 +740,7 @@ class SmtIo: print("(check-sat)", file=self.debug_file) self.debug_file.flush() - if result not in ["sat", "unsat", "unknown", "timeout", "interrupted"]: + if result not in expected: if result == "": print("%s Unexpected EOF response from solver." % (self.timestamp()), flush=True) else: |