4 files changed, 6 insertions, 6 deletions
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index 6231d5a8a..6e1be2e09 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -117,13 +117,13 @@ ExprManager::mkFunctionType(const std::vector<const Type*>& argTypes,
   return FunctionType::getInstance(this, argTypes, range);
 }
 
-const Type* ExprManager::mkSort(std::string name) {
+const Type* ExprManager::mkSort(const std::string& name) {
   // FIXME: Sorts should be unique per-ExprManager
   NodeManagerScope nms(d_nodeManager);
   return new SortType(this, name);
 }
 
-Expr ExprManager::mkVar(const Type* type, string name) {
+Expr ExprManager::mkVar(const Type* type, const std::string& name) {
   NodeManagerScope nms(d_nodeManager);
   return Expr(this, new Node(d_nodeManager->mkVar(type, name)));
 }
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index 4b00c27fc..319a5d318 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -100,10 +100,10 @@ public:
                    const Type* range);
 
   /** Make a new sort with the given name. */
-  const Type* mkSort(std::string name);
+  const Type* mkSort(const std::string& name);
 
   // variables are special, because duplicates are permitted
-  Expr mkVar(const Type* type, std::string name);
+  Expr mkVar(const Type* type, const std::string& name);
   Expr mkVar(const Type* type);
 
 private:
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index ae6bdbd29..556b577e5 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -72,7 +72,7 @@ Node NodeManager::mkNode(Kind kind, const vector<Node>& children) {
   return NodeBuilder<>(this, kind).append(children);
 }
 
-Node NodeManager::mkVar(const Type* type, string name) {
+Node NodeManager::mkVar(const Type* type, const std::string& name) {
   Node n = mkVar(type);
   n.setAttribute(VarNameAttr(), name);
   return n;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 29c738c10..1c46743e9 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -74,7 +74,7 @@ public:
   Node mkNode(Kind kind, const std::vector<Node>& children);
 
   // variables are special, because duplicates are permitted
-  Node mkVar(const Type* type, std::string name);
+  Node mkVar(const Type* type, const std::string& name);
   Node mkVar(const Type* type);
   Node mkVar();