diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-07 14:45:45 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-07 19:45:45 +0000 |
| commit | aa1f4021b70a1016502ead46bf68907bf092d65c (patch) | |
| tree | a0d9b352689cd27628b0be4adf1da2b297163d09 /src/theory/uf/proof_equality_engine.cpp | |
| parent | 8838a4e8ac47f94089044e2c638376c28a0fd7cd (diff) | |
(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.
Diffstat (limited to 'src/theory/uf/proof_equality_engine.cpp')
| -rw-r--r-- | src/theory/uf/proof_equality_engine.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
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 |