@@ -532,7 +532,6 @@ This is a variant of the \texttt{Lemma} tactic dedicated to \texttt{Havoc} predi

...

@@ -532,7 +532,6 @@ This is a variant of the \texttt{Lemma} tactic dedicated to \texttt{Havoc} predi

\paragraph{Separated} Expand Separation Cases\\

\paragraph{Separated} Expand Separation Cases\\

This tactic decompose a \texttt{separated}$(a,n,b,m)$ predicate into its four base cases: $a$ and $b$ have different bases, $a+n \leq b$, $b+m \leq a$, and $a[0..n-1]$ and $b[0..m-1]$ overlaps. The regions are separated in the first three cases, and not separated in the overlapping case. This is kind of normal disjunctive form of the separation clause.

This tactic decompose a \texttt{separated}$(a,n,b,m)$ predicate into its four base cases: $a$ and $b$ have different bases, $a+n \leq b$, $b+m \leq a$, and $a[0..n-1]$ and $b[0..m-1]$ overlaps. The regions are separated in the first three cases, and not separated in the overlapping case. This is kind of normal disjunctive form of the separation clause.