diff options
author | ajreynol <reynolds@larapc05.epfl.ch> | 2014-06-17 15:25:58 +0200 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-19 18:24:39 -0400 |
commit | 0fe78eebc0c0f2d01c7aa64725bee08ba5aa2274 (patch) | |
tree | 475b094989b0828d7d82e41160a010a6134e8674 /src/printer | |
parent | 35cdae503bd88633a52333bf06fbf80cd81926e2 (diff) |
For casc : print models of functions rewritten by sort inference.
Diffstat (limited to 'src/printer')
-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; } |