summaryrefslogtreecommitdiff
path: root/src/smt/command.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r--src/smt/command.cpp6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 419b925c4..c2aa1c5f9 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1168,8 +1168,8 @@ void DeclareFunctionCommand::toStream(std::ostream& out,
size_t dag,
Language language) const
{
- Printer::getPrinter(language)->toStreamCmdDeclareFunction(out,
- termToNode(d_func));
+ Printer::getPrinter(language)->toStreamCmdDeclareFunction(
+ out, d_symbol, sortToTypeNode(d_func.getSort()));
}
/* -------------------------------------------------------------------------- */
@@ -2221,7 +2221,7 @@ void GetQuantifierEliminationCommand::toStream(std::ostream& out,
Language language) const
{
Printer::getPrinter(language)->toStreamCmdGetQuantifierElimination(
- out, termToNode(d_term));
+ out, termToNode(d_term), d_doFull);
}
/* -------------------------------------------------------------------------- */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback