(proof-new) Minor changes to proof node updater (#5011)

(proof-new) Minor changes to proof node updater (#5011)

This includes some changes to proof node updater that are not currently on master.

This includes:
(1) Explicitly passing the result of the current proof node we are updating,
(2) Caching the results of updates based on Node. In other words, proofs (in the same scope) that we have already seen that prove the same thing as the current proof node are reused.

It also enables the compilation of proof post-processor, which was missing on master and makes Rewriter of SmtEngine public which is required for doing so.