diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index 0cfd435c9c..7d705be71d 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -4770,7 +4770,7 @@ permIndicesForProvingOffset ps imprecise_p off =
   let ixs_holdss = flip findMaybeIndices ps $ \p ->
         case llvmPermContainsOffset off p of
           Just (_, True) -> Just True
-          Just _ | isLLVMArrayPerm p && imprecise_p -> Just False
+          Just _ | llvmPermContainsArray p && imprecise_p -> Just False
           _ -> Nothing in
   case find (\(_,holds) -> holds) ixs_holdss of
     Just (i,_) -> [i]
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index c5af937ed5..06bb5c28c9 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -3733,6 +3733,19 @@ llvmAtomicPermEndOffset p =
 llvmAtomicPermRange :: AtomicPerm (LLVMPointerType w) -> Maybe (BVRange w)
 llvmAtomicPermRange p = fmap llvmBlockRange $ llvmAtomicPermToBlock p
 
+-- | Test if an LLVM atomic permission contains some range of offsets that have
+-- an array shape
+llvmPermContainsArray :: AtomicPerm (LLVMPointerType w) -> Bool
+llvmPermContainsArray (Perm_LLVMArray _) = True
+llvmPermContainsArray (Perm_LLVMBlock bp) =
+  shapeContainsArray $ llvmBlockShape bp where
+  shapeContainsArray :: PermExpr (LLVMShapeType w) -> Bool
+  shapeContainsArray (PExpr_ArrayShape _ _ _) = True
+  shapeContainsArray (PExpr_SeqShape sh1 sh2) =
+    shapeContainsArray sh1 || shapeContainsArray sh2
+  shapeContainsArray _ = False
+llvmPermContainsArray _ = False
+
 -- | Set the range of an 'LLVMBlock'
 llvmBlockSetRange :: LLVMBlockPerm w -> BVRange w -> LLVMBlockPerm w
 llvmBlockSetRange bp (BVRange off len) =