summaryrefslogtreecommitdiff
path: root/src/printer/smt2/smt2_printer.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
-rw-r--r--src/printer/smt2/smt2_printer.cpp3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 9bad4c7b5..3f7eb58c0 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -178,7 +178,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
if(toDepth != 0) {
n.getOperator().toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
types, language::output::LANG_SMTLIB_V2);
- out << " ";
} else {
out << "(...)";
}
@@ -207,7 +206,7 @@ void printBvParameterizedOp(std::ostream& out, TNode n) {
switch(n.getKind()) {
case kind::BITVECTOR_EXTRACT: {
BitVectorExtract p = n.getOperator().getConst<BitVectorExtract>();
- out << "extract " << p.high << " " << p.low;
+ out << "extract " << p.high << ' ' << p.low;
break;
}
case kind::BITVECTOR_REPEAT:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback