mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-27 02:45:52 +00:00
Code Activity

Merge pull request #3358 from jix/smtbmc-yices-forall

Browse source 
smtbmc: Force nonincremental mode when yices is used with forall
This commit is contained in:
Jannis Harder 2022-06-07 13:19:34 +02:00 • committed by GitHub
commit fe048a48b3
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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