@@ -24,7 +24,7 @@ Given the symbolic heaps $\varphi$ and $\psi$ in \slah\ such that

Our goal in this section is to show that the entailment problem is decidable, as stated in the following theorem.

\begin{theorem}\label{thm-entail}

The entailment problem of {\slah} is in 2-EXPTIME.

The entailment problem of {\slah} is in EXPTIME.

\end{theorem}

For comparison, the entailment problem of quantifier-free ASL formulas is in coNP~\cite{BrotherstonGK17}.

...

...

@@ -49,7 +49,7 @@ In Section~\ref{ssec:ent-1}, we consider the special case

The general case is dealt with in Section~\ref{ssec:ent-all};

the procedure calls the special case for the first atom of the consequent with

all the compatible prefixes of the antecedent, and

it does a recursive call for the remainders of the consequent and the antecedent. Note that to find all the compatible prefixes of the antecedent, some spatial atoms in the antecedent might be split into several ones. The doubly-exponential time complexity of the decision procedure is due to: 1) the enumeration of total preorders as well as different splittings of the spatial atoms in the antecedent, 2) the satisfiability of quantifier-free{\PbA} formulas (with modulo constraints) is NP-complete.

it does a recursive call for the remainders of the consequent and the antecedent. Note that to find all the compatible prefixes of the antecedent, some spatial atoms in the antecedent might be split into several ones. The EXPTIME complexity is explained in the sequel: 1) the number of total preorders as well as different splittings of the spatial atoms in the antecedent is at most exponential, 2) the entailment of {\EPbA} formulas (with modulo constraints) can be solved in exponential time.

%At first, it is easy to observe that if $\abs(\varphi)$ is unsatisfiable,

%then the entailment holds. Moreover, if $\abs(\varphi) \not\models \abs(\psi)$,