//#rTerminationDerivable
/*
 * Date: 2014-02-06
 *
 * The stem is equivalent to false,
 * f(x) = 0 is a ranking function with supporting invariant -1 >= 0.
 *
 */

procedure StemUnsat() returns (x: int)
{
  assume(false);
  while (true) {
  }
}