Add a execution-time require checker flag

mythril/analysis/solver.py

@@ -13,18 +13,21 @@ import logging
 log = logging.getLogger(__name__)
 
 
-def get_model(constraints, minimize=(), maximize=()):
+def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True):
     """
 
     :param constraints:
     :param minimize:
     :param maximize:
+    :param enforce_execution_time: Bool variable which enforces --execution-timeout's time
     :return:
     """
     s = Optimize()
-    timeout = min(100000, time_handler.time_remaining() - 500)
-    if timeout <= 0:
-        raise UnsatError
+    timeout = 100000
+    if enforce_execution_time:
+        timeout = min(timeout, time_handler.time_remaining() - 500)
+        if timeout <= 0:
+            raise UnsatError
     s.set_timeout(timeout)
     for constraint in constraints:
         if type(constraint) == bool and not constraint:

tests/laser/evm_testsuite/evm_test.py

@@ -127,7 +127,8 @@ def test_vmtest(
         assert len(laser_evm.open_states) == 1
         world_state = laser_evm.open_states[0]
         model = get_model(
-            next(iter(laser_evm.nodes.values())).states[0].mstate.constraints
+            next(iter(laser_evm.nodes.values())).states[0].mstate.constraints,
+            enforce_execution_time=False,
         )
 
         for address, details in post_condition.items():