From 6ef464441e96ffc2537e006490ac234e256b2e74 Mon Sep 17 00:00:00 2001
From: Lorenzo Manacorda <lorenzo@mailbox.org>
Date: Tue, 14 Apr 2020 11:37:52 +0200
Subject: [PATCH] src/lemmas.k.md: fix TIME rule

rangeUInt(224, pow224) is false, which means our rule wouldn't have applied.
---
 src/lemmas.k.md | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/lemmas.k.md b/src/lemmas.k.md
index 1a24a4f4..bd368ad0 100644
--- a/src/lemmas.k.md
+++ b/src/lemmas.k.md
@@ -73,9 +73,7 @@ rule (X &Int Y) <=Int X => true
 ```
 
 ```k
-rule chop((X &Int Y) *Int Z) => (X &Int Y) *Int Z
-  requires (#rangeUInt(32,  X) orBool #rangeUInt(32, Y))
-  andBool #rangeUInt(224, Z)
+rule ((maxUInt32 &Int X) *Int pow224) <= maxUInt256 => true
 ```
 
 Repeated application of `modInt` can be simplified as follows. This lets us clean the storage