(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.

1 files changed, 3 insertions, 0 deletions

diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index 9f60a49e4..8ed9779d3 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -254,6 +254,8 @@ bool ProofNodeManager::updateNode(
 
 bool ProofNodeManager::updateNode(ProofNode* pn, ProofNode* pnr)
 {
+  Assert(pn != nullptr);
+  Assert(pnr != nullptr);
   if (pn->getResult() != pnr->getResult())
   {
     return false;
@@ -296,6 +298,7 @@ bool ProofNodeManager::updateNodeInternal(
     const std::vector<Node>& args,
     bool needsCheck)
 {
+  Assert(pn != nullptr);
   // ---------------- check for cyclic
   std::unordered_map<const ProofNode*, bool> visited;
   std::unordered_map<const ProofNode*, bool>::iterator it;