This patch almost totally revised the patch for bug mdev-4177.
The latter had too many defects. In particular, it did not
propagate multiple equalities formed when merging a degenerate
disjunct into underlying AND formula.