diff options
Diffstat (limited to 'src/printer/cvc')
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index a9d439a0f..c375c76c4 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -828,6 +828,10 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t } } else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) { Node n = Node::fromExpr( ((const DeclareFunctionCommand*)c)->getFunction() ); + if(n.getKind() == kind::SKOLEM) { + // don't print out internal stuff + return; + } TypeNode tn = n.getType(); out << n << " : "; /* Boolean terms functionality needs to be merged in |