summaryrefslogtreecommitdiff
path: root/src/theory/uf/theory_uf.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
-rw-r--r--src/theory/uf/theory_uf.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index b388dd1cb..84fad2f19 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -224,11 +224,11 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) {
d_equalityEngine.getExplanation(lhs, rhs, assumptions);
}
-void TheoryUF::explain(TNode literal) {
+Node TheoryUF::explain(TNode literal) {
Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl;
std::vector<TNode> assumptions;
explain(literal, assumptions);
- d_out->explanation(mkAnd(assumptions));
+ return mkAnd(assumptions);
}
void TheoryUF::presolve() {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback