diff options
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 8e5a9dae4..95f35a5a6 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -797,8 +797,13 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c) } } } else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) { - Node n = Node::fromExpr( ((const DeclareFunctionCommand*)c)->getFunction() ); - if(n.getKind() == kind::SKOLEM) { + const DeclareFunctionCommand* dfc = (const DeclareFunctionCommand*)c; + Node n = Node::fromExpr( dfc->getFunction() ); + if(dfc->getPrintInModelSetByUser()){ + if(!dfc->getPrintInModel()){ + return; + } + }else if(n.getKind() == kind::SKOLEM) { // don't print out internal stuff return; } |