/***
 *** Command 
 ***   cbmc --unwind 20 --no-unwinding-assertions <this-file-name>
 ***
 *** returns a counterexample that shows an infinite execution (i.e.,
 *** the same program state is reached twice.
 ***
 *** The --no-unwinding-assertions is necessary to prevent CBMC from
 *** discovering that the loop can be unrolled further. 
 ***
 ***/

/** nondet has to be declared, but has special meaning */
int nondet_int (void);


void main(void)
{

  /**
   ** The idea is to non-deterministically store a state during
   ** execution and then check if it was repeated or not. CBMC takes
   ** care of resolving the non-determinism.
   **/


  // -- place to store 'saved' version of x and dir
  int sx;
  int sdir;

  // -- flag to indicate that we've stored a previous state
  int f;


  // -- x and dir of the original program
  int x;
  int dir = 1;

  // -- initially, the flag is unset, everything else is
  // -- non-deterministic, but saved values differ from real values
  f = 0;
  x = nondet_int ();
  sx = nondet_int ();
  sdir = nondet_int ();
  __CPROVER_assume (x != sx);
  __CPROVER_assume (sdir != dir);
  
  while (x > 0)
    {

      // -- non-deterministically either save current state, or check
      // -- if current state is different from saved state. The f flag
      // -- ensures that the state is saved at least once before the
      // -- assertion is made
      if (nondet_int ())
      {	f = 1;
        sx = x;
        sdir = dir; }
      else
	assert (!f || (x != sx || dir != sdir));
     
      x = x + dir;
      
      if (x > 10) dir = -1 * dir;
      if (x < 5) dir = -1 * dir;
    }
  
}