diff options
Diffstat (limited to 'src/printer/printer.cpp')
| -rw-r--r-- | src/printer/printer.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 0e7550518..d13fc55f1 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -23,6 +23,7 @@ #include "printer/cvc/cvc_printer.h" #include "printer/smt2/smt2_printer.h" #include "printer/tptp/tptp_printer.h" +#include "smt/node_command.h" using namespace std; @@ -72,9 +73,10 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang) void Printer::toStream(std::ostream& out, const Model& m) const { for(size_t i = 0; i < m.getNumCommands(); ++i) { - const Command* cmd = m.getCommand(i); - const DeclareFunctionCommand* dfc = dynamic_cast<const DeclareFunctionCommand*>(cmd); - if (dfc != NULL && !m.isModelCoreSymbol(dfc->getFunction())) + const NodeCommand* cmd = m.getCommand(i); + const DeclareFunctionNodeCommand* dfc = + dynamic_cast<const DeclareFunctionNodeCommand*>(cmd); + if (dfc != NULL && !m.isModelCoreSymbol(dfc->getFunction().toExpr())) { continue; } |