Fix simplify output for SMT2 printer.

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 1250bc6591727ddb9a25e31d36a5013739e0d1a2..6fd047ebc4d5fe33f4a9c33384491ff3983ddb50 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -967,9 +967,7 @@ static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) thr
 }
 
 static void toStream(std::ostream& out, const SimplifyCommand* c) throw() {
-  out << "Simplify( << " << c->getTerm() << " >> )";
-
-  out << "ERROR: don't know how to output simplify command" << endl;
+  out << "(simplify " << c->getTerm() << ")";
 }
 
 static void toStream(std::ostream& out, const GetValueCommand* c) throw() {