fix substrSparseBytes

runtimeverification · Oct 22, 2023 · 76f42d0 · 76f42d0
1 parent 89a9221
commit 76f42d0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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