Make some changes

mythril/laser/ethereum/plugins/implementations/state_merge/__init__.py

@@ -16,13 +16,12 @@ log = logging.getLogger(__name__)
 
 
 class MergeAnnotation(StateAnnotation):
-    def __init__(self):
-        pass
+    pass
 
 
 class StateMerge(LaserPlugin):
     def initialize(self, symbolic_vm: LaserEVM):
-        """Initializes the mutation pruner
+        """Initializes the State merging plugin
 
         Introduces hooks for SSTORE operations
         :param symbolic_vm:

mythril/laser/ethereum/plugins/implementations/state_merge/merge_states.py

@@ -97,7 +97,7 @@ def merge_storage(storage1: Storage, storage2: Storage, path_condition: Bool):
                 path_condition, storage1.printable_storage[key], value
             )
         else:
-            storage1.printable_storage[key] = value
+            storage1.printable_storage[key] = If(path_condition, 0, value)
 
 
 def _merge_annotations(state1: "WorldState", state2: "WorldState"):

mythril/laser/smt/bitvec_helper.py

@@ -47,9 +47,7 @@ def If(
     """
     if not isinstance(a, Bool):
         a = Bool(z3.BoolVal(a))
-    if (isinstance(b, K) or isinstance(b, Array)) and (
-        isinstance(c, Array) or isinstance(c, K)
-    ):
+    if isinstance(b, BaseArray) and isinstance(c, BaseArray):
         array = z3.If(a.raw, b.raw, c.raw)
         return z3_array_converter(array)