Merged improvements of symbolic simplifier (revisions: r4220, r4226, r4235:4238) back into trunk. #1026