From 308e87f360322e13623ef47f4c1973338c03933c Mon Sep 17 00:00:00 2001
From: Alexander Bakst <abakst@galois.com>
Date: Wed, 16 Mar 2022 10:31:17 -0700
Subject: [PATCH] Fix error in  that does not correctly handle non-zero offset
 arrays.

---
 heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index 2ea9321b8b..a4e594d36c 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -4575,7 +4575,7 @@ permForLLVMArrayBorrow ap (FieldBorrow cell) =
   ValPerm_LLVMBlock $ llvmArrayCellPerm ap cell
 permForLLVMArrayBorrow ap (RangeBorrow (BVRange off len)) =
   ValPerm_Conj1 $ Perm_LLVMArray $
-  ap { llvmArrayOffset = llvmArrayCellToOffset ap off,
+  ap { llvmArrayOffset = llvmArrayCellToAbsOffset ap off,
        llvmArrayLen = len,
        llvmArrayBorrows = [] }