From: Jannis Harder <me@jix.one>
Date: Fri, 3 Jun 2022 14:45:23 +0000 (+0200)
Subject: smtbmc: Force nonincremental mode when yices is used with forall
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ab9e887dee3c6e173ca0943a4ac8bb55dd9b31b3;p=yosys.git

smtbmc: Force nonincremental mode when yices is used with forall
---

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