From 272c711611d9e020f1991bae7e96a4ecb9be4218 Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Wed, 21 Aug 2024 12:00:13 +0200
Subject: [PATCH] lemma correction

---
 test/kontrol/lido-lemmas.k | 1 -
 1 file changed, 1 deletion(-)

diff --git a/test/kontrol/lido-lemmas.k b/test/kontrol/lido-lemmas.k
index 1dfb3601..864862f3 100644
--- a/test/kontrol/lido-lemmas.k
+++ b/test/kontrol/lido-lemmas.k
@@ -255,7 +255,6 @@ module LIDO-LEMMAS
     rule X <Int A +Int B => true requires X <=Int 0 andBool 0  <Int A andBool 0 <=Int B [concrete(X), simplification]
     rule X <Int A +Int B => true requires X <=Int 0 andBool 0 <=Int A andBool 0  <Int B [concrete(X), simplification]
     rule X <Int A *Int B => true requires X <=Int 0 andBool 0  <Int A andBool 0  <Int B [concrete(X), simplification]
-    rule X <Int A /Int B => true requires X <=Int 0 andBool 0  <Int A andBool 0  <Int B [concrete(X), simplification, preserves-definedness]
 
     rule [chop-no-overflow-add-l]: X:Int <=Int chop ( X +Int Y:Int ) => X +Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)             [simplification]
     rule [chop-no-overflow-add-r]: X:Int <=Int chop ( Y +Int X:Int ) => X +Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)             [simplification]