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