Rounding Bug in Verification?

[DavePearce]

The following example verifies, when it clearly shouldn't:

type Money is {
    int dollars,    // number of dollar coins
    int fiftyCents  // number of fifty cent pieces
}

function giveChange(int fiveDollarNotes, Money cost) -> (Money r)
// Money provided for payment must be greater than cost of item
requires fiveDollarNotes * 500 >= cost.dollars * 100 + cost.fiftyCents * 50
// Amount of change returned must give total after cost
ensures (r.dollars + cost.dollars) * 100
        + (r.fiftyCents + cost.fiftyCents) * 50 == fiveDollarNotes * 500:
    //
    int totalPaid = fiveDollarNotes * 500
    int totalCost = cost.dollars * 100 + cost.fiftyCents * 50

    int totalChangeDollars = totalPaid - totalCost
    int r = totalChangeDollars / 100

    return {
        dollars: r,
        fiftyCents: 0
    } 

However, I can't seem to identify a minimal example which illustrates the rounding

[DavePearce]

Here is a minimal example, but this fails correctly:

function giveChange(int cs) -> {int dollars, int cents}
ensures ((dollars*100) + cents) == cs:
    //
    int d = cs / 100
    int c = (d*100)-cs
    return {
        dollars: d,
        cents: 0
    }

Likewise, this minimal WyAL example also fails:

assert "postcondition not satisfied":
    forall (int cs):
       (cs/100)*100 == cs

And, at this stage, I don't have time to investigate further.