1 files changed, 7 insertions, 9 deletions
diff --git a/src/base/output.cpp b/src/base/output.cpp
index a4003efd0..4ef76a772 100644
--- a/src/base/output.cpp
+++ b/src/base/output.cpp
@@ -17,27 +17,25 @@
 
 #include <iostream>
 
-using namespace std;
-
 namespace cvc5 {
 
 /* Definitions of the declared globals from output.h... */
 
 null_streambuf null_sb;
-ostream null_os(&null_sb);
+std::ostream null_os(&null_sb);
 
 NullC nullStream;
 
 const std::string Cvc5ostream::s_tab = "  ";
-const int Cvc5ostream::s_indentIosIndex = ios_base::xalloc();
+const int Cvc5ostream::s_indentIosIndex = std::ios_base::xalloc();
 
-DebugC DebugChannel(&cout);
-WarningC WarningChannel(&cerr);
-MessageC MessageChannel(&cout);
+DebugC DebugChannel(&std::cout);
+WarningC WarningChannel(&std::cerr);
+MessageC MessageChannel(&std::cout);
 NoticeC NoticeChannel(&null_os);
 ChatC ChatChannel(&null_os);
-TraceC TraceChannel(&cout);
-std::ostream DumpOutC::dump_cout(cout.rdbuf());// copy cout stream buffer
+TraceC TraceChannel(&std::cout);
+std::ostream DumpOutC::dump_cout(std::cout.rdbuf());  // copy cout stream buffer
 DumpOutC DumpOutChannel(&DumpOutC::dump_cout);
 
 }  // namespace cvc5