test-procedure-checker-6.ucl

module main
{
  var tail           : integer;
  var initialized    : boolean;

  input push_valid   : boolean;
  output value_found : boolean;

  init {
    tail = 0;
    initialized = false;
  }

  next {
    initialized' = true;

    if (push_valid) {
      call push();
    }
  }

  invariant push_affects_tail: initialized ==> (push_valid ==> (tail == past(tail) + 1));

  procedure [noinline] push()
    requires push_valid;
    modifies tail;
    ensures tail == old(tail) + 1;
  {
    tail = tail + 10;
  }

  control {
  print_module;
	v2 = unroll(4);
	check;
	print_results;
	// v2.print_cex(push_valid, tail);
  }
}