diff options
Diffstat (limited to 'src/theory/inference_manager_buffered.cpp')
| -rw-r--r-- | src/theory/inference_manager_buffered.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp index e5f6ae4e4..6789043b1 100644 --- a/src/theory/inference_manager_buffered.cpp +++ b/src/theory/inference_manager_buffered.cpp @@ -45,6 +45,7 @@ bool InferenceManagerBuffered::hasPendingLemma() const } bool InferenceManagerBuffered::addPendingLemma(Node lem, + InferenceId id, LemmaProperty p, ProofGenerator* pg, bool checkCache) @@ -59,7 +60,7 @@ bool InferenceManagerBuffered::addPendingLemma(Node lem, } } // make the simple theory lemma - d_pendingLem.emplace_back(new SimpleTheoryLemma(InferenceId::UNKNOWN, lem, p, pg)); + d_pendingLem.emplace_back(new SimpleTheoryLemma(id, lem, p, pg)); return true; } @@ -70,12 +71,13 @@ void InferenceManagerBuffered::addPendingLemma( } void InferenceManagerBuffered::addPendingFact(Node conc, + InferenceId id, Node exp, ProofGenerator* pg) { // make a simple theory internal fact Assert(conc.getKind() != AND && conc.getKind() != OR); - d_pendingFact.emplace_back(new SimpleTheoryInternalFact(InferenceId::UNKNOWN, conc, exp, pg)); + d_pendingFact.emplace_back(new SimpleTheoryInternalFact(id, conc, exp, pg)); } void InferenceManagerBuffered::addPendingFact( |