diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-11 22:38:04 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-11 22:38:04 -0500 |
| commit | 3a8a27994584ca2168ef71d5eb0ce46ef558ba34 (patch) | |
| tree | efa67475c597a8fdb6664a67dd80e7b022919bd2 /src/preprocessing | |
| parent | 383d061be2bc8162d3379c98ad106555d21e5f86 (diff) | |
(proof-new) Add SMT proof manager (#5054)
This module is responsible for constructing the proof checker, proof node manager, and implementing dumping and checking of the final proof.
This PR includes setting up some connections into the various modules for proof production.
Diffstat (limited to 'src/preprocessing')
| -rw-r--r-- | src/preprocessing/assertion_pipeline.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index a9e2d4d36..735a93f56 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -72,7 +72,7 @@ void AssertionPipeline::pushBackTrusted(theory::TrustNode trn) { Assert(trn.getKind() == theory::TrustNodeKind::LEMMA); // push back what was proven - push_back(trn.getProven(), false, trn.getGenerator()); + push_back(trn.getProven(), false, false, trn.getGenerator()); } void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen) |