Predicate ContradictoryTypeChecks::contradictoryTypeCheck

e assumes that v could be of type t, but cond, in fact, ensures that v is not of type sup, which is a supertype of t.

predicate contradictoryTypeCheck(Expr e, Variable v, RefType t, RefType sup, Expr cond)