summaryrefslogtreecommitdiff
path: root/src/printer/smt/smt_printer.cpp
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-04-06 22:06:52 +0000
committerMorgan Deters <mdeters@gmail.com>2012-04-06 22:06:52 +0000
commit7237456b4e2e5a119feacf98f52ec9e55d7a62a5 (patch)
treeea510f4987dadcdbbb361684445419e4939cdf00 /src/printer/smt/smt_printer.cpp
parent6a5fb6d945b109921cb9b6117f4ede0b6d110c08 (diff)
* Fix ITEs and functions in CVC language printer.
* Permit "BOOL = BOOL" in CVC language parser (auto-replaced with IFF internally, except in strict mode). * SExpr atoms now can be string-, integer-, or rational-valued. * SmtEngine::setInfo(":status", ...) now properly dumps a SetBenchmarkStatusCommand rather than a SetInfoCommand. * Some dumping fixes (resolves bug 313)
Diffstat (limited to 'src/printer/smt/smt_printer.cpp')
-rw-r--r--src/printer/smt/smt_printer.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp
index 2ac514988..e6490de63 100644
--- a/src/printer/smt/smt_printer.cpp
+++ b/src/printer/smt/smt_printer.cpp
@@ -45,7 +45,7 @@ void SmtPrinter::toStream(std::ostream& out, const Command* c,
void SmtPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
s->toStream(out, language::output::LANG_SMTLIB_V2);
-}
+}/* SmtPrinter::toStream() */
}/* CVC4::printer::smt namespace */
}/* CVC4::printer namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback