From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 8 May 2017 12:33:22 +0000 (+0200)
Subject: Fix boolector support in yosys-smtbmc
X-Git-Tag: yosys-0.8~442
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1a4b7c6bfa715cfa6fbd92a91b3cc017931c0495;p=yosys.git

Fix boolector support in yosys-smtbmc
---

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 14ee787f6..50ed8c01d 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -83,16 +83,6 @@ class SmtIo:
             self.info_stmts = list()
             self.nocomments = False
 
-        if self.unroll:
-            self.logic_uf = False
-            self.unroll_idcnt = 0
-            self.unroll_buffer = ""
-            self.unroll_sorts = set()
-            self.unroll_objs = set()
-            self.unroll_decls = dict()
-            self.unroll_cache = dict()
-            self.unroll_stack = list()
-
         self.start_time = time()
 
         self.modinfo = dict()
@@ -103,14 +93,6 @@ class SmtIo:
     def setup(self):
         assert not self.setup_done
 
-        if self.logic is None:
-            self.logic = ""
-            if self.logic_qf: self.logic += "QF_"
-            if self.logic_ax: self.logic += "A"
-            if self.logic_uf: self.logic += "UF"
-            if self.logic_bv: self.logic += "BV"
-            if self.logic_dt: self.logic = "ALL"
-
         if self.solver == "yices":
             self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
 
@@ -145,6 +127,24 @@ class SmtIo:
             if not self.noincr:
                 self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
 
+        if self.unroll:
+            self.logic_uf = False
+            self.unroll_idcnt = 0
+            self.unroll_buffer = ""
+            self.unroll_sorts = set()
+            self.unroll_objs = set()
+            self.unroll_decls = dict()
+            self.unroll_cache = dict()
+            self.unroll_stack = list()
+
+        if self.logic is None:
+            self.logic = ""
+            if self.logic_qf: self.logic += "QF_"
+            if self.logic_ax: self.logic += "A"
+            if self.logic_uf: self.logic += "UF"
+            if self.logic_bv: self.logic += "BV"
+            if self.logic_dt: self.logic = "ALL"
+
         self.setup_done = True
 
         if self.produce_models: