diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 0b84893ae..851ae414e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1402,7 +1402,8 @@ Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRe << " Responsible theory is: " << theoryOf(atom)->getId() << std::endl; - Node explanation = theoryOf(atom)->explain(node); + TrustNode texplanation = theoryOf(atom)->explain(node); + Node explanation = texplanation.getNode(); Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl; PROOF({ if(proofRecipe) { @@ -1877,7 +1878,8 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector } else { - explanation = theoryOf(toExplain.d_theory)->explain(toExplain.d_node); + TrustNode texp = theoryOf(toExplain.d_theory)->explain(toExplain.d_node); + explanation = texp.getNode(); Debug("theory::explain") << "\tTerm was propagated by owner theory: " << theoryOf(toExplain.d_theory)->getId() << ". Explanation: " << explanation << std::endl; |