From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 30 Apr 2014 01:28:25 +0000 (-0400)
Subject: Fix simplify output for SMT2 printer.
X-Git-Tag: cvc5-1.0.0~6943
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=db9f91437fa4acae5c80b7b1a0bafc67bfa19943;p=cvc5.git

Fix simplify output for SMT2 printer.
---

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 1250bc659..6fd047ebc 100644
--- 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() {