source: CIVL/examples/loop_invariants/loop_assigns_given/twoLoops.cvl

#include <civlc.cvh>
#pragma CIVL ACSL

int main() {
  int i = 0;

  /*@ loop invariant i >= 0 ;
    @ loop assigns i;
    @ loop variant i;
    @*/
  while (1) {    
    i++;   
    //@ assert i >= 0;
  }

  // The second loop will never executes

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