/**
 * Issue here is that focus cannot be applied across functions as usual.
 * If we want to apply focus to a loop in a function then that function
 * needs a function contract.
 
 * Function contract here doesn't work for some reason (CIVL bug)
 
 * Also the postcondition currently can't be transformed with focus
 * so an assertion must be inserted into the function to apply focus.
 * This could be fixed.
 */
#include<assert.h>

#pragma CIVL ACSL

$input int N;
$assume(N > 0);
$input double a[N];
$input double b[N];

/*@ requires n > 0;
  @ requires \valid(a+(0..n)) && \valid(b+(0..n));
  @ assigns \nothing;
  @ ensures (\result == \true) ==> (\forall int i; 0 <= i && i < n ==> a[i] == b[i]);
  @*/
_Bool arrayEquals(double * a, double * b, int n) {
  _Bool equal = $true;

  //@ focus F;
  for (int i = 0; i < n; i++) 
    if (a[i] != b[i])
      equal = $false;
  //@ focus F;
  assert($forall (int i: 0 .. n-1) equal => a[i] == b[i]);
  return equal;
}

int main() {
  _Bool ret = arrayEquals(a, b, N);
  
  if (ret) {
    assert($forall (int i: 0 .. N-1) a[i] == b[i]);
  }
}