reorg size inf
remove forall with upper bound from size inference; it actually made unsatisfiable constraints satisfiable, *and* was more complicated