From 2e060f15e32dfa02d924d32eb058ab7c27a31a24 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Petar=20Maksimovi=C4=87?=
 <PetarMax@users.noreply.github.com>
Date: Mon, 22 Jul 2024 18:27:10 +0200
Subject: [PATCH] Test for previously added simplification (#2530)

* adding first version of test

* Set Version: 1.0.647

* alternative lemma

---------

Co-authored-by: devops <devops@runtimeverification.com>
---
 kevm-pyk/pyproject.toml              | 2 +-
 kevm-pyk/src/kevm_pyk/__init__.py    | 2 +-
 package/version                      | 2 +-
 tests/specs/functional/lemmas-spec.k | 6 ++++++
 4 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
index 551fb468ad..381426b601 100644
--- a/kevm-pyk/pyproject.toml
+++ b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.646"
+version = "1.0.647"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
index 9f16528ed8..6ef4704288 100644
--- a/kevm-pyk/src/kevm_pyk/__init__.py
+++ b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.646'
+VERSION: Final = '1.0.647'
diff --git a/package/version b/package/version
index 5873c63698..452644bd0f 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-1.0.646
+1.0.647
diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k
index 12e42d036d..92deeac9fa 100644
--- a/tests/specs/functional/lemmas-spec.k
+++ b/tests/specs/functional/lemmas-spec.k
@@ -403,6 +403,12 @@ module LEMMAS-SPEC
           ) ... </k>
       requires lengthBytes(B) <Int 2 ^Int 64
 
+    claim [chop-additional-knowledge]: <k> runLemma (
+                      X <=Int chop ( X +Int C ) andBool Y <=Int chop ( Y +Int C )
+              andBool notBool ( ( X +Int C <Int pow256 ) andBool ( Y +Int C <Int pow256 ) )
+          ) => doneLemma ( false ) ... </k>
+    requires #rangeUInt(256, X) andBool #rangeUInt(256, Y) andBool #rangeUInt(256, C)
+
  // #padToWidth simplification
  // --------------------------