congruence closure not returning redundant propagation
new regression test