diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-11 14:38:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-11 14:38:13 -0500 |
| commit | bff3b0cbcc38cae5548bc4b36af5bb1c0f66c149 (patch) | |
| tree | c7c980ff07ebf1895633a9e22ca14010c8089d4f /src/expr/proof_node_manager.cpp | |
| parent | edf2e3ff7b751001901d377c3aacd044a3e15ef4 (diff) | |
(proof-new) Use deep copy for final lemma step in proof equality engine (#5013)
Previously, strings on proof-new used a ProofStepBuffer for deriving the final conclusion of lemmas in proof equality engine (assertLemma). This was recently changed to use the more standard ProofGenerator interface of assertLemma. However, there was a bug in this method: the steps from this proof need to be deep copied into the proof we are generating or otherwise the explanation of these literals are not connected in the CDProof. This updates the proof equality engine so that it instructs the proof generator to do a deep copy in this case. Notice this is very rarely more than a single step.
Diffstat (limited to 'src/expr/proof_node_manager.cpp')
0 files changed, 0 insertions, 0 deletions