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.cpp4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index dd6eac0ff..849d5c0a5 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -281,7 +281,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
case kind::ABS:
case kind::IS_INTEGER:
case kind::TO_INTEGER:
- case kind::TO_REAL: out << smtKindString(k) << " "; break;
+ case kind::TO_REAL:
+ case kind::POW: out << smtKindString(k) << " "; break;
case kind::DIVISIBLE:
out << "(_ divisible " << n.getOperator().getConst<Divisible>().k << ")";
@@ -545,6 +546,7 @@ static string smtKindString(Kind k) throw() {
case kind::IS_INTEGER: return "is_int";
case kind::TO_INTEGER: return "to_int";
case kind::TO_REAL: return "to_real";
+ case kind::POW: return "^";
// arrays theory
case kind::SELECT: return "select";
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback