summaryrefslogtreecommitdiff
path: root/Test/test20/EmptySeq.bpl
blob: 2eeb95894bfd096a187732ffaf52e0b15cef65e0 (plain)
1
2
3
4
5
6
7
8
// RUN: %boogie -noVerify "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
type Seq T;

function Seq#Length<T>(Seq T) returns (int);
function Seq#Empty<T>() returns (Seq T);

axiom (forall<T> :: Seq#Length(Seq#Empty(): Seq T) == 0);