From d6f3787fb5f23f9ec361b9bd37f3b3b57a80a135 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Mon, 10 Jun 2019 00:27:15 +0200 Subject: [PATCH] Set parallelism=true --- mythril/analysis/solver.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 98d3633a..4ecfc95e 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -2,7 +2,7 @@ from z3 import sat, unknown, FuncInterp import z3 -from mythril.laser.smt import simplify, UGE, Optimize, symbol_factory +from mythril.laser.smt import UGE, Optimize, symbol_factory from mythril.laser.ethereum.time_handler import time_handler from mythril.exceptions import UnsatError from mythril.laser.ethereum.transaction.transaction_models import ( @@ -12,6 +12,8 @@ import logging log = logging.getLogger(__name__) +z3.set_param('parallel.enable', True) + def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True): """ @@ -23,7 +25,7 @@ def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True :return: """ s = Optimize() - timeout = 100000 + timeout = 10000 if enforce_execution_time: timeout = min(timeout, time_handler.time_remaining() - 500) if timeout <= 0: