summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/alpha_equivalence.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/alpha_equivalence.cpp')
-rwxr-xr-xsrc/theory/quantifiers/alpha_equivalence.cpp6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index 84bf2ec14..b72f15a01 100755
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -55,9 +55,9 @@ bool AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersE
return true;
}else{
//lemma ( q <=> d_quant )
- Trace("alpha-eq") << "Alpha equivalent : " << std::endl;
- Trace("alpha-eq") << " " << q << std::endl;
- Trace("alpha-eq") << " " << aen->d_quant << std::endl;
+ Trace("quant-ae") << "Alpha equivalent : " << std::endl;
+ Trace("quant-ae") << " " << q << std::endl;
+ Trace("quant-ae") << " " << aen->d_quant << std::endl;
qe->getOutputChannel().lemma( q.iffNode( aen->d_quant ) );
return false;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback