Use new variadic __add_noovfl(...) predicates
Do constant folding for final up/downsweep barrier invariants