#include <civlc.cvh>
#pragma CIVL ACSL

int main() {
  int i = 0;

  /*@ loop invariant i >= 0 ;
    @*/
  while (i < 3) {    
    i++;   
  }

  /*@ loop invariant i >= 0 ;
    @*/
  while(1) i--;
}