CollItem_false

function getCardSet(self: Ref): Int function getCardRarity(self: Ref): Int function getCardId(self: Ref): Int function cardType(self: Ref): Int function sgn(i: Int) : Int ensures i > 0 ==> result == 1 ensures i == 0 ==> result == 0 ensures i < 0 ==> result == -1 method compare(o1: Ref, o2: Ref) returns (res: Int) requires rel(o2, 0) == rel(o1, 1) && rel(o1, 2) == rel(o1, 0) && rel(o2, 2) == rel(o2, 1) ensures ((rel(res, 0) > 0) && rel(res, 1) > 0) ==> (rel(res, 2) > 0) // P2 { var returned : Bool returned := false if (o1 == o2){ res := 0 returned := true } if (!returned) { if (getCardSet(o1) < getCardSet(o2)) { res := -1 returned := true } else { if (getCardSet(o1) == getCardSet(o2)) { if (getCardRarity(o1) < getCardRarity(o2)) { res := 1 returned := true } else { if (getCardId(o1) == getCardId(o2)) { if (cardType(o1) > cardType(o2)) { res := 1 returned := true } else { if (cardType(o1) == cardType(o2)){ res := 0 returned := true }else{ res := -1 returned := true } } }else{ res := -1 returned := true } } }else{ res := -1 returned := true } } } assert returned }