From 1a4b7c6bfa715cfa6fbd92a91b3cc017931c0495 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 8 May 2017 14:33:22 +0200
Subject: Fix boolector support in yosys-smtbmc
---
backends/smt2/smtio.py | 36 ++++++++++++++++++------------------
1 file changed, 18 insertions(+), 18 deletions(-)
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:
--
cgit v1.2.3