diff options
Diffstat (limited to 'src/printer/cvc/cvc_printer.cpp')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
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; |