3 files changed, 5 insertions, 5 deletions
diff --git a/src/base/exception.h b/src/base/exception.h
index 51829c86c..704ca928e 100644
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -125,15 +125,15 @@ inline std::ostream& operator<<(std::ostream& os, const Exception& e)
 
 template <class T> inline void CheckArgument(bool cond, const T& arg,
                                              const char* tail) CVC4_PUBLIC;
-template <class T> inline void CheckArgument(bool cond, const T& arg,
-                                             const char* tail) {
+template <class T> inline void CheckArgument(bool cond, const T& arg CVC4_UNUSED,
+                                             const char* tail CVC4_UNUSED) {
   if(__builtin_expect( ( !cond ), false )) { \
     throw ::CVC4::IllegalArgumentException("", "", ""); \
   } \
 }
 template <class T> inline void CheckArgument(bool cond, const T& arg)
   CVC4_PUBLIC;
-template <class T> inline void CheckArgument(bool cond, const T& arg) {
+template <class T> inline void CheckArgument(bool cond, const T& arg CVC4_UNUSED) {
   if(__builtin_expect( ( !cond ), false )) { \
     throw ::CVC4::IllegalArgumentException("", "", ""); \
   } \
diff --git a/src/context/cdlist_forward.h b/src/context/cdlist_forward.h
index d7b1cbc61..1cdbab7cb 100644
--- a/src/context/cdlist_forward.h
+++ b/src/context/cdlist_forward.h
@@ -42,7 +42,7 @@ namespace context {
 template <class T>
 class DefaultCleanUp {
 public:
-  inline void operator()(T* t) const{}
+  inline void operator()(T* t CVC4_UNUSED) const{}
 };
 
 template <class T, class CleanUp = DefaultCleanUp<T>, class Allocator = std::allocator<T> >
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 0e8ace709..b7a2721ab 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -1084,7 +1084,7 @@ class CVC4_PUBLIC DatatypeIndexConstant {
  public:
   DatatypeIndexConstant(unsigned index);
 
-  const unsigned getIndex() const { return d_index; }
+  unsigned getIndex() const { return d_index; }
   bool operator==(const DatatypeIndexConstant& uc) const
   {
     return d_index == uc.d_index;