diff --git a/config.json b/config.json
index 8552fde8..915aa6bc 100644
--- a/config.json
+++ b/config.json
@@ -8,9 +8,6 @@
     "rules": [
       "./src/storage.k.md",
       "./src/lemmas.k.md"
-    ],
-    "dirty_rules": [
-      "./src/dirty_lemmas.k.md"
     ]
   },
   "implementations": {
diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md
deleted file mode 100644
index 6f1a0338..00000000
--- a/src/dirty_lemmas.k.md
+++ /dev/null
@@ -1,6 +0,0 @@
-```k
-rule chop(((pow112 *Int A) /Int B) *Int X) => ((pow112 *Int A) /Int B) *Int X
-        requires A <Int pow112
-        andBool B >Int 0
-        andBool X <Int pow32
-```
diff --git a/src/lemmas.k.md b/src/lemmas.k.md
index eb538955..2c074a63 100644
--- a/src/lemmas.k.md
+++ b/src/lemmas.k.md
@@ -347,6 +347,20 @@ rule (B |Int (notMaxUInt160 &Int A)) => B
   andBool (#rangeAddress(A) orBool #rangeUInt(256, A))
 ```
 
+## Z3 non-determinism
+
+Sometimes, the result of a Z3 query is non-deterministic. In the case below, Z3
+is sometimes able to deduce that `chop(X) => X`, but other times it isn't.
+
+This lemma ensures that we always drop the `chop`, when the constraints are satisfied.
+
+```k
+rule chop(((pow112 *Int A) /Int B) *Int X) => ((pow112 *Int A) /Int B) *Int X
+        requires A <Int pow112
+        andBool B >Int 0
+        andBool X <Int pow32
+```
+
 ## Packed Words In Memory
 
 Sometimes solidity will try and read a Word from memory containing unaligned data. In that case `K`