Fix the graph tests

mythril/laser/ethereum/instructions.py

@@ -1596,9 +1596,13 @@ class Instruction:
         """
         state = global_state.mstate
         offset, length = state.stack.pop(), state.stack.pop()
-        state.mem_extend(offset, length)
-        StateTransition.check_gas_usage_limit(global_state)
-        return_data = state.memory[offset : offset + length]
+        if length.symbolic:
+            return_data = [global_state.new_bitvec("return_data", 8)]
+            log.debug("Return with symbolic length or offset. Not supported")
+        else:
+            state.mem_extend(offset, length)
+            StateTransition.check_gas_usage_limit(global_state)
+            return_data = state.memory[offset : offset + length]
         global_state.current_transaction.end(global_state, return_data)
 
     @StateTransition()

mythril/laser/ethereum/state/memory.py

@@ -137,7 +137,7 @@ class Memory:
             start, stop, step = convert_bv(start), convert_bv(stop), convert_bv(step)
             ret_lis = []
             itr = symbol_factory.BitVecVal(0, 256)
-            while simplify(start + itr != stop) and itr <= 10000000:
+            while simplify(start + itr < stop) and itr <= 10000000:
                 ret_lis.append(self[start + step * itr])
                 itr += 1
 
@@ -170,7 +170,7 @@ class Memory:
             assert type(value) == list
             start, stop, step = convert_bv(start), convert_bv(stop), convert_bv(step)
             itr = symbol_factory.BitVecVal(0, 256)
-            while simplify(start + itr != stop) and itr <= 10000000:
+            while simplify(start + itr < stop) and itr <= 10000000:
                 self[start + itr] = value[itr.value]
                 itr += 1