smtbmc: Force nonincremental mode when yices is used with forall

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 14feec30d156e3e62dad45c39d0f0559df6fbad3..3d8a51d8b5c33ea45f1f859029bca5ac5af7cf46 100644 (file)
--- 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