summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
authorDejan Jovanović <dejan.jovanovic@gmail.com>2010-02-03 19:50:44 +0000
committerDejan Jovanović <dejan.jovanovic@gmail.com>2010-02-03 19:50:44 +0000
commite0fc2cbe091097d95dbe6dd2eb9b6416b75be279 (patch)
tree8259c8bac6274d16e1d78a9c96ab41fa2fbdfdac /src/util
parent03ca7cdb382216ef995665cc59a07b4125241965 (diff)
simple ITE parsing
Diffstat (limited to 'src/util')
-rw-r--r--src/util/command.cpp4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/util/command.cpp b/src/util/command.cpp
index 334180967..06545a0a0 100644
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -110,7 +110,9 @@ void CheckSatCommand::toStream(ostream& out) const {
}
void QueryCommand::toStream(ostream& out) const {
- out << "Query(" << d_expr << ")";
+ out << "Query(";
+ d_expr.printAst(out, 2);
+ out << ")";
}
void CommandSequence::toStream(ostream& out) const {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback