diff options
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 4 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 4 |
2 files changed, 8 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 diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index ae589eba6..2b2824334 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -563,6 +563,10 @@ void Smt2Printer::toStream(std::ostream& out, Model& m, const Command* c) const } } 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; + } Node val = tm.getValue( n ); if(val.getKind() == kind::LAMBDA) { out << "(define-fun " << n << " " << val[0] |