Preserve mapping between old and new representatives with AC symbols

[bclement-ocp]

In CC(X), the leaves are always terms that were present in the original problem: we do not introduce new uninterpreted terms.

In AC(X), this is no longer true: we might introduce new AC leaves dynamically that are not themselves term representatives (i.e. they don't have an entry in the repr map) through "deep" rewriting into the AC leaf.

When we have a class representative rr for a semantic value r, and a new class representative nrr is found, the relations see an equality (with Subst origin) r = nrr. Normally, since rr is a term representative, we have rr --> rr as a mapping, and so the relation will see rr = nrr and can use this to update its internal state.

With these "dynamic" representative, when they later get override by a new representative, the relations will not see an rr = nrr equality, which makes its internal state get out of sync and can cause bugs.

This patch makes it so that, when we encounter one of these "dynamic" representatives, we artificially add the rr = nrr equality (by adding rr --> nrr as a pivot, which will in turn cause the equality to show up).

Since this case should only be possible with AC rewriting, the rr = nrr equality is only added in up_uf_rs, i.e. if there are AC rewrite rules.

Fixes #474

(Note that I did not add the original test case from #474 as a test — this is because since #731, we simplify if true then ruqv0 else ur_3 into ruqv0 which causes Alt-Ergo to not terminate with the CDCL solver)

[bclement-ocp]

Marking as draft for now since, while the diagnosis is correct, I am not sure the fix is the right one.