diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-13 19:10:19 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-13 19:10:19 -0500 |
| commit | 0fdf29ba194b8f6763ae41bea05b3208345d89b9 (patch) | |
| tree | 97e2a41d50f625a68637dfc9e038eec7a0949de6 /src/theory/eager_proof_generator.cpp | |
| parent | c3a075c82c6ba038bfb58a8ef7dfb3bb2fc244c0 (diff) | |
(proof-new) Miscellaneous minor improvements and fixes to proofs in theory files. (#5241)
Diffstat (limited to 'src/theory/eager_proof_generator.cpp')
| -rw-r--r-- | src/theory/eager_proof_generator.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp index bc101595f..c49c33790 100644 --- a/src/theory/eager_proof_generator.cpp +++ b/src/theory/eager_proof_generator.cpp @@ -30,7 +30,10 @@ EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm, void EagerProofGenerator::setProofFor(Node f, std::shared_ptr<ProofNode> pf) { // pf should prove f - Assert(pf->getResult() == f); + Assert(pf->getResult() == f) + << "EagerProofGenerator::setProofFor: unexpected result" << std::endl + << "Expected: " << f << std::endl + << "Actual: " << pf->getResult() << std::endl; d_proofs[f] = pf; } void EagerProofGenerator::setProofForConflict(Node conf, |