From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 3 Oct 2014 17:09:39 +0000 (-0400)
Subject: Minor fixes to CVC printer.
X-Git-Tag: cvc5-1.0.0~6509^2~18
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4a69f126fb2301f8da2db3841e1362aacb59362c;p=cvc5.git

Minor fixes to CVC printer.
---

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 9b3e83578..3f93106a0 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -152,6 +152,9 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       case BOOLEAN_TYPE:
         out << "BOOLEAN";
         break;
+      case STRING_TYPE:
+        out << "STRING";
+        break;
       default:
         out << tc;
         break;
@@ -162,15 +165,13 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       out << n.getConst<Datatype>().getName();
       break;
 
-    case kind::EMPTYSET: {
+    case kind::EMPTYSET:
       out << "{} :: " << n.getConst<EmptySet>().getType();
-      return;
       break;
-    }
 
     default:
-      // fall back on whatever operator<< does on underlying type; we
-      // might luck out and print something reasonable
+      // Fall back to whatever operator<< does on underlying type; we
+      // might luck out and print something reasonable.
       kind::metakind::NodeValueConstPrinter::toStream(out, n);
     }