Test/dafny4/Bug72.dfy


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
    }
}