change smtbmc to correctly handle output of $smtlib2_expr

(cherry picked from commit e33d7a9a1dcbf1a507efc18c3135e71f1af650ca)

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index d73a875ba4c116e164d90c782098b2e23b56025f..086d1cb7bf8de1b40798c73fe70ba4da155ca4e2 100644 (file)
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -434,6 +434,8 @@ class SmtIo:
 
             elif len(s) >= 4 and s[0] == "define-fun":
                 for arg_name, arg_sort in s[2]:
+                    if isinstance(arg_sort, list):
+                        break
                     if arg_sort in self.unroll_sorts:
                         self.unroll_decls[s[1]] = s
                         return