class Sequences { 
	var xs: seq<int>

	method append(a: int) 
		requires acc(xs) 
		ensures acc(xs) 
		ensures size() == old(size()) + 1  /* verifies */ 
		ensures |xs| == old(|xs|) + 1      /* previously failed */ 
	{ xs := xs ++ [a] }
	 
	/* this heap-independent version also verifies. */ 
	method append0(ins: seq<int>, a: int) returns (outs: seq<int>) 
		ensures |outs| == |ins| + 1 
	{ outs := ins ++ [a] } 
	 
	function size(): int  
		requires rd(xs)
	{ |xs| }
}