diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-03 01:16:08 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-02 23:16:08 -0700 |
| commit | f45c0f10a01023b7653c8c36ffe37f70e4e56baa (patch) | |
| tree | b45d33bbb0493f718b514127a7570774842682c0 | |
| parent | bc40dbf0d808a3e30b721ef04b985b3e594a88bd (diff) | |
Fix cvc printer for nullary constructors (#1856)
| -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; |