[proofs] [sat] Make SAT assumption bookeeping robust to incremental (#8536)

[proofs] [sat] Make SAT assumption bookeeping robust to incremental (#8536)

Similarly to what happened with proofs of optimized SAT clauses getting lost (in the sense of inserted at lower assertion levels than the current one, during incremental solving), we need to make the bookeeping of the current SAT assumptions in the SAT proof manager robust to context popping. Not doing so can break the final proof construction, which relies on this information. A regression is added which showed the issue via the openness of a step added to the lazy proof chain (even though this did not lead to issues in the final proof).

This commit extends the OptimizedClausesManager to also optionally track a hash set of nodes to have nodes added to it during popping. This is hooked in the SAT proof manager to the SAT assumptions hash set.

There are four instances of notifications to the SAT proof manager of SAT assumptions: two in the proof CNF stream and two in the SAT solver. We only need to worry about the proof CNF stream ones, since the SAT solver ones are for literals (which do
not have assertion levels) and for some cases of the final conflict clause generated, which is always at the current assertion level. For the proof CNF stream ones it suffices to notify the SAT proof manager when the CNF stream itself is notified that a propagation or clause was inserted at an optimized level, as these are the only possible cases.