source: CIVL/examples/complex/unity.cvl

#include <complex.h>

$input int N = 3;

double _Complex mypow(double _Complex a, int n) {
  double _Complex result = 1.0;
  for (int i=0; i<n; i++)
    result *= a;
  return result;
}


int main(void) {
  // Assume x is an n-th root of 1 but not 1...
  double _Complex x;
  $havoc(&x);
  $assume(mypow(x, N) == 1.0);
  $assume(x != 1.0);
  
  double _Complex y = 0.0;
  for (int i=0; i<N; i++) {
    y += mypow(x, i);
  }
  $print("y = ", y, "\n");
  $assert(y*(x-1) == 0.0); // ok for N<=10
  $assert(y == 0.0);  // ok for N<=4
}

//   (1+x+x^2+x^3+ .... + x^{n-1} + x^{n-1}) * (1-x)
// =  1+x+x^2+x^3+ .... + x^{n-1} + x^{n-1} +
//     -x-x^2-x^3 ......................... -x^n
// =  1 - x^n = 1 - 1 = 0