Catch Z3Exceptions in DependecyPruner

mythril/laser/ethereum/plugins/implementations/dependency_pruner.py

@@ -38,17 +38,28 @@ class DependencyAnnotation(StateAnnotation):
         return result
 
     def get_storage_write_cache(self, iteration: int):
-        if iteration not in self.storage_written:
+        try:
-            self.storage_written[iteration] = []
+            if iteration not in self.storage_written:
+                self.storage_written[iteration] = []
 
-        return self.storage_written[iteration]
+            return self.storage_written[iteration]
+        except Z3Exception:
+            return
 
     def extend_storage_write_cache(self, iteration: int, value: object):
-        if iteration not in self.storage_written:
+        """
-            self.storage_written[iteration] = [value]
+        FIXME: Catching Z3Exceptions here because laser returns BitVec512 symbols on rare occasions.
-        else:
+        This shouldn't actually happen.
-            if value not in self.storage_written[iteration]:
+        """
-                self.storage_written[iteration].append(value)
+
+        try:
+            if iteration not in self.storage_written:
+                self.storage_written[iteration] = [value]
+            else:
+                if value not in self.storage_written[iteration]:
+                    self.storage_written[iteration].append(value)
+        except Z3Exception:
+            return
 
 
 class WSDependencyAnnotation(StateAnnotation):