From: Jannis Harder <me@jix.one>
Date: Wed, 8 Jun 2022 09:22:17 +0000 (+0200)
Subject: smtbmc: noincr: keep solver running for post check-sat unrolling
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0c5f62f6ffd53c1a65325df0d71046957d94dfd0;p=yosys.git

smtbmc: noincr: keep solver running for post check-sat unrolling
---

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)":