From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 22 Aug 2014 19:40:14 +0000 (-0400)
Subject: Fix operator-printing issue in SMT2.
X-Git-Tag: cvc5-1.0.0~6509^2~34
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=60ae9e3334e74b04f9ad0287ecaa2a847e54ae1a;p=cvc5.git

Fix operator-printing issue in SMT2.
---

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) {