diff --git a/algorithm-correctness/deposit-symbolic.k b/algorithm-correctness/deposit-symbolic.k
index 3b52247..7f334d1 100644
--- a/algorithm-correctness/deposit-symbolic.k
+++ b/algorithm-correctness/deposit-symbolic.k
@@ -18,21 +18,26 @@ rule tn(M, 0, I) => 0  requires I >Int M
    andBool isNat(M) andBool isNat(I)
 // andBool M <=Int 2 ^Int TREE_HEIGHT
 // andBool I <=Int 2 ^Int TREE_HEIGHT
+[simplification]
 
 /*
  * By Equations 1 and 2. (\ref{eq:def:up}, \ref{eq:def:down})
  */
 rule up(0, M) => M  requires true
    andBool isNat(M)
+[simplification]
 
 rule down(0, M) => M  requires true
    andBool isNat(M)
+[simplification]
 
 rule down(K, M) /Int 2 => down(K +Int 1, M)  requires true
    andBool isNat(K) andBool isNat(M)
+[simplification]
 
 rule up(H, M) => 1  requires M <=Int 2 ^Int H
    andBool isNat(H) andBool isNat(M)
+[simplification]
 
 /*
  * Lemma 8 (Contract Invariant).
@@ -61,6 +66,7 @@ rule hash(Branch[K], tn(M, K, up(K, M +Int 1))) => tn(M, K +Int 1, up(K +Int 1,
       andBool isNat(K) andBool isNat(M)
 //    andBool K <Int TREE_HEIGHT
 //    andBool M <Int 2 ^Int TREE_HEIGHT
+[simplification]
 
 /*
  * By Lemmas 3 and 8. (\ref{lem:zero}, \ref{lem:contract-invariant})
@@ -71,6 +77,7 @@ rule hash(tn(M, K, up(K, M +Int 1)), Zeros[K])  => tn(M, K +Int 1, up(K +Int 1,
       andBool isNat(K) andBool isNat(M)
 //    andBool K <Int TREE_HEIGHT
 //    andBool M <Int 2 ^Int TREE_HEIGHT
+[simplification]
 
 // Proof of Lemma 7 (deposit)
 
@@ -86,6 +93,7 @@ rule hash(Branch[I], tn(M, I, down(I, M))) => tn(M, I +Int 1, down(I +Int 1, M))
       andBool isNat(I) andBool isNat(M)
 //    andBool I <Int TREE_HEIGHT
 //    andBool M <Int 2 ^Int TREE_HEIGHT
+[simplification]
 
 /*
  * By Lemma 5. (\ref{lem:two-chains})
@@ -97,6 +105,7 @@ rule isValidBranch(B[I <- tn(M, I, down(I, M))], M) => true
       andBool isNat(I) andBool isNat(M)
 //    andBool I <Int TREE_HEIGHT
 //    andBool M <Int 2 ^Int TREE_HEIGHT
+[simplification]
 
 rule isValidBranch(B[I <- tn(M, I, down(I, M))], M) => true
      requires isValidBranch(B, M -Int 1)
@@ -105,11 +114,13 @@ rule isValidBranch(B[I <- tn(M, I, down(I, M))], M) => true
       andBool isNat(I) andBool isNat(M)
 //    andBool I <Int TREE_HEIGHT
 //    andBool M <Int 2 ^Int TREE_HEIGHT
+[simplification]
 
 //rule down(K, M) => 1
 //     requires M <Int 2 ^Int (K +Int 1)
 //      andBool (2 ^Int K) *Int down(K, M) ==Int M
 //      andBool M >Int 0
+//[simplification]
 
 /*
  * By Equation 2. (\ref{eq:def:down})
@@ -120,5 +131,6 @@ rule (2 ^Int (I +Int 1)) *Int down(I +Int 1, M) => M
       andBool isNat(I) andBool isNat(M)
 //    andBool I <Int TREE_HEIGHT
 //    andBool M <Int 2 ^Int TREE_HEIGHT
+[simplification]
 
 endmodule
diff --git a/algorithm-correctness/imap.k b/algorithm-correctness/imap.k
index 7aef5e6..a2708ba 100644
--- a/algorithm-correctness/imap.k
+++ b/algorithm-correctness/imap.k
@@ -8,8 +8,8 @@ endmodule
 
 module IMAP-SYMBOLIC [symbolic]
     imports IMAP-SYNTAX
-    rule M [ K0 <- V ] [ K ] => V       requires K0  ==Int K
-    rule M [ K0 <- V ] [ K ] => M [ K ] requires K0 =/=Int K
+    rule M [ K0 <- V ] [ K ] => V       requires K0  ==Int K [simplification]
+    rule M [ K0 <- V ] [ K ] => M [ K ] requires K0 =/=Int K [simplification]
 //  rule .IMap [ _ ] => 0
 
 // syntax IntMap
diff --git a/deps/evm-semantics b/deps/evm-semantics
index 5da8519..b2c5c71 160000
--- a/deps/evm-semantics
+++ b/deps/evm-semantics
@@ -1 +1 @@
-Subproject commit 5da85195e74ca4e416e4e8218017be289af24e3a
+Subproject commit b2c5c7190f0a4a2774b66f3c56de391f7b4bebb2