From ab9e887dee3c6e173ca0943a4ac8bb55dd9b31b3 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Fri, 3 Jun 2022 16:45:23 +0200
Subject: [PATCH] smtbmc: Force nonincremental mode when yices is used with
 forall

---
 backends/smt2/smtio.py | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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