prevent loops with anc caused by AVATAR models flip-flopping

[MichaelRawson]

As discussed with @quickbeam123, we can get into a situation with Minisat (Z3 may have the same problem, I'm not sure) where the solver flip-flops between one of two feasible models. This is not a problem per se - although annoying from a performance point of view - but it does lead to a looping scenario where we:

1. Be in model M1
2. Derive a SAT clause via "AVATAR known components" (-anc, partially-on by default)
3. Recompute model, get model M2
4. Derive another SAT clause
5. Recompute model, get model M1
6. Go to 1, loop indefinitely.

This quick fix prevents exactly this scenario by not adding duplicate clauses to the SAT solver. A longer-term solution would try to fix the underlying flip-flopping.

[MichaelRawson]

This logic is weird but inherited from the existing operator new.

[quickbeam123]

@MichaelRawson , is this intentionally only applied on the path of handleNonSplittable, maybe other split's and contradiction clauses could benefit too?

[MichaelRawson]

Conflicts should always be unique, so I'm reasonably certain that there is no point de-duplicating those. Split clauses I'm not sure about - I can't imagine a looping scenario there, and I have to think hard to produce an example where we get a duplicate split clause, but I'm happy to add the logic there too. Lmk if so.