[proofs] [alethe] Fix Alethe post-processor (#8525)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Fri, 1 Apr 2022 19:22:42 +0000 (16:22 -0300)
committerGitHub <noreply@github.com>
Fri, 1 Apr 2022 19:22:42 +0000 (19:22 +0000)
commitc5d2f79e86d460addd922649a64a57eeb10ec059
treeebdd88d80f7bd8dc4985b30223083a9fdc593974
parent62ff810fa519c0f3f2f2c219a49e73e65f65d0db
[proofs] [alethe] Fix Alethe post-processor (#8525)

Previously the Alethe post-processor was merging subproofs, which should not be done at this stage. As a consequence some post-processed proofs were becoming open.
src/proof/alethe/alethe_post_processor.cpp
test/regress/cli/CMakeLists.txt
test/regress/cli/regress0/proofs/nomerge-alethe-pf.smt2 [new file with mode: 0644]