(proof-new) Updates to proof node updater algorithm (#5088)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 18 Sep 2020 02:38:42 +0000 (21:38 -0500)
committerGitHub <noreply@github.com>
Fri, 18 Sep 2020 02:38:42 +0000 (21:38 -0500)
commit89c5d4ac65f45f24a7dc0ab76bb2bdb447bdfcda
treecd827a431bbd9122b683dee079869f253c0299ac
parentcb438c1aca9e205359313f2e661fef910e1132b6
(proof-new) Updates to proof node updater algorithm (#5088)

This updates the proof node updater so that we apply updates to a fixed point, stopping if the proof node is not updated or if the callback explicitly tells us not to continue. This also fixes an issue where proof nodes would be updated to SCOPE and incorrectly traversed after updating.

This additionally adds debugging feature to proof node updater to track the moment at which an unexpected free assumption is introduced by an update.
src/expr/proof_node_updater.cpp
src/expr/proof_node_updater.h
src/smt/proof_post_processor.cpp
src/smt/proof_post_processor.h