Unwound SSA has incorrect guards for return from loop body

[peterschrammel]

Example:

extern void __VERIFIER_error() __attribute__ ((__noreturn__));
void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } }
#define SIZE 1
int _strcmp( int src[SIZE] , int dst[SIZE] ) {
  int i = 0;
  while ( i < SIZE ) {
    int k=src[i];
    int l=dst[i];
    if( k != l ) return 1;
    i = i + 1;
  }
  return 0;
}
int main( ) {
  int a[SIZE];
  int b[SIZE];
  int c = _strcmp( a , b );
  if ( c == 0 ) {
    int x;
    for ( x = 0 ; x < SIZE ; x++ ) {
      int m=a[x];
      int n=b[x];
      __VERIFIER_assert( m == n );
    }
  }
  return 0;
}