From 385d05db8e578207ca276426670fc0cc305d6292 Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Sun, 18 Nov 2018 15:25:15 +0530
Subject: [PATCH 1/4] Do not compare variables in gas check

---
 mythril/laser/ethereum/instructions.py | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index c7dddc9b..09df96e2 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -13,6 +13,7 @@ from z3 import (
     Concat,
     ULT,
     UGT,
+    BitVecRef,
     BitVecNumRef,
     Not,
     is_false,
@@ -83,6 +84,8 @@ class StateTransition(object):
     @staticmethod
     def check_gas_usage_limit(global_state: GlobalState):
         global_state.mstate.check_gas()
+        if type(global_state.current_transaction.gas_limit) == BitVecRef:
+            return
         if (
             global_state.mstate.min_gas_used
             >= global_state.current_transaction.gas_limit
@@ -1139,6 +1142,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]
 
@@ -1491,7 +1495,7 @@ class Instruction:
                 global_state.new_bitvec("retval_" + str(instr["address"]), 256)
             )
             return [global_state]
-
+        
         transaction = MessageCallTransaction(
             world_state=global_state.world_state,
             gas_price=environment.gasprice,

From e70f099599edd670e63fdaf8bc59032c8ce28d37 Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Sun, 18 Nov 2018 15:34:41 +0530
Subject: [PATCH 2/4] reformat instructions.py with black

---
 mythril/laser/ethereum/instructions.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index 09df96e2..47ec3f1d 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -1495,7 +1495,7 @@ class Instruction:
                 global_state.new_bitvec("retval_" + str(instr["address"]), 256)
             )
             return [global_state]
-        
+
         transaction = MessageCallTransaction(
             world_state=global_state.world_state,
             gas_price=environment.gasprice,

From bc63040602a486385482d67ce7d7cb19c6b7ad3a Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Sun, 18 Nov 2018 20:12:10 +0530
Subject: [PATCH 3/4] Add isinstance and get value from BitVecNums()

---
 mythril/laser/ethereum/instructions.py | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index 47ec3f1d..19a8b29a 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -84,8 +84,11 @@ class StateTransition(object):
     @staticmethod
     def check_gas_usage_limit(global_state: GlobalState):
         global_state.mstate.check_gas()
-        if type(global_state.current_transaction.gas_limit) == BitVecRef:
-            return
+        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

From d808e8544fa84183378f2000901be1f706da4700 Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Sun, 18 Nov 2018 20:13:09 +0530
Subject: [PATCH 4/4] Reformat file with black

---
 mythril/laser/ethereum/instructions.py | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index 19a8b29a..4cbc06c5 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -86,7 +86,9 @@ class StateTransition(object):
         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()
+                global_state.current_transaction.gas_limit = (
+                    global_state.current_transaction.gas_limit.as_long()
+                )
             except AttributeError:
                 return
         if (