/* Commandline execution:
 *		civl verify dynamicStruct.cvl
 * */
#include <civlc.h>

void f(int n) {
  int sum;
  typedef struct foo {
    int sum;
    int bar[n];
  } foo;
  
  foo s;
  sum = (n * (n - 1)) / 2;
  if (n > 1) {
    $spawn f(n-1);
  }
  s.sum = 0;
  for (int i = 0; i < n; i++) {
    s.bar[i] =  i;
    s.sum += s.bar[i];
  }
  $assert sum == s.sum;
}

void main() {
  $spawn f(3);
}