aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
authorJannis Harder <me@jix.one>2022-06-08 11:22:17 +0200
committerJannis Harder <me@jix.one>2022-06-08 13:20:25 +0200
commit0c5f62f6ffd53c1a65325df0d71046957d94dfd0 (patch)
tree38a37df67c16cba7b1e1f422b2f37b0875ec9a6d /backends
parent6db29489386ce749d08c67547eb1b8acc16f8e5c (diff)
downloadyosys-0c5f62f6ffd53c1a65325df0d71046957d94dfd0.tar.gz
yosys-0c5f62f6ffd53c1a65325df0d71046957d94dfd0.tar.bz2
yosys-0c5f62f6ffd53c1a65325df0d71046957d94dfd0.zip
smtbmc: noincr: keep solver running for post check-sat unrolling
Diffstat (limited to 'backends')
-rw-r--r--backends/smt2/smtio.py9
1 files changed, 7 insertions, 2 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 64e4cd79a..91efc13a3 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -411,6 +411,13 @@ class SmtIo:
recheck = None
+ if self.solver != "dummy":
+ if self.noincr:
+ # Don't close the solver yet, if we're just unrolling definitions
+ # required for a (get-...) statement
+ if self.p is not None and not stmt.startswith("(get-") and unroll:
+ self.p_close()
+
if unroll and self.unroll:
stmt = self.unroll_buffer + stmt
self.unroll_buffer = ""
@@ -473,8 +480,6 @@ class SmtIo:
if self.solver != "dummy":
if self.noincr:
- if self.p is not None and not stmt.startswith("(get-"):
- self.p_close()
if stmt == "(push 1)":
self.smt2cache.append(list())
elif stmt == "(pop 1)":