github.com/YosysHQ.yosys
1
0
Fork 0
mirror of synced 2026-02-11 02:49:49 +00:00
Code Issues Releases Wiki Activity

smtbmc: Force nonincremental mode when yices is used with forall

Browse Source
This commit is contained in:
Jannis Harder
2022-06-03 16:45:23 +02:00
parent d88a5d26b7
commit ab9e887dee
1 changed files with 4 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
backends/smt2/smtio.py
View File

@@ -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