Fix bug with upperbound: now it is computed for all soft literals, including those in lower levels. This should improve the hardening.
Revise trim (to be extended later).