From 8b604004dae31f7f3120685dd05d16a4bace904a Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 7 Mar 2018 22:54:19 +0100 Subject: [PATCH] Check results of (check-sat) in yosys-smtbmc Signed-off-by: Clifford Wolf --- backends/smt2/smtio.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index f61f3e77e..fed4524ce 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -646,6 +646,8 @@ class SmtIo: sys.stderr.flush() result = self.read() + assert result in ["sat", "unsat"] + if self.debug_file: print("(set-info :status %s)" % result, file=self.debug_file) print("(check-sat)", file=self.debug_file)