add option for z3 parallelising (#1372)

mythril/interfaces/cli.py

@@ -445,6 +445,11 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser):
         default=10,
         help="The amount of seconds to spend on the initial contract creation",
     )
+    options.add_argument(
+        "--parallel-solving",
+        action="store_true",
+        help="Enable solving z3 queries in parallel",
+    )
     options.add_argument(
         "--no-onchain-data",
         action="store_true",
@@ -684,6 +689,7 @@ def execute_command(
             disable_dependency_pruning=args.disable_dependency_pruning,
             use_onchain_data=not args.no_onchain_data,
             solver_timeout=args.solver_timeout,
+            parallel_solving=args.parallel_solving,
             enable_coverage_strategy=args.enable_coverage_strategy,
             custom_modules_directory=args.custom_modules_directory
             if args.custom_modules_directory

mythril/laser/smt/solver/__init__.py

@@ -1,3 +1,9 @@
+import z3
+
 from mythril.laser.smt.solver.solver import Solver, Optimize, BaseSolver
 from mythril.laser.smt.solver.independence_solver import IndependenceSolver
 from mythril.laser.smt.solver.solver_statistics import SolverStatistics
+from mythril.support.support_args import args
+
+if args.parallel_solving:
+    z3.set_param("parallel.enable", True)

mythril/mythril/mythril_analyzer.py

@@ -47,6 +47,7 @@ class MythrilAnalyzer:
         custom_modules_directory: str = "",
         sparse_pruning: bool = False,
         unconstrained_storage: bool = False,
+        parallel_solving: bool = False,
     ):
         """
 
@@ -70,6 +71,7 @@ class MythrilAnalyzer:
         self.custom_modules_directory = custom_modules_directory
         args.sparse_pruning = sparse_pruning
         args.solver_timeout = solver_timeout
+        args.parallel_solving = parallel_solving
         args.unconstrained_storage = unconstrained_storage
 
     def dump_statespace(self, contract: EVMContract = None) -> str:

mythril/support/support_args.py

@@ -8,6 +8,7 @@ class Args:
         self.solver_timeout = 10000
         self.sparse_pruning = True
         self.unconstrained_storage = False
+        self.parallel_solving = False
 
 
 args = Args()