diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-11 20:02:33 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-11 20:02:33 -0500 |
commit | 383d061be2bc8162d3379c98ad106555d21e5f86 (patch) | |
tree | 56ae66e579cbadbe465a7f2617328df83ab9630b /src/theory/combination_engine.cpp | |
parent | b7bbe9a3bc30f41d1775a187ccc732aaeb41eaa1 (diff) |
(proof-new) Update TheoryEngine lemma and conflict to TrustNode (#5056)
This updates the theory engine interfaces for conflicts and lemmas to be in terms of TrustNode not Node.
This also updates the return value of getExplanation methods in TheoryEngine to TrustNode, but it does not yet add the proof generation code to that method yet, which will come in a separate PR.
Diffstat (limited to 'src/theory/combination_engine.cpp')
-rw-r--r-- | src/theory/combination_engine.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index f1e977fe3..5c9e6713b 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -113,7 +113,7 @@ eq::EqualityEngineNotify* CombinationEngine::getModelEqualityEngineNotify() void CombinationEngine::sendLemma(TrustNode trn, TheoryId atomsTo) { - d_te.lemma(trn.getNode(), false, LemmaProperty::NONE, atomsTo); + d_te.lemma(trn, LemmaProperty::NONE, atomsTo); } void CombinationEngine::resetRound() |