blob: 829c82e06426d1f003597230a5fc195ca2ceddfd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
datatype Ballot = Ballot(seqno:int)
predicate BalLt(ba:Ballot, bb:Ballot)
{
ba.seqno < bb.seqno
}
lemma Cases()
{
var b1:Ballot;
var b2:Ballot;
if (b1 == b2) {
} else if (BalLt(b1,b2)) {
} else {
//assert b1.seqno == b1.seqno;
//assert b2.seqno == b2.seqno;
assert BalLt(b2, b1); // Fails without asserts above
}
}
|