[proofs] [sat] Handle resolution proofs for optimized clauses in incremental (#8389)

[proofs] [sat] Handle resolution proofs for optimized clauses in incremental (#8389)

The SAT solver may associate, to the result of a resolution, a lower assertion
level than the current one. To be able to produce proofs to such clauses, we
extend the SAT proof manager to track which resolution results were
optimized. Then, when the SAT solver pops, the manager is notified and stores
the proofs for these optimized clauses, so that they can be reinserted when the
user context is popped. The latter is handled by the SAT proof manager's
OptClauseManager attribute.