Fix operator-printing issue in SMT2.

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 421518fed1b8d5d84868b090cd99e5482d5f92c4..c9db1eecee6f28dfe981648d0f33fcbaddc3ed06 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -171,6 +171,9 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     case kind::BUILTIN:
       out << smtKindString(n.getConst<Kind>());
       break;
+    case kind::CHAIN_OP:
+      out << smtKindString(n.getConst<Chain>().getOperator());
+      break;
     case kind::CONST_RATIONAL: {
       Rational r = n.getConst<Rational>();
       if(r < 0) {