From ab81bbd336dce1cb45b049f08c7eefd26ea742d8 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 23 Mar 2022 23:51:25 +0000
Subject: [PATCH] Remove local declaration of void_t

With the move to C++ 17 we can use std::void_t instead.
---
 src/solvers/smt2_incremental/ast/smt_terms.h |  3 +-
 src/solvers/smt2_incremental/type_traits.h   | 37 --------------------
 2 files changed, 1 insertion(+), 39 deletions(-)
 delete mode 100644 src/solvers/smt2_incremental/type_traits.h

diff --git a/src/solvers/smt2_incremental/ast/smt_terms.h b/src/solvers/smt2_incremental/ast/smt_terms.h
index f69aadeffd6..c8b2d375a37 100644
--- a/src/solvers/smt2_incremental/ast/smt_terms.h
+++ b/src/solvers/smt2_incremental/ast/smt_terms.h
@@ -6,7 +6,6 @@
 #include <util/irep.h>
 
 #include <solvers/smt2_incremental/response_or_error.h>
-#include <solvers/smt2_incremental/type_traits.h>
 
 #include "smt_index.h"
 #include "smt_sorts.h"
@@ -150,7 +149,7 @@ class smt_function_application_termt : public smt_termt
   template <class functiont>
   struct has_indicest<
     functiont,
-    void_t<decltype(std::declval<functiont>().indices())>> : std::true_type
+    std::void_t<decltype(std::declval<functiont>().indices())>> : std::true_type
   {
   };
 
diff --git a/src/solvers/smt2_incremental/type_traits.h b/src/solvers/smt2_incremental/type_traits.h
deleted file mode 100644
index ea928e1ddb7..00000000000
--- a/src/solvers/smt2_incremental/type_traits.h
+++ /dev/null
@@ -1,37 +0,0 @@
-// Author: Diffblue Ltd.
-
-/// \file
-/// Back ports of utilities available in the `<type_traits>` library for C++14
-/// or C++17 to C++11. These can be replaced with the standard library versions
-/// as and when we upgrade the version CBMC is compiled with.
-
-#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_TYPE_TRAITS_H
-#define CPROVER_SOLVERS_SMT2_INCREMENTAL_TYPE_TRAITS_H
-
-#include <type_traits>
-
-namespace detail // NOLINT
-{
-// Implementation detail of `void_t`.
-template <typename... typest>
-struct make_voidt
-{
-  using type = void;
-};
-} // namespace detail
-
-// The below definition is of a back-ported version of the C++17 STL
-// `std::void_t` template. This makes this particular template available when
-// compiling for the C++11 or C++14 standard versions. It will also compile
-// as-is when targeting the C++17 standard. The back-ported version is not added
-// to the `std` namespace as this would be undefined behaviour. However once we
-// permanently move to the new standard the below code should be removed
-// and `std::void_t` should be used directly, to avoid polluting the global
-// namespace. For example -
-//   `void_t<decltype(foo.bar())>`
-// should be updated to -
-//   `std::void_t<decltype(foo.bar())>`
-template <typename... typest>
-using void_t = typename detail::make_voidt<typest...>::type;
-
-#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_TYPE_TRAITS_H