From 76f42d0f1d167aea5a1993d85fafd57e5028b0a7 Mon Sep 17 00:00:00 2001
From: Burak Bilge Yalcinkaya <bbyalcinkaya@gmail.com>
Date: Sun, 22 Oct 2023 12:18:57 +0300
Subject: [PATCH] fix substrSparseBytes

---
 data/sparse-bytes.k | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/data/sparse-bytes.k b/data/sparse-bytes.k
index 91690d4c4..6f4823e10 100644
--- a/data/sparse-bytes.k
+++ b/data/sparse-bytes.k
@@ -67,7 +67,7 @@ module SPARSE-BYTES
 
   rule substrSparseBytes(SBChunk(SBI) REST, S, E) 
     => #let SUB = substrSBItem(SBI, S, E)
-       #in SUB substrSparseBytes(REST, S -Int size(SUB), E -Int size(SUB))
+       #in SUB substrSparseBytes(REST, 0, E -Int size(SBI))
     requires 0 <=Int S andBool S <=Int E
      andBool size(SBI) >Int S