From 0c5f62f6ffd53c1a65325df0d71046957d94dfd0 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 8 Jun 2022 11:22:17 +0200 Subject: [PATCH] smtbmc: noincr: keep solver running for post check-sat unrolling --- backends/smt2/smtio.py | 9 +++++++-- 1 file 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)": -- 2.30.2