source: CIVL/examples/arithmetic/meanBad.cvl

/* Commandline execution:
 *              civl verify -inputB=10 meanBad.cvl
 * or (if you want to find the minimal counterexample)
 *              civl verify -inputB=10 -min meanBad.cvl
 */
$input int B = 10;
$input int n;
$assume(1<=n && n<=B);
$input double a[n];
double s;

void main() {
  double mean1() {
    double sum=0.0;

    for (int i=0; i<n; i++)
      sum += a[i];
    return sum/n;
  }
  double mean2() {
    double result=a[0];

    for (int i=1; i<n; i++)
      result = result*(i/(i+1)) + a[i]/(i+1);
    return result;
  }
  double result1 = mean1();
  double result2 = mean2();
  $assert(result1==result2); 
}