aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
authorJannis Harder <me@jix.one>2022-06-07 13:19:34 +0200
committerGitHub <noreply@github.com>2022-06-07 13:19:34 +0200
commitfe048a48b3e9507b119def1a88a952c94ad600c7 (patch)
tree273e73df241bf38cfcd6636a78f3192ccab1677b /backends
parentd07828b40958c6c2a1d09cf13c9a307c75b855b4 (diff)
parentab9e887dee3c6e173ca0943a4ac8bb55dd9b31b3 (diff)
downloadyosys-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.py5
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