From: Jacob Lifshay <programmerjake@gmail.com>
Date: Fri, 20 May 2022 08:08:41 +0000 (-0700)
Subject: change smtbmc to correctly handle output of $smtlib2_expr
X-Git-Tag: smtlib2-expr-support-old~2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e33d7a9a1dcbf1a507efc18c3135e71f1af650ca;p=yosys.git

change smtbmc to correctly handle output of $smtlib2_expr
---

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