Fix smtio.py for large SMT2 S-expressions

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index a9d9de8fa7ea95edcd85c6925dde1547c96b4cc0..07bd92265afa64125350c1a758624febc27d7dd8 100644 (file)
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -16,7 +16,8 @@
 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 #
 
-import sys, subprocess, re, os
+import sys, re, os
+import resource, subprocess
 from copy import deepcopy
 from select import select
 from time import time
@@ -24,6 +25,16 @@ from queue import Queue, Empty
 from threading import Thread
 
 
+# This is needed so that the recursive SMT2 S-expression parser
+# does not run out of stack frames when parsing large expressions
+smtio_reclimit = 64 * 1024
+smtio_stacksize = 128 * 1024 * 1024
+if sys.getrecursionlimit() < smtio_reclimit:
+    sys.setrecursionlimit(smtio_reclimit)
+if resource.getrlimit(resource.RLIMIT_STACK)[0] < smtio_stacksize:
+    resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, -1))
+
+
 hex_dict = {
     "0": "0000", "1": "0001", "2": "0010", "3": "0011",
     "4": "0100", "5": "0101", "6": "0110", "7": "0111",