projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1d2c509) | patch
[proofs] Fix singleton check in MACRO_RES post-processing (#7498)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Tue, 26 Oct 2021 20:59:31 +0000 (17:59 -0300)
committerGitHub <noreply@github.com>
Tue, 26 Oct 2021 20:59:31 +0000 (20:59 +0000)
commit38b59f152974347c132f3ca665948f4a7780abc4
treedd4bfe185bb4f92f2dbf10a532361c726767712ftree
parent1d2c50986cb53207e0f99a950b939736db226634commit | diff
[proofs] Fix singleton check in MACRO_RES post-processing (#7498)

Previously the check for whether the original conclusion of the MACRO_RESOULTION step was a singleton was incomplete. Now the test is made the proper way.

Depends on #7497.

Fixes cvc5/cvc5-projects#318
src/smt/proof_post_processor.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2 [new file with mode: 0644] blob