From e97f10b14249a412d3a97d899f6e2a8685fbcdcf Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 29 Jan 2018 12:34:28 +0100 Subject: [PATCH] Fix smtio.py for large SMT2 S-expressions --- backends/smt2/smtio.py | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index a9d9de8fa..07bd92265 100644 --- 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", -- 2.30.2