Merge pull request #851 from ConsenSys/bugfix/846

Put BitVecVals in stack

mythril/laser/ethereum/instructions.py

@@ -371,7 +371,9 @@ class Instruction:
             )
         else:
 
-            state.stack.append(pow(base.value, exponent.value, 2 ** 256))
+            state.stack.append(
+                symbol_factory.BitVecVal(pow(base.value, exponent.value, 2 ** 256), 256)
+            )
 
         return [global_state]
 

mythril/laser/ethereum/state/account.py

@@ -44,7 +44,7 @@ class Storage:
                 except ValueError:
                     pass
         if self.concrete:
-            return 0
+            return symbol_factory.BitVecVal(0, 256)
         self._storage[item] = symbol_factory.BitVecVal(0, 256)
         return self._storage[item]
 

mythril/laser/ethereum/state/memory.py

@@ -29,8 +29,12 @@ class Memory:
         :return: 32 byte word at the specified index
         """
         try:
-            return util.concrete_int_from_bytes(
-                bytes([util.get_concrete_int(b) for b in self[index : index + 32]]), 0
+            return symbol_factory.BitVecVal(
+                util.concrete_int_from_bytes(
+                    bytes([util.get_concrete_int(b) for b in self[index : index + 32]]),
+                    0,
+                ),
+                256,
             )
         except:
             result = simplify(