From 60ae9e3334e74b04f9ad0287ecaa2a847e54ae1a Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 22 Aug 2014 15:40:14 -0400
Subject: [PATCH] Fix operator-printing issue in SMT2.

---
 src/printer/smt2/smt2_printer.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 421518fed..c9db1eece 100644
--- 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) {
-- 
2.30.2