smtbmc: Avoid quadratic behavior when scanning s-exprs

The previous implementation for finding the end of a top-level s-expr
exhibited quadratic behavior as it would re-scan the complete input for
the current expression for every new line. For large designs with
trivial properties this could easily take seconds and dominate the
runtime over the actual solving.

This change remembers the current nesting level between lines, avoiding
the re-scanning.

backends/smt2/smtio.py

@@ -245,6 +245,7 @@ class SmtIo:
             self.logic_uf = False
             self.unroll_idcnt = 0
             self.unroll_buffer = ""
+            self.unroll_level = 0
             self.unroll_sorts = set()
             self.unroll_objs = set()
             self.unroll_decls = dict()
@@ -420,14 +421,16 @@ class SmtIo:
                     self.p_close()
 
         if unroll and self.unroll:
+            s = re.sub(r"\|[^|]*\|", "", stmt)
+            self.unroll_level += s.count("(") - s.count(")")
+            if self.unroll_level > 0:
+                self.unroll_buffer += stmt
+                self.unroll_buffer += " "
+                return
+            else:
                 stmt = self.unroll_buffer + stmt
                 self.unroll_buffer = ""
 
-            s = re.sub(r"\|[^|]*\|", "", stmt)
-            if s.count("(") != s.count(")"):
-                self.unroll_buffer = stmt + " "
-                return
-
             s = self.parse(stmt)
 
             if self.recheck and s and s[0].startswith("get-"):