#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
}