7 files changed, 9 insertions, 8 deletions
diff --git a/src/util/decision_engine.cpp b/src/util/decision_engine.cpp
index 210391555..7641472f8 100644
--- a/src/util/decision_engine.cpp
+++ b/src/util/decision_engine.cpp
@@ -11,8 +11,9 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief .
+ ** \brief A decision engine for CVC4
  **
+ ** A decision engine for CVC4.
  **/
 
 #include "util/decision_engine.h"
diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h
index e1d9e21b7..3eee8aeb6 100644
--- a/src/util/decision_engine.h
+++ b/src/util/decision_engine.h
@@ -11,7 +11,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief A decision engine for CVC4.
+ ** \brief A decision engine for CVC4
  **
  ** A decision engine for CVC4.
  **/
diff --git a/src/util/options.cpp b/src/util/options.cpp
index f6d3c3092..1d2e4ed8b 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -79,7 +79,7 @@ string Options::getDescription() const {
   return optionsDescription;
 }
 
-void Options::printUsage(const string msg, std::ostream& out) {
+void Options::printUsage(const std::string msg, std::ostream& out) {
   out << msg << optionsDescription << endl << flush;
   // printf(usage + options.getDescription(), options.binary_name.c_str());
   //     printf(usage, binary_name.c_str());
diff --git a/src/util/output.cpp b/src/util/output.cpp
index 10db4f723..34a3af93e 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -63,7 +63,7 @@ void DebugC::printf(const char* tag, const char* fmt, ...) {
   }
 }
 
-void DebugC::printf(string tag, const char* fmt, ...) {
+void DebugC::printf(std::string tag, const char* fmt, ...) {
   if(d_tags.find(tag) != d_tags.end()) {
     // chop off output after 1024 bytes
     char buf[1024];
@@ -127,7 +127,7 @@ void TraceC::printf(const char* tag, const char* fmt, ...) {
   }
 }
 
-void TraceC::printf(string tag, const char* fmt, ...) {
+void TraceC::printf(std::string tag, const char* fmt, ...) {
   if(d_tags.find(tag) != d_tags.end()) {
     // chop off output after 1024 bytes
     char buf[1024];
diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
index c675ab6c9..057100d10 100644
--- a/src/util/rational_cln_imp.cpp
+++ b/src/util/rational_cln_imp.cpp
@@ -30,7 +30,7 @@ using namespace CVC4;
 /* Computes a rational given a decimal string. The rational
  * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>.
  */
-Rational Rational::fromDecimal(const string& dec) {
+Rational Rational::fromDecimal(const std::string& dec) {
   // Find the decimal point, if there is one
   string::size_type i( dec.find(".") );
   if( i != string::npos ) {
diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp
index aad1f8b2d..5921b8fd3 100644
--- a/src/util/rational_gmp_imp.cpp
+++ b/src/util/rational_gmp_imp.cpp
@@ -30,7 +30,7 @@ using namespace CVC4;
 /* Computes a rational given a decimal string. The rational
  * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>.
  */
-Rational Rational::fromDecimal(const string& dec) {
+Rational Rational::fromDecimal(const std::string& dec) {
   // Find the decimal point, if there is one
   string::size_type i( dec.find(".") );
   if( i != string::npos ) {
diff --git a/src/util/result.cpp b/src/util/result.cpp
index 9760eaefb..8e1db27c4 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -28,7 +28,7 @@ using namespace std;
 
 namespace CVC4 {
 
-Result::Result(const string& instr) :
+Result::Result(const std::string& instr) :
   d_sat(SAT_UNKNOWN),
   d_validity(VALIDITY_UNKNOWN),
   d_which(TYPE_NONE),