From cd5964c5b2ce4b2a4b1b0e32632504a421fca38c Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Wed, 23 Oct 2019 14:47:43 +0200
Subject: [PATCH] implement expression substitution for arrays

---
 mythril/laser/smt/array.py | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/mythril/laser/smt/array.py b/mythril/laser/smt/array.py
index b804b374..18d7ae3f 100644
--- a/mythril/laser/smt/array.py
+++ b/mythril/laser/smt/array.py
@@ -34,6 +34,13 @@ class BaseArray:
     def __eq__(self, other: "BaseArray"):
         return Bool(self.raw == other.raw)
 
+    def substitute(self, original_expression: "BaseArray", new_expression: "BaseArray"):
+        if self.raw is None:
+            return
+        original_z3 = original_expression.raw
+        new_z3 = new_expression.raw
+        self.raw = z3.substitute(self.raw, (original_z3, new_z3))
+
 
 class Array(BaseArray):
     """A basic symbolic array."""