projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f3c6bb5) | patch
(proof-new) Allow null proofs from generators in LazyCDProof (#5196)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 6 Oct 2020 14:31:16 +0000 (09:31 -0500)
committerGitHub <noreply@github.com>
Tue, 6 Oct 2020 14:31:16 +0000 (09:31 -0500)
commit6d663abe421c07976755c224180b1a1ee93442f6
treedfcc35c47d786bc19f311b1097f7ed73b0116224tree
parentf3c6bb510a87f390c51bf3cecc079cc9c9615ea4commit | diff
(proof-new) Allow null proofs from generators in LazyCDProof (#5196)

In some cases, a proof generator provided to a LazyCDProof may provide a null proof, which causes a segfault on proof-new currently. This PR makes LazyCDProof robust to this case; nullptr is interpreted as the fact is an assumption.
src/expr/lazy_proof.cpp diff | blob | history
src/expr/proof_node_manager.cpp diff | blob | history