@@ -60,11 +60,11 @@ The ordered entailment problem is then decided by matching each spatial atom in

Splitting a spatial atom into multiple ones in the antecedent is attributed to pointer arithmetic and unnecessary for SH fragments with nominal addresses.

%Moreover, the availability of $\hls{}$ makes the splitting more involved.

We implemented the decision procedures on top of \cspen\footnote{We anonymize the name of the tool to comply with the double blind procedure.} solver~\cite{GuCW16}.

We implemented the decision procedures on top of the \cspen\footnote{We anonymize the name of the tool to comply with the double blind procedure.} solver. %~\cite{GuCW16}.

We evaluate the performance of the new solver, called {\cspenp}~\cite{CompSpenSite},

on a set of formulas originating from path conditions and verification conditions of programs working on heap lists in memory allocators.

We also randomly generate some formulas, in order to test the scalability of {\cspenp} further.

The experimental results show that {\cspenp} is able to solve the satisfiability and entailment problems for {\slah} efficiently (in average, less than 1 second for satisfiability and less than 15 seconds for entailment).\zhilin{The anonymization is properly done.}

The experimental results show that {\cspenp} is able to solve the satisfiability and entailment problems for {\slah} efficiently (in average, less than 1 second for satisfiability and less than 15 seconds for entailment).%\zhilin{The anonymization is properly done.}

To the best of our knowledge, this work presents the first decision procedure and automated solver for decision problems in a separation logic fragment allowing both pointer arithmetic and memory blocks inside inductive definitions.