diff options
| author | Jannis Harder <me@jix.one> | 2022-06-03 16:45:23 +0200 |
|---|---|---|
| committer | Jannis Harder <me@jix.one> | 2022-06-03 16:45:23 +0200 |
| commit | ab9e887dee3c6e173ca0943a4ac8bb55dd9b31b3 (patch) | |
| tree | 233f525b4d1b16bcd72ba8cfd58b433748115d80 | |
| parent | d88a5d26b7849e25dceb3854070dd56f9044c7ee (diff) | |
| download | yosys-ab9e887dee3c6e173ca0943a4ac8bb55dd9b31b3.tar.gz yosys-ab9e887dee3c6e173ca0943a4ac8bb55dd9b31b3.tar.bz2 yosys-ab9e887dee3c6e173ca0943a4ac8bb55dd9b31b3.zip | |
smtbmc: Force nonincremental mode when yices is used with forall
| -rw-r--r-- | backends/smt2/smtio.py | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 14feec30d..3d8a51d8b 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -176,7 +176,10 @@ class SmtIo: self.unroll = False if self.solver == "yices": - if self.noincr or self.forall: + if self.forall: + self.noincr = True + + if self.noincr: self.popen_vargs = ['yices-smt2'] + self.solver_opts else: self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts |