diff options
author | Jannis Harder <me@jix.one> | 2022-06-07 13:19:34 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2022-06-07 13:19:34 +0200 |
commit | fe048a48b3e9507b119def1a88a952c94ad600c7 (patch) | |
tree | 273e73df241bf38cfcd6636a78f3192ccab1677b /backends | |
parent | d07828b40958c6c2a1d09cf13c9a307c75b855b4 (diff) | |
parent | ab9e887dee3c6e173ca0943a4ac8bb55dd9b31b3 (diff) | |
download | yosys-fe048a48b3e9507b119def1a88a952c94ad600c7.tar.gz yosys-fe048a48b3e9507b119def1a88a952c94ad600c7.tar.bz2 yosys-fe048a48b3e9507b119def1a88a952c94ad600c7.zip |
Merge pull request #3358 from jix/smtbmc-yices-forall
smtbmc: Force nonincremental mode when yices is used with forall
Diffstat (limited to 'backends')
-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 |