smtbmc: Avoid unnecessary string copies when parsing solver output

1 files changed, 9 insertions, 12 deletions

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index de09c040e..9af454cca 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -847,31 +847,28 @@ class SmtIo:
         return result
 
     def parse(self, stmt):
-        def worker(stmt):
-            if stmt[0] == '(':
+        def worker(stmt, cursor=0):
+            while stmt[cursor] in [" ", "\t", "\r", "\n"]:
+                cursor += 1
+
+            if stmt[cursor] == '(':
                 expr = []
-                cursor = 1
+                cursor += 1
                 while stmt[cursor] != ')':
-                    el, le = worker(stmt[cursor:])
+                    el, cursor = worker(stmt, cursor)
                     expr.append(el)
-                    cursor += le
                 return expr, cursor+1
 
-            if stmt[0] == '|':
+            if stmt[cursor] == '|':
                 expr = "|"
-                cursor = 1
+                cursor += 1
                 while stmt[cursor] != '|':
                     expr += stmt[cursor]
                     cursor += 1
                 expr += "|"
                 return expr, cursor+1
 
-            if stmt[0] in [" ", "\t", "\r", "\n"]:
-                el, le = worker(stmt[1:])
-                return el, le+1
-
             expr = ""
-            cursor = 0
             while stmt[cursor] not in ["(", ")", "|", " ", "\t", "\r", "\n"]:
                 expr += stmt[cursor]
                 cursor += 1