change smtbmc to correctly handle output of $smtlib2_expr

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 14feec30d156e3e62dad45c39d0f0559df6fbad3..5c951766a04f6574e8b93495659057da955da33f 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