From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 3 May 2018 06:16:08 +0000 (-0500)
Subject: Fix cvc printer for nullary constructors (#1856)
X-Git-Tag: cvc5-1.0.0~5100
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f45c0f10a01023b7653c8c36ffe37f70e4e56baa;p=cvc5.git

Fix cvc printer for nullary constructors (#1856)
---

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index d778ccc2b..f9cd7db83 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -385,6 +385,12 @@ void CvcPrinter::toStream(
           return;
         }else{
           toStream(op, n.getOperator(), depth, types, false);
+          if (n.getNumChildren() == 0)
+          {
+            // for datatype constants d, we print "d" and not "d()"
+            out << op.str();
+            return;
+          }
         }
       }
       break;