summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/inst_match.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/inst_match.cpp')
-rw-r--r--src/theory/quantifiers/inst_match.cpp6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index c419bbc46..7e5424d9c 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -229,7 +229,7 @@ void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& term
}
if( print ){
if( firstTime ){
- out << "Instantiations of " << q << " : " << std::endl;
+ out << "(instantiation " << q << std::endl;
firstTime = false;
}
out << " ( ";
@@ -403,12 +403,12 @@ void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& te
}
if( print ){
if( firstTime ){
- out << "Instantiations of " << q << " : " << std::endl;
+ out << "(instantiation " << q << std::endl;
firstTime = false;
}
out << " ( ";
for( unsigned i=0; i<terms.size(); i++ ){
- if( i>0 ) out << ", ";
+ if( i>0 ) out << " ";
out << terms[i];
}
out << " )" << std::endl;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback