Merge branch 'develop' into fixed_tx_count

mythril/laser/ethereum/instructions.py

@@ -13,6 +13,7 @@ from z3 import (
     Concat,
     ULT,
     UGT,
+    BitVecRef,
     BitVecNumRef,
     Not,
     is_false,
@@ -83,6 +84,13 @@ class StateTransition(object):
     @staticmethod
     def check_gas_usage_limit(global_state: GlobalState):
         global_state.mstate.check_gas()
+        if isinstance(global_state.current_transaction.gas_limit, BitVecRef):
+            try:
+                global_state.current_transaction.gas_limit = (
+                    global_state.current_transaction.gas_limit.as_long()
+                )
+            except AttributeError:
+                return
         if (
             global_state.mstate.min_gas_used
             >= global_state.current_transaction.gas_limit
@@ -1139,6 +1147,7 @@ class Instruction:
 
     @StateTransition()
     def gas_(self, global_state: GlobalState) -> List[GlobalState]:
+        # TODO: Push a Constrained variable which lies between min gas and max gas
         global_state.mstate.stack.append(global_state.new_bitvec("gas", 256))
         return [global_state]