  This paper presents two decidability results on the validity checking problem
for entailments of symbolic heaps in separation logic with Presburger
arithmetic and arrays. The first result is for a system with arrays and
existential quantifiers. The correctness of the decision procedure is proved
under the condition that sizes of arrays in the succedent are not existentially
quantified. This condition is different from that proposed by Brotherston et
al. in 2017 and one of them does not imply the other. The main idea is a novel
translation from an entailment of symbolic heaps into a formula in Presburger
arithmetic. The second result is the decidability for a system with both arrays
and lists. The key idea is to extend the unroll collapse technique proposed by
Berdine et al. in 2005 to arrays and arithmetic as well as double-linked lists.
