Adding Intermediate Assertions (2)
global:
a == a0
static int search(int a[], int v)
{
for(
int i = 0; i < a.length; i++ )
{
if( a[i] == v )
{ r = i;
return i; a[r] == v
}
} r = -1;
return -1;
}
[(( i) a[i] == v) ¨ a[r] == v] ^ [(( i) a[i] != v) ¨ r == -1]
