diff --git a/NEWS b/NEWS
index 8e65fd174..fd2b86bf5 100644
--- a/NEWS
+++ b/NEWS
@@ -246,6 +246,10 @@ New in spot 2.4.4.dev (net yet released)
   - ltlcross could crash when calling remove_fin() on an automaton
     with 32 acceptance sets would need an additional set.
 
+  - the down_cast() helper function used in severaly headers of Spot
+    was not in the spot namespace, and caused issues with some
+    configurations of GCC.
+
 New in spot 2.4.4 (2017-12-25)
 
   Bugs fixed:
diff --git a/spot/misc/casts.hh b/spot/misc/casts.hh
index 56c315ae3..0b0b9720c 100644
--- a/spot/misc/casts.hh
+++ b/spot/misc/casts.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2015-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2011, 2015-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -34,112 +34,36 @@
 // If an error occurs during the cast, an exception is thrown.
 //
 // NB: down_cast can also be used on shared_ptr.
-
-namespace
+namespace spot
 {
-  // A helper struct to check that downcasts are performed down an inheritance
-  // hierarchy, not between unrelated types.
-  template<typename Base, typename Derived>
-  struct is_base_of : std::is_base_of<Base, Derived>
-  {};
-  template<typename Base, typename Derived>
-  struct is_base_of<Base*, Derived*> : is_base_of<Base, Derived>
-  {};
-  // Also handle smart pointers.
-  template<typename Base, typename Derived>
-  struct is_base_of<std::shared_ptr<Base>, std::shared_ptr<Derived>>
-    : is_base_of<Base, Derived>
-  {};
-
-  // std::is_pointer does not detect smart pointers.
-  // Make our own version that detects pointer, plain or smart.
-  template<typename T>
-  struct is_pointer : std::is_pointer<T>
-  {};
-  template<typename T>
-  struct is_pointer<std::shared_ptr<T>> : std::true_type
-  {};
-
-  template<typename T, typename U, bool check>
-  struct _downcast;
-
-  // A down-cast on non-pointer type is legitimate, e.g. down_cast<Derived&>(m);
-  // An error in the dynamic_cast will throw an exception.
   template<typename T, typename U>
-  struct _downcast<T, U, false>
+  inline
+  T down_cast(U* u) noexcept
   {
-    static_assert(is_base_of<U, T>::value, "invalid downcast");
+    SPOT_ASSERT(dynamic_cast<T>(u));
+    return static_cast<T>(u);
+  }
 
-    static
-    inline
-    T
-    cast(U u)
+  template<typename T, typename U>
+  inline
+  T down_cast(const std::shared_ptr<U>& u) noexcept
+  {
+    SPOT_ASSERT(std::dynamic_pointer_cast<typename T::element_type>(u));
+    return std::static_pointer_cast<typename T::element_type>(u);
+  }
+
+  template<typename T, typename U>
+  inline
+  T down_cast(U u)
 #ifdef NDEBUG
     noexcept
-#else
-    noexcept(is_pointer<T>::value)
 #endif
-    {
-#ifdef NDEBUG
-      return static_cast<T>(u);
-#else
-      return dynamic_cast<T>(u);
-#endif
-    }
-  };
-
-  // A specialization for smart pointer, so that down_cast can be used
-  // uniformly.
-  // NB: Use
-  //    auto d = down_cast<std::shared_ptr<T>>(b);
-  // instead of
-  //    auto d = std::dynamic_pointer_cast<T>(b);
-  template<typename T, typename U>
-  struct _downcast<std::shared_ptr<T>, U, false>
   {
-    static_assert(is_base_of<U, std::shared_ptr<T>>::value, "invalid downcast");
-
-    static
-    inline
-    std::shared_ptr<T>
-    cast(U u) noexcept
-    {
 #ifdef NDEBUG
-      return std::static_pointer_cast<T>(u);
+    return static_cast<T>(u);
 #else
-      return std::dynamic_pointer_cast<T>(u);
+    return dynamic_cast<T>(u);
 #endif
-    }
-  };
-
-  // Pointer type specialization.
-  // Cast errors are caught by an assertion, no exception is thrown.
-  template<typename T, typename U>
-  struct _downcast<T, U, true>
-  {
-    static
-    inline
-    T
-    cast(U u) noexcept
-    {
-      T t = _downcast<T, U, false>::cast(u);
-      SPOT_ASSERT(t);
-      return t;
-    }
-  };
-} // anonymous namespace
-
-// The actual function to call.
-template<typename T, typename U>
-inline
-T
-down_cast(U u)
-#ifdef NDEBUG
-    noexcept
-#else
-    noexcept(is_pointer<T>::value)
-#endif
-{
-  return _downcast<T, U, is_pointer<T>::value>::cast(u);
-}
+  }
 
+} // namespace spot
diff --git a/tests/core/ikwiad.cc b/tests/core/ikwiad.cc
index ada62e4de..b60aa72f9 100644
--- a/tests/core/ikwiad.cc
+++ b/tests/core/ikwiad.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2007-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2007-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003-2007 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -1155,7 +1155,7 @@ checked_main(int argc, char** argv)
           if (scc_filter && (reduction_dir_sim || reduction_rev_sim))
             {
               tm.start("SCC-filter post-sim");
-              auto aa = down_cast<spot::const_twa_graph_ptr>(a);
+              auto aa = spot::down_cast<spot::const_twa_graph_ptr>(a);
               // Do not filter_all for SBA
               a = spot::scc_filter(aa, assume_sba ?
                                    false : scc_filter_all);
diff --git a/tests/core/ngraph.cc b/tests/core/ngraph.cc
index 8ae18c963..6de093314 100644
--- a/tests/core/ngraph.cc
+++ b/tests/core/ngraph.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement de
+// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement de
 // l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -347,7 +347,7 @@ public:
 
   int compare(const spot::state* other) const override
   {
-    auto o = down_cast<const my_state*>(other);
+    auto o = spot::down_cast<const my_state*>(other);
 
     // Do not simply return "other - this", it might not fit in an int.
     if (o < this)