From aa1f4021b70a1016502ead46bf68907bf092d65c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 7 Apr 2021 14:45:45 -0500 Subject: (proof-new) Proper implementation of proof node cloning (#6285) Previously, we were traversing proof node as a tree, now we use a dag traversal. This also makes sure that proofs work when we have a external proof conversion and we are in incremental mode. In such cases, the final proof must be cloned to ensure that we do not overwrite proof nodes, which may be reused across multiple check-sat. --- src/theory/uf/proof_equality_engine.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/theory/uf/proof_equality_engine.cpp') diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index 5292f754f..3d6176840 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -349,7 +349,7 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc, return TrustNode::null(); } // clone it so that we have a fresh copy - pfBody = pfBody->clone(); + pfBody = d_pnm->clone(pfBody); Trace("pfee-proof") << "pfee::ensureProofForFact: add scope" << std::endl; // The free assumptions must be closed by assumps, which should be passed // as arguments of SCOPE. However, some of the free assumptions may not -- cgit v1.2.3