From a207cb362cc4b682a37060f380362b23c927805e Mon Sep 17 00:00:00 2001 From: Claire Wolf Date: Mon, 20 Jul 2020 19:35:32 +0200 Subject: Only allow "sat" and "unsat" smt solver responses in yosys-smtbmc Signed-off-by: Claire Wolf --- backends/smt2/smtbmc.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backends/smt2/smtbmc.py') 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" -- cgit v1.2.3