diff --git a/Generated/erc20shim/ERC20Shim/fun__transfer_user.lean b/Generated/erc20shim/ERC20Shim/fun__transfer_user.lean
index d0b2252..83a942e 100644
--- a/Generated/erc20shim/ERC20Shim/fun__transfer_user.lean
+++ b/Generated/erc20shim/ERC20Shim/fun__transfer_user.lean
@@ -40,7 +40,7 @@ def A_fun__transfer  (var_from var_to var_value : Literal) (s₀ s₉ : State) :
     ∨
     -- Case: _transfer fails
     (
-      IsERC20 erc20 s₉ ∧ preservesEvm s₀ s₉ ∧
+      IsERC20 erc20 s₉ ∧ preservesEvm s₀ s₉ ∧ s₉.evm.hash_collision = false ∧
       (from_addr = 0 ∨ to_addr = 0)
     )
     -- Case: Hash collision
diff --git a/Generated/erc20shim/ERC20Shim/fun_spendAllowance_user.lean b/Generated/erc20shim/ERC20Shim/fun_spendAllowance_user.lean
index 5b059dc..55a44ee 100644
--- a/Generated/erc20shim/ERC20Shim/fun_spendAllowance_user.lean
+++ b/Generated/erc20shim/ERC20Shim/fun_spendAllowance_user.lean
@@ -35,7 +35,7 @@ def A_fun_spendAllowance  (var_owner var_spender var_value : Literal) (s₀ s₉
     ∨
     -- Case: spendAllowance fails
     (
-      IsERC20 erc20 s₉ ∧ preservesEvm s₀ s₉ ∧
+      IsERC20 erc20 s₉ ∧ preservesEvm s₀ s₉ ∧ s₉.evm.hash_collision = false ∧
       currentAllowance < transfer_value
     )
     -- Case: Hash collision
diff --git a/Generated/erc20shim/ERC20Shim/fun_transferFrom_user.lean b/Generated/erc20shim/ERC20Shim/fun_transferFrom_user.lean
index b684a73..bdee7b9 100644
--- a/Generated/erc20shim/ERC20Shim/fun_transferFrom_user.lean
+++ b/Generated/erc20shim/ERC20Shim/fun_transferFrom_user.lean
@@ -47,7 +47,7 @@ def A_fun_transferFrom (var : Identifier) (var_from var_to var_value : Literal)
     ∨
     -- Case: transferFrom fails
     (
-      IsERC20 erc20 s₉ ∧ preservesEvm s₀ s₉ ∧
+      IsERC20 erc20 s₉ ∧ preservesEvm s₀ s₉ ∧ s₉.evm.hash_collision = false ∧
       s₉[var]!! = 0
     )
     -- Case: Hash collision