Fix smtio.py for large SMT2 S-expressions

This commit is contained in:
Clifford Wolf 2018-01-29 12:34:28 +01:00
parent 675f53abbb
commit e97f10b142
1 changed files with 12 additions and 1 deletions

View File

@ -16,7 +16,8 @@
# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. # 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 copy import deepcopy
from select import select from select import select
from time import time from time import time
@ -24,6 +25,16 @@ from queue import Queue, Empty
from threading import Thread 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 = { hex_dict = {
"0": "0000", "1": "0001", "2": "0010", "3": "0011", "0": "0000", "1": "0001", "2": "0010", "3": "0011",
"4": "0100", "5": "0101", "6": "0110", "7": "0111", "4": "0100", "5": "0101", "6": "0110", "7": "0111",