diff options
Diffstat (limited to 'backends/smt2')
| -rw-r--r-- | backends/smt2/smtio.py | 36 | 
1 files 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:  | 
