Merge pull request #3357 from jix/smtbmc-cvc5

smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5

1 files changed, 13 insertions, 3 deletions

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 3d8a51d8b..64e4cd79a 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -123,6 +123,7 @@ class SmtIo:
         self.forall = False
         self.timeout = 0
         self.produce_models = True
+        self.recheck = False
         self.smt2cache = [list()]
         self.smt2_options = dict()
         self.p = None
@@ -192,11 +193,12 @@ class SmtIo:
             if self.timeout != 0:
                 self.popen_vargs.append('-T:%d' % self.timeout);
 
-        if self.solver == "cvc4":
+        if self.solver in ["cvc4", "cvc5"]:
+            self.recheck = True
             if self.noincr:
-                self.popen_vargs = ['cvc4', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
+                self.popen_vargs = [self.solver, '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
             else:
-                self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
+                self.popen_vargs = [self.solver, '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
             if self.timeout != 0:
                 self.popen_vargs.append('--tlimit=%d000' % self.timeout);
 
@@ -407,6 +409,8 @@ class SmtIo:
             stmt = re.sub(r" *;.*", "", stmt)
             if stmt == "": return
 
+        recheck = None
+
         if unroll and self.unroll:
             stmt = self.unroll_buffer + stmt
             self.unroll_buffer = ""
@@ -418,6 +422,9 @@ class SmtIo:
 
             s = self.parse(stmt)
 
+            if self.recheck and s and s[0].startswith("get-"):
+                recheck = self.unroll_idcnt
+
             if self.debug_print:
                 print("-> %s" % s)
 
@@ -443,6 +450,9 @@ class SmtIo:
 
             stmt = self.unparse(self.unroll_stmt(s))
 
+            if recheck is not None and recheck != self.unroll_idcnt:
+                self.check_sat(["sat"])
+
             if stmt == "(push 1)":
                 self.unroll_stack.append((
                     copy(self.unroll_sorts),