From 970f7d073402ffc307f1cdb143a14d980c7a870f Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Wed, 9 Oct 2024 22:26:33 +0100
Subject: [PATCH] adding appropriate test

---
 tests/specs/functional/lemmas-spec.k | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k
index bd5acfe8ae..05b336c043 100644
--- a/tests/specs/functional/lemmas-spec.k
+++ b/tests/specs/functional/lemmas-spec.k
@@ -361,6 +361,11 @@ module LEMMAS-SPEC
       <k> runLemma( #range (#buf(8, X:Int), -3, _:Int) ) => doneLemma( .Bytes ) ... </k>
       requires 0 <=Int X andBool X <Int pow64
 
+    claim [range-39]:
+      <k> runLemma( b"\xaa" ==K #range ( BYTES:Bytes +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" , ( lengthBytes ( BYTES:Bytes ) /Int 2 ) , 1 ) [ ( lengthBytes ( BYTES:Bytes ) /Int 2 ) := b"\xaa" ] )
+            => doneLemma(true) ... </k>
+      requires lengthBytes ( BYTES:Bytes ) <Int 32
+
  // #buf simplification
  // -------------------
     claim [bufExtractPadding]: <k> runLemma ( #asWord ( ( #range( #buf ( 32 , X ), 0, 28 ) ):Bytes ) ) => doneLemma ( 0 ) ... </k> requires #rangeUInt(32, X)