
module main
{
  var x : int;

  procedure Inc()
  {
    while (true) {
      if (x < 200) {
        x := x + 1;
      }
    }
  }

  procedure Dec()
  {
    while (true) {
      if (x > 0) {
        x := x - 1;
      }
    }
  }

  procedure Reset()
  {
    while (true) {
      if (x == 200) {
        x := 0;
      }
    }
  }

  init {
    x := 100; // Arbitrary initial value for x
  }

  concurrent {
    call Inc();
    call Dec();
    call Reset();
  }

  invariant x_between_0_and_200 : (x >= 0 && x <= 200);

  control {
    v = unroll(10); // Unroll the program for 10 steps
    check;
    print_results;
    v.print_cex(x);
  }
}
