1 files changed, 20 insertions, 21 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 2e1170666..d33b97d66 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -15,25 +15,26 @@
  **/
 
 #include "printer/cvc/cvc_printer.h"
-#include "expr/expr.h" // for ExprSetDepth etc..
-#include "util/language.h" // for LANG_AST
-#include "expr/node_manager_attributes.h" // for VarNameAttr
-#include "expr/command.h"
-#include "theory/substitutions.h"
-#include "smt/smt_engine.h"
-#include "smt/options.h"
-#include "theory/theory_model.h"
-#include "theory/arrays/theory_arrays_rewriter.h"
-#include "printer/dagification_visitor.h"
-#include "util/node_visitor.h"
 
-#include <iostream>
-#include <vector>
-#include <string>
-#include <typeinfo>
 #include <algorithm>
+#include <iostream>
 #include <iterator>
 #include <stack>
+#include <string>
+#include <typeinfo>
+#include <vector>
+
+#include "expr/expr.h" // for ExprSetDepth etc..
+#include "expr/node_manager_attributes.h" // for VarNameAttr
+#include "options/language.h" // for LANG_AST
+#include "printer/dagification_visitor.h"
+#include "options/smt_options.h"
+#include "smt/smt_engine.h"
+#include "smt_util/command.h"
+#include "smt_util/node_visitor.h"
+#include "theory/arrays/theory_arrays_rewriter.h"
+#include "theory/substitutions.h"
+#include "theory/theory_model.h"
 
 using namespace std;
 
@@ -894,10 +895,6 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c,
 
 }/* CvcPrinter::toStream(Command*) */
 
-static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() {
-  Printer::getPrinter(language::output::LANG_CVC4)->toStream(out, sexpr);
-}
-
 template <class T>
 static bool tryToStream(std::ostream& out, const CommandStatus* s, bool cvc3Mode) throw();
 
@@ -1170,7 +1167,9 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, bool
 
 static void toStream(std::ostream& out, const SetInfoCommand* c, bool cvc3Mode) throw() {
   out << "% (set-info " << c->getFlag() << " ";
-  toStream(out, c->getSExpr());
+  OutputLanguage language =
+      cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4;
+  SExpr::toStream(out, c->getSExpr(), language);
   out << ")";
 }
 
@@ -1180,7 +1179,7 @@ static void toStream(std::ostream& out, const GetInfoCommand* c, bool cvc3Mode)
 
 static void toStream(std::ostream& out, const SetOptionCommand* c, bool cvc3Mode) throw() {
   out << "OPTION \"" << c->getFlag() << "\" ";
-  toStream(out, c->getSExpr());
+  SExpr::toStream(out, c->getSExpr(), language::output::LANG_CVC4);
   out << ";";
 }