[proof-new] Fixing SMT post-processor's handling of assumptions (#6277)

Previously the SMT post-processor would update any assumption as long as it
had a proof for it. This can be a problem when one as assumption introduced in a
scope that should not be expanded. This commit fixes the issue by adding the
option of configuring a proof node updater to track scopes and the assumptions
they introduce, which can be used to determine the prood nodes which should be
updated. It also changes the SMT post-processor to only update assumptions that
have not been introduced in some scope.

This commit fixes an issue found by @Lachnitt during the integration of CVC4 and Isabelle.

0 files changed, 0 insertions, 0 deletions