From 7640bce61ffdbeff8692c96bf7870dc80ffe427a Mon Sep 17 00:00:00 2001
From: Jacob Lifshay <programmerjake@gmail.com>
Date: Fri, 20 May 2022 01:08:41 -0700
Subject: [PATCH] change smtbmc to correctly handle output of $smtlib2_expr

(cherry picked from commit e33d7a9a1dcbf1a507efc18c3135e71f1af650ca)
---
 backends/smt2/smtio.py | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index d73a875ba..086d1cb7b 100644
--- 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
-- 
2.30.2