diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp
index 1112df70a87..7f16b087364 100644
--- a/jbmc/src/java_bytecode/java_utils.cpp
+++ b/jbmc/src/java_bytecode/java_utils.cpp
@@ -577,7 +577,7 @@ void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class)
   symbol.type.set(ID_C_class, declaring_class);
 }
 
-NODISCARD optionalt<std::string>
+[[nodiscard]] optionalt<std::string>
 class_name_from_method_name(const std::string &method_name)
 {
   const auto signature_index = method_name.rfind(":");
diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h
index 148406dd204..1e23021188e 100644
--- a/jbmc/src/java_bytecode/java_utils.h
+++ b/jbmc/src/java_bytecode/java_utils.h
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <unordered_set>
 
-#include <util/nodiscard.h>
 #include <util/pointer_expr.h>
 
 #include <goto-programs/resolve_inherited_component.h>
@@ -185,7 +184,7 @@ void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class);
 /// Get JVM type name of the class in which \p method_name is defined.
 /// Returns an empty optional if the class name cannot be retrieved,
 /// e.g. method_name is an internal function.
-NODISCARD optionalt<std::string>
+[[nodiscard]] optionalt<std::string>
 class_name_from_method_name(const std::string &method_name);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
diff --git a/src/cprover/bv_pointers_wide.h b/src/cprover/bv_pointers_wide.h
index 790a24e3b57..02f65e13897 100644
--- a/src/cprover/bv_pointers_wide.h
+++ b/src/cprover/bv_pointers_wide.h
@@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_CPROVER_BV_POINTERS_WIDE_H
 #define CPROVER_CPROVER_BV_POINTERS_WIDE_H
 
-#include <util/nodiscard.h>
 #include <util/pointer_expr.h>
 
 #include <solvers/flattening/boolbv.h>
@@ -51,13 +50,12 @@ class bv_pointers_widet : public boolbvt
   // NOLINTNEXTLINE(readability/identifiers)
   typedef boolbvt SUB;
 
-  NODISCARD
-  bvt encode(const mp_integer &object, const pointer_typet &) const;
+  [[nodiscard]] bvt
+  encode(const mp_integer &object, const pointer_typet &) const;
 
   virtual bvt convert_pointer_type(const exprt &);
 
-  NODISCARD
-  virtual bvt add_addr(const exprt &);
+  [[nodiscard]] virtual bvt add_addr(const exprt &);
 
   // overloading
   literalt convert_rest(const exprt &) override;
@@ -66,19 +64,16 @@ class bv_pointers_widet : public boolbvt
   exprt
   bv_get_rec(const exprt &, const bvt &, std::size_t offset) const override;
 
-  NODISCARD
-  optionalt<bvt> convert_address_of_rec(const exprt &);
+  [[nodiscard]] optionalt<bvt> convert_address_of_rec(const exprt &);
 
-  NODISCARD
-  bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &);
-  NODISCARD
-  bvt offset_arithmetic(
+  [[nodiscard]] bvt
+  offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &);
+  [[nodiscard]] bvt offset_arithmetic(
     const pointer_typet &,
     const bvt &,
     const mp_integer &factor,
     const exprt &index);
-  NODISCARD
-  bvt offset_arithmetic(
+  [[nodiscard]] bvt offset_arithmetic(
     const pointer_typet &,
     const bvt &,
     const mp_integer &factor,
diff --git a/src/goto-programs/link_goto_model.h b/src/goto-programs/link_goto_model.h
index 9a49636a467..cf37cfe4dba 100644
--- a/src/goto-programs/link_goto_model.h
+++ b/src/goto-programs/link_goto_model.h
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H
 #define CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H
 
-#include <util/nodiscard.h>
 #include <util/replace_symbol.h>
 
 class goto_modelt;
@@ -23,7 +22,7 @@ class message_handlert;
 /// which need to be applied using \ref finalize_linking.
 /// \return nullopt if linking fails, else a (possibly empty) collection of
 ///   replacements to be applied.
-NODISCARD optionalt<replace_symbolt::expr_mapt>
+[[nodiscard]] optionalt<replace_symbolt::expr_mapt>
 link_goto_model(goto_modelt &dest, goto_modelt &&src, message_handlert &);
 
 /// Apply \p type_updates to \p dest, where \p type_updates were constructed
diff --git a/src/goto-symex/field_sensitivity.h b/src/goto-symex/field_sensitivity.h
index 9de75a903ff..5fa0fe79b8d 100644
--- a/src/goto-symex/field_sensitivity.h
+++ b/src/goto-symex/field_sensitivity.h
@@ -9,7 +9,6 @@ Author: Michael Tautschnig
 #ifndef CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
 #define CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
 
-#include <util/nodiscard.h>
 #include <util/ssa_expr.h>
 
 class namespacet;
@@ -158,13 +157,11 @@ class field_sensitivityt
   /// \param expr: an expression to be (recursively) transformed.
   /// \param write: set to true if the expression is to be used as an lvalue.
   /// \return the transformed expression
-  NODISCARD
-  exprt
+  [[nodiscard]] exprt
   apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write)
     const;
   /// \copydoc apply(const namespacet&,goto_symex_statet&,exprt,bool) const
-  NODISCARD
-  exprt apply(
+  [[nodiscard]] exprt apply(
     const namespacet &ns,
     goto_symex_statet &state,
     ssa_exprt expr,
@@ -182,8 +179,7 @@ class field_sensitivityt
   /// \return Expanded expression; for example, for a \p ssa_expr of some struct
   ///   type, a `struct_exprt` with each component now being an SSA expression
   ///   is built.
-  NODISCARD
-  exprt get_fields(
+  [[nodiscard]] exprt get_fields(
     const namespacet &ns,
     goto_symex_statet &state,
     const ssa_exprt &ssa_expr,
@@ -198,8 +194,8 @@ class field_sensitivityt
   ///   (`true`)
   /// \return False, if and only if, \p expr would be a single field-sensitive
   /// SSA expression.
-  NODISCARD
-  bool is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const;
+  [[nodiscard]] bool
+  is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const;
 
 private:
   const std::size_t max_field_sensitivity_array_size;
@@ -214,8 +210,7 @@ class field_sensitivityt
     symex_targett &target,
     bool allow_pointer_unsoundness) const;
 
-  NODISCARD
-  exprt simplify_opt(exprt e, const namespacet &ns) const;
+  [[nodiscard]] exprt simplify_opt(exprt e, const namespacet &ns) const;
 };
 
 #endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 186e35ac5ae..72de8769922 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -112,8 +112,7 @@ class goto_symext
   /// \param fields The shadow memory field declarations
   /// \return A symbol table holding the symbols added during symbolic
   ///   execution.
-  NODISCARD
-  virtual symbol_tablet symex_from_entry_point_of(
+  [[nodiscard]] virtual symbol_tablet symex_from_entry_point_of(
     const get_goto_functiont &get_goto_function,
     const shadow_memory_field_definitionst &fields);
 
@@ -138,8 +137,7 @@ class goto_symext
   /// \param saved_equation: The equation as previously built up
   /// \return A symbol table holding the symbols added during symbolic
   ///   execution.
-  NODISCARD
-  virtual symbol_tablet resume_symex_from_saved_state(
+  [[nodiscard]] virtual symbol_tablet resume_symex_from_saved_state(
     const get_goto_functiont &get_goto_function,
     const statet &saved_state,
     symex_target_equationt *saved_equation);
@@ -156,8 +154,7 @@ class goto_symext
   ///   execute
   /// \return A symbol table holding the symbols added during symbolic
   ///   execution.
-  NODISCARD
-  virtual symbol_tablet
+  [[nodiscard]] virtual symbol_tablet
   symex_with_state(statet &state, const get_goto_functiont &get_goto_functions);
 
   /// \brief Set when states are pushed onto the workqueue
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index 6bfe8652304..fa7c06895f5 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
 
 #include <util/invariant.h>
-#include <util/nodiscard.h>
 #include <util/ssa_expr.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
@@ -98,21 +97,21 @@ class goto_symex_statet final : public goto_statet
   /// A full explanation of SSA (which is why we do this renaming) is in
   /// the SSA section of background-concepts.md.
   template <levelt level = L2>
-  NODISCARD renamedt<exprt, level> rename(exprt expr, const namespacet &ns);
+  [[nodiscard]] renamedt<exprt, level> rename(exprt expr, const namespacet &ns);
 
   /// Version of rename which is specialized for SSA exprt.
   /// Implementation only exists for level L0 and L1.
   template <levelt level>
-  NODISCARD renamedt<ssa_exprt, level>
+  [[nodiscard]] renamedt<ssa_exprt, level>
   rename_ssa(ssa_exprt ssa, const namespacet &ns);
 
   template <levelt level = L2>
   void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns);
 
-  NODISCARD exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns);
+  [[nodiscard]] exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns);
 
   /// \return lhs renamed to level 2
-  NODISCARD renamedt<ssa_exprt, L2> assignment(
+  [[nodiscard]] renamedt<ssa_exprt, L2> assignment(
     ssa_exprt lhs,    // L0/L1
     const exprt &rhs, // L2
     const namespacet &ns,
@@ -130,7 +129,7 @@ class goto_symex_statet final : public goto_statet
 
   /// Update values up to \c level.
   template <levelt level>
-  NODISCARD renamedt<ssa_exprt, level>
+  [[nodiscard]] renamedt<ssa_exprt, level>
   set_indices(ssa_exprt expr, const namespacet &ns);
 
   // this maps L1 names to (L2) types
diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp
index 4dba867e25a..7806a720269 100644
--- a/src/goto-symex/symex_clean_expr.cpp
+++ b/src/goto-symex/symex_clean_expr.cpp
@@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/expr_iterator.h>
-#include <util/nodiscard.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
 
@@ -228,7 +227,7 @@ void goto_symext::lift_lets(statet &state, exprt &rhs)
   }
 }
 
-NODISCARD exprt
+[[nodiscard]] exprt
 goto_symext::clean_expr(exprt expr, statet &state, const bool write)
 {
   replace_nondet(expr, path_storage.build_symex_nondet);
diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h
index e165c510d79..151a1205c63 100644
--- a/src/solvers/flattening/bv_pointers.h
+++ b/src/solvers/flattening/bv_pointers.h
@@ -10,8 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
 #define CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
 
-#include <util/nodiscard.h>
-
 #include "boolbv.h"
 #include "pointer_logic.h"
 
@@ -39,13 +37,12 @@ class bv_pointerst:public boolbvt
   // NOLINTNEXTLINE(readability/identifiers)
   typedef boolbvt SUB;
 
-  NODISCARD
-  bvt encode(const mp_integer &object, const pointer_typet &) const;
+  [[nodiscard]] bvt
+  encode(const mp_integer &object, const pointer_typet &) const;
 
   virtual bvt convert_pointer_type(const exprt &);
 
-  NODISCARD
-  virtual bvt add_addr(const exprt &);
+  [[nodiscard]] virtual bvt add_addr(const exprt &);
 
   // overloading
   literalt convert_rest(const exprt &) override;
@@ -54,25 +51,21 @@ class bv_pointerst:public boolbvt
   exprt
   bv_get_rec(const exprt &, const bvt &, std::size_t offset) const override;
 
-  NODISCARD
-  optionalt<bvt> convert_address_of_rec(const exprt &);
+  [[nodiscard]] optionalt<bvt> convert_address_of_rec(const exprt &);
 
-  NODISCARD
-  bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &);
-  NODISCARD
-  bvt offset_arithmetic(
+  [[nodiscard]] bvt
+  offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &);
+  [[nodiscard]] bvt offset_arithmetic(
     const pointer_typet &,
     const bvt &,
     const mp_integer &factor,
     const exprt &index);
-  NODISCARD
-  bvt offset_arithmetic(
+  [[nodiscard]] bvt offset_arithmetic(
     const pointer_typet &type,
     const bvt &bv,
     const exprt &factor,
     const exprt &index);
-  NODISCARD
-  bvt offset_arithmetic(
+  [[nodiscard]] bvt offset_arithmetic(
     const pointer_typet &,
     const bvt &,
     const mp_integer &factor,
diff --git a/src/solvers/flattening/bv_utils.h b/src/solvers/flattening/bv_utils.h
index ba0352bf17c..a9a195257a6 100644
--- a/src/solvers/flattening/bv_utils.h
+++ b/src/solvers/flattening/bv_utils.h
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_SOLVERS_FLATTENING_BV_UTILS_H
 
 #include <util/mp_arith.h>
-#include <util/nodiscard.h>
 
 #include <solvers/prop/prop.h>
 
@@ -224,16 +223,16 @@ class bv_utilst
 
   /// Return the sum and carry-out when adding \p op0 and \p op1 under initial
   /// carry \p carry_in.
-  NODISCARD std::pair<bvt, literalt>
+  [[nodiscard]] std::pair<bvt, literalt>
   adder(const bvt &op0, const bvt &op1, literalt carry_in);
 
-  NODISCARD bvt adder_no_overflow(
+  [[nodiscard]] bvt adder_no_overflow(
     const bvt &op0,
     const bvt &op1,
     bool subtract,
     representationt rep);
 
-  NODISCARD bvt adder_no_overflow(const bvt &op0, const bvt &op1);
+  [[nodiscard]] bvt adder_no_overflow(const bvt &op0, const bvt &op1);
 
   bvt unsigned_multiplier_no_overflow(
     const bvt &op0, const bvt &op1);
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 8ce9f6e3e96..4c975f192f9 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -6,7 +6,6 @@
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/namespace.h>
-#include <util/nodiscard.h>
 #include <util/range.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
@@ -663,8 +662,8 @@ void smt2_incremental_decision_proceduret::pop()
   UNIMPLEMENTED_FEATURE("`pop`.");
 }
 
-NODISCARD
-static decision_proceduret::resultt lookup_decision_procedure_result(
+[[nodiscard]] static decision_proceduret::resultt
+lookup_decision_procedure_result(
   const smt_check_sat_response_kindt &response_kind)
 {
   if(response_kind.cast<smt_sat_responset>())
@@ -716,6 +715,7 @@ decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
   {
     if(check_sat_response->kind().cast<smt_unknown_responset>())
       log.error() << "SMT2 solver returned \"unknown\"" << messaget::eom;
+    lookup_decision_procedure_result(check_sat_response->kind());
     return lookup_decision_procedure_result(check_sat_response->kind());
   }
   if(const auto problem = get_problem_messages(result))
diff --git a/src/solvers/smt2_incremental/smt_response_validation.h b/src/solvers/smt2_incremental/smt_response_validation.h
index 4fbfbd7dc7f..609311cfbfc 100644
--- a/src/solvers/smt2_incremental/smt_response_validation.h
+++ b/src/solvers/smt2_incremental/smt_response_validation.h
@@ -3,12 +3,10 @@
 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSE_VALIDATION_H
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSE_VALIDATION_H
 
-#include <util/nodiscard.h>
-
 #include <solvers/smt2_incremental/ast/smt_responses.h> // IWYU pragma: keep
 #include <solvers/smt2_incremental/response_or_error.h>
 
-NODISCARD response_or_errort<smt_responset> validate_smt_response(
+[[nodiscard]] response_or_errort<smt_responset> validate_smt_response(
   const irept &parse_tree,
   const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table);
 
diff --git a/src/solvers/strings/string_dependencies.h b/src/solvers/strings/string_dependencies.h
index 03a455117eb..624ab59c5a8 100644
--- a/src/solvers/strings/string_dependencies.h
+++ b/src/solvers/strings/string_dependencies.h
@@ -14,8 +14,6 @@ Author: Diffblue Ltd.
 
 #include <memory>
 
-#include <util/nodiscard.h>
-
 #include "string_builtin_function.h"
 
 /// Keep track of dependencies between strings.
@@ -115,7 +113,7 @@ class string_dependenciest
   /// For all builtin call on which a test (or an unsupported buitin)
   /// result depends, add the corresponding constraints. For the other builtin
   /// only add constraints on the length.
-  NODISCARD string_constraintst add_constraints(
+  [[nodiscard]] string_constraintst add_constraints(
     string_constraint_generatort &generatort,
     message_handlert &message_handler);
 
diff --git a/src/util/interval_union.h b/src/util/interval_union.h
index b04cb605e77..d4ddf1aee93 100644
--- a/src/util/interval_union.h
+++ b/src/util/interval_union.h
@@ -14,7 +14,6 @@ Author: Diffblue Limited
 
 #include <util/interval_template.h>
 #include <util/mp_arith.h>
-#include <util/nodiscard.h>
 #include <util/optional.h>
 #include <vector>
 
@@ -44,12 +43,12 @@ class interval_uniont
 
   /// Return a new interval_uniontt object representing the set of intergers in
   /// the intersection of this object and \p other.
-  NODISCARD interval_uniont
+  [[nodiscard]] interval_uniont
   make_intersection(const interval_uniont &other) const;
 
   /// Return a new interval_uniontt object representing the set of intergers in
   /// the union of this object and \p other.
-  NODISCARD interval_uniont make_union(const interval_uniont &other) const;
+  [[nodiscard]] interval_uniont make_union(const interval_uniont &other) const;
 
   bool is_empty() const;
 
diff --git a/src/util/nodiscard.h b/src/util/nodiscard.h
deleted file mode 100644
index 55ab4030fd3..00000000000
--- a/src/util/nodiscard.h
+++ /dev/null
@@ -1,25 +0,0 @@
-/*******************************************************************\
-
-Module: Util
-
-Author: Diffblue Ltd.
-
-\*******************************************************************/
-
-#ifndef CPROVER_UTIL_NODISCARD_H
-#define CPROVER_UTIL_NODISCARD_H
-
-#if __has_cpp_attribute(nodiscard)
-#  ifdef __clang__
-#    pragma GCC diagnostic ignored "-Wc++1z-extensions"
-#  endif
-// NOLINTNEXTLINE(whitespace/braces)
-#  define NODISCARD [[nodiscard]]
-#elif __has_cpp_attribute(gnu::warn_unused_result)
-// NOLINTNEXTLINE(whitespace/braces)
-#  define NODISCARD [[gnu::warn_unused_result]]
-#else
-#  define NODISCARD
-#endif
-
-#endif // CPROVER_UTIL_NODISCARD_H
diff --git a/src/util/piped_process.cpp b/src/util/piped_process.cpp
index f5b028ae2f6..2e499e03b67 100644
--- a/src/util/piped_process.cpp
+++ b/src/util/piped_process.cpp
@@ -344,8 +344,8 @@ piped_processt::~piped_processt()
 #  endif
 }
 
-NODISCARD
-piped_processt::send_responset piped_processt::send(const std::string &message)
+[[nodiscard]] piped_processt::send_responset
+piped_processt::send(const std::string &message)
 {
   if(process_state != statet::RUNNING)
   {
diff --git a/src/util/piped_process.h b/src/util/piped_process.h
index 01815aa9ea0..c95e4b14b21 100644
--- a/src/util/piped_process.h
+++ b/src/util/piped_process.h
@@ -14,7 +14,6 @@ typedef void *HANDLE;                                    // NOLINT
 #endif
 
 #include "message.h"
-#include "nodiscard.h"
 #include "optional.h"
 
 #include <vector>
@@ -45,7 +44,7 @@ class piped_processt
   /// Send a string message (command) to the child process.
   /// \param message The string message to be sent.
   /// \return
-  NODISCARD send_responset send(const std::string &message);
+  [[nodiscard]] send_responset send(const std::string &message);
   /// Read a string from the child process' output.
   /// \return a string containing data from the process, empty string if no data
   std::string receive();
diff --git a/src/util/rename.h b/src/util/rename.h
index 1c7c1d97239..b60f472ca74 100644
--- a/src/util/rename.h
+++ b/src/util/rename.h
@@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 //
 
 #include "irep.h"
-#include "nodiscard.h"
 
 class namespacet;
 
@@ -26,7 +25,7 @@ class namespacet;
 /// \param delimiter: character to separate the name and a newly generated
 ///   suffix
 /// \return Identifier that is not yet part of the namespace.
-NODISCARD irep_idt
+[[nodiscard]] irep_idt
 get_new_name(const irep_idt &name, const namespacet &ns, char delimiter = '_');
 
 #endif // CPROVER_UTIL_RENAME_H
diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h
index 4b08396c190..2e7341be03b 100644
--- a/src/util/simplify_expr_class.h
+++ b/src/util/simplify_expr_class.h
@@ -19,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "expr.h"
 #include "mp_arith.h"
-#include "nodiscard.h"
 #include "type.h"
 // #define USE_LOCAL_REPLACE_MAP
 #ifdef USE_LOCAL_REPLACE_MAP
@@ -135,12 +134,12 @@ class simplify_exprt
     }
   };
 
-  NODISCARD static resultt<> unchanged(exprt expr)
+  [[nodiscard]] static resultt<> unchanged(exprt expr)
   {
     return resultt<>(resultt<>::UNCHANGED, std::move(expr));
   }
 
-  NODISCARD static resultt<> changed(resultt<> result)
+  [[nodiscard]] static resultt<> changed(resultt<> result)
   {
     result.expr_changed = resultt<>::CHANGED;
     return result;
@@ -148,101 +147,105 @@ class simplify_exprt
 
   // These below all return 'true' if the simplification wasn't applicable.
   // If false is returned, the expression has changed.
-  NODISCARD resultt<> simplify_typecast(const typecast_exprt &);
-  NODISCARD resultt<> simplify_typecast_preorder(const typecast_exprt &);
-  NODISCARD resultt<> simplify_extractbit(const extractbit_exprt &);
-  NODISCARD resultt<> simplify_extractbits(const extractbits_exprt &);
-  NODISCARD resultt<> simplify_concatenation(const concatenation_exprt &);
-  NODISCARD resultt<> simplify_mult(const mult_exprt &);
-  NODISCARD resultt<> simplify_div(const div_exprt &);
-  NODISCARD resultt<> simplify_mod(const mod_exprt &);
-  NODISCARD resultt<> simplify_plus(const plus_exprt &);
-  NODISCARD resultt<> simplify_minus(const minus_exprt &);
-  NODISCARD resultt<> simplify_floatbv_op(const ieee_float_op_exprt &);
-  NODISCARD resultt<> simplify_floatbv_typecast(const floatbv_typecast_exprt &);
-  NODISCARD resultt<> simplify_shifts(const shift_exprt &);
-  NODISCARD resultt<> simplify_power(const binary_exprt &);
-  NODISCARD resultt<> simplify_bitwise(const multi_ary_exprt &);
-  NODISCARD resultt<> simplify_if_preorder(const if_exprt &expr);
-  NODISCARD resultt<> simplify_if(const if_exprt &);
-  NODISCARD resultt<> simplify_bitnot(const bitnot_exprt &);
-  NODISCARD resultt<> simplify_not(const not_exprt &);
-  NODISCARD resultt<> simplify_boolean(const exprt &);
-  NODISCARD resultt<> simplify_inequality(const binary_relation_exprt &);
-  NODISCARD resultt<>
+  [[nodiscard]] resultt<> simplify_typecast(const typecast_exprt &);
+  [[nodiscard]] resultt<> simplify_typecast_preorder(const typecast_exprt &);
+  [[nodiscard]] resultt<> simplify_extractbit(const extractbit_exprt &);
+  [[nodiscard]] resultt<> simplify_extractbits(const extractbits_exprt &);
+  [[nodiscard]] resultt<> simplify_concatenation(const concatenation_exprt &);
+  [[nodiscard]] resultt<> simplify_mult(const mult_exprt &);
+  [[nodiscard]] resultt<> simplify_div(const div_exprt &);
+  [[nodiscard]] resultt<> simplify_mod(const mod_exprt &);
+  [[nodiscard]] resultt<> simplify_plus(const plus_exprt &);
+  [[nodiscard]] resultt<> simplify_minus(const minus_exprt &);
+  [[nodiscard]] resultt<> simplify_floatbv_op(const ieee_float_op_exprt &);
+  [[nodiscard]] resultt<>
+  simplify_floatbv_typecast(const floatbv_typecast_exprt &);
+  [[nodiscard]] resultt<> simplify_shifts(const shift_exprt &);
+  [[nodiscard]] resultt<> simplify_power(const binary_exprt &);
+  [[nodiscard]] resultt<> simplify_bitwise(const multi_ary_exprt &);
+  [[nodiscard]] resultt<> simplify_if_preorder(const if_exprt &expr);
+  [[nodiscard]] resultt<> simplify_if(const if_exprt &);
+  [[nodiscard]] resultt<> simplify_bitnot(const bitnot_exprt &);
+  [[nodiscard]] resultt<> simplify_not(const not_exprt &);
+  [[nodiscard]] resultt<> simplify_boolean(const exprt &);
+  [[nodiscard]] resultt<> simplify_inequality(const binary_relation_exprt &);
+  [[nodiscard]] resultt<>
   simplify_ieee_float_relation(const binary_relation_exprt &);
-  NODISCARD resultt<> simplify_lambda(const lambda_exprt &);
-  NODISCARD resultt<> simplify_with(const with_exprt &);
-  NODISCARD resultt<> simplify_update(const update_exprt &);
-  NODISCARD resultt<> simplify_index(const index_exprt &);
-  NODISCARD resultt<> simplify_index_preorder(const index_exprt &);
-  NODISCARD resultt<> simplify_member(const member_exprt &);
-  NODISCARD resultt<> simplify_member_preorder(const member_exprt &);
-  NODISCARD resultt<> simplify_byte_update(const byte_update_exprt &);
-  NODISCARD resultt<> simplify_byte_extract(const byte_extract_exprt &);
-  NODISCARD resultt<>
+  [[nodiscard]] resultt<> simplify_lambda(const lambda_exprt &);
+  [[nodiscard]] resultt<> simplify_with(const with_exprt &);
+  [[nodiscard]] resultt<> simplify_update(const update_exprt &);
+  [[nodiscard]] resultt<> simplify_index(const index_exprt &);
+  [[nodiscard]] resultt<> simplify_index_preorder(const index_exprt &);
+  [[nodiscard]] resultt<> simplify_member(const member_exprt &);
+  [[nodiscard]] resultt<> simplify_member_preorder(const member_exprt &);
+  [[nodiscard]] resultt<> simplify_byte_update(const byte_update_exprt &);
+  [[nodiscard]] resultt<> simplify_byte_extract(const byte_extract_exprt &);
+  [[nodiscard]] resultt<>
   simplify_byte_extract_preorder(const byte_extract_exprt &);
-  NODISCARD resultt<> simplify_pointer_object(const pointer_object_exprt &);
-  NODISCARD resultt<>
+  [[nodiscard]] resultt<> simplify_pointer_object(const pointer_object_exprt &);
+  [[nodiscard]] resultt<>
   simplify_unary_pointer_predicate_preorder(const unary_exprt &);
-  NODISCARD resultt<> simplify_object_size(const object_size_exprt &);
-  NODISCARD resultt<> simplify_is_dynamic_object(const unary_exprt &);
-  NODISCARD resultt<> simplify_is_invalid_pointer(const unary_exprt &);
-  NODISCARD resultt<> simplify_object(const exprt &);
-  NODISCARD resultt<> simplify_unary_minus(const unary_minus_exprt &);
-  NODISCARD resultt<> simplify_unary_plus(const unary_plus_exprt &);
-  NODISCARD resultt<> simplify_dereference(const dereference_exprt &);
-  NODISCARD resultt<> simplify_dereference_preorder(const dereference_exprt &);
-  NODISCARD resultt<> simplify_address_of(const address_of_exprt &);
-  NODISCARD resultt<> simplify_pointer_offset(const pointer_offset_exprt &);
-  NODISCARD resultt<> simplify_bswap(const bswap_exprt &);
-  NODISCARD resultt<> simplify_isinf(const unary_exprt &);
-  NODISCARD resultt<> simplify_isnan(const unary_exprt &);
-  NODISCARD resultt<> simplify_isnormal(const unary_exprt &);
-  NODISCARD resultt<> simplify_abs(const abs_exprt &);
-  NODISCARD resultt<> simplify_sign(const sign_exprt &);
-  NODISCARD resultt<> simplify_popcount(const popcount_exprt &);
-  NODISCARD resultt<> simplify_complex(const unary_exprt &);
+  [[nodiscard]] resultt<> simplify_object_size(const object_size_exprt &);
+  [[nodiscard]] resultt<> simplify_is_dynamic_object(const unary_exprt &);
+  [[nodiscard]] resultt<> simplify_is_invalid_pointer(const unary_exprt &);
+  [[nodiscard]] resultt<> simplify_object(const exprt &);
+  [[nodiscard]] resultt<> simplify_unary_minus(const unary_minus_exprt &);
+  [[nodiscard]] resultt<> simplify_unary_plus(const unary_plus_exprt &);
+  [[nodiscard]] resultt<> simplify_dereference(const dereference_exprt &);
+  [[nodiscard]] resultt<>
+  simplify_dereference_preorder(const dereference_exprt &);
+  [[nodiscard]] resultt<> simplify_address_of(const address_of_exprt &);
+  [[nodiscard]] resultt<> simplify_pointer_offset(const pointer_offset_exprt &);
+  [[nodiscard]] resultt<> simplify_bswap(const bswap_exprt &);
+  [[nodiscard]] resultt<> simplify_isinf(const unary_exprt &);
+  [[nodiscard]] resultt<> simplify_isnan(const unary_exprt &);
+  [[nodiscard]] resultt<> simplify_isnormal(const unary_exprt &);
+  [[nodiscard]] resultt<> simplify_abs(const abs_exprt &);
+  [[nodiscard]] resultt<> simplify_sign(const sign_exprt &);
+  [[nodiscard]] resultt<> simplify_popcount(const popcount_exprt &);
+  [[nodiscard]] resultt<> simplify_complex(const unary_exprt &);
 
   /// Try to simplify overflow-+, overflow-*, overflow--, overflow-shl.
   /// Simplification will be possible when the operands are constants or the
   /// types of the operands have infinite domains.
-  NODISCARD resultt<> simplify_overflow_binary(const binary_overflow_exprt &);
+  [[nodiscard]] resultt<>
+  simplify_overflow_binary(const binary_overflow_exprt &);
 
   /// Try to simplify overflow-unary-.
   /// Simplification will be possible when the operand is constants or the
   /// type of the operand has an infinite domain.
-  NODISCARD resultt<> simplify_overflow_unary(const unary_overflow_exprt &);
+  [[nodiscard]] resultt<> simplify_overflow_unary(const unary_overflow_exprt &);
 
   /// Try to simplify overflow_result-+, overflow_result-*, overflow_result--,
   /// overflow_result-shl, overflow_result-unary--.
   /// Simplification will be possible when the operands are constants or the
   /// types of the operands have infinite domains.
-  NODISCARD resultt<> simplify_overflow_result(const overflow_result_exprt &);
+  [[nodiscard]] resultt<>
+  simplify_overflow_result(const overflow_result_exprt &);
 
   /// Attempt to simplify mathematical function applications if we have
   /// enough information to do so. Currently focused on constant comparisons.
-  NODISCARD resultt<>
+  [[nodiscard]] resultt<>
   simplify_function_application(const function_application_exprt &);
 
   /// Try to simplify count-leading-zeros to a constant expression.
-  NODISCARD resultt<> simplify_clz(const count_leading_zeros_exprt &);
+  [[nodiscard]] resultt<> simplify_clz(const count_leading_zeros_exprt &);
 
   /// Try to simplify count-trailing-zeros to a constant expression.
-  NODISCARD resultt<> simplify_ctz(const count_trailing_zeros_exprt &);
+  [[nodiscard]] resultt<> simplify_ctz(const count_trailing_zeros_exprt &);
 
   /// Try to simplify bit-reversing to a constant expression.
-  NODISCARD resultt<> simplify_bitreverse(const bitreverse_exprt &);
+  [[nodiscard]] resultt<> simplify_bitreverse(const bitreverse_exprt &);
 
   /// Try to simplify find-first-set to a constant expression.
-  NODISCARD resultt<> simplify_ffs(const find_first_set_exprt &);
+  [[nodiscard]] resultt<> simplify_ffs(const find_first_set_exprt &);
 
   /// Try to simplify prophecy_{r,w,rw}_ok to a constant expression.
-  NODISCARD resultt<>
+  [[nodiscard]] resultt<>
   simplify_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &);
 
   /// Try to simplify prophecy_pointer_in_range to a constant expression.
-  NODISCARD resultt<>
+  [[nodiscard]] resultt<>
   simplify_prophecy_pointer_in_range(const prophecy_pointer_in_range_exprt &);
 
   // auxiliary
@@ -253,22 +256,22 @@ class simplify_exprt
   bool simplify_if_disj(exprt &expr, const exprt &cond);
   bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond);
   bool simplify_if_cond(exprt &expr);
-  NODISCARD resultt<> simplify_address_of_arg(const exprt &);
-  NODISCARD resultt<>
+  [[nodiscard]] resultt<> simplify_address_of_arg(const exprt &);
+  [[nodiscard]] resultt<>
   simplify_inequality_both_constant(const binary_relation_exprt &);
-  NODISCARD resultt<>
+  [[nodiscard]] resultt<>
   simplify_inequality_no_constant(const binary_relation_exprt &);
-  NODISCARD resultt<>
+  [[nodiscard]] resultt<>
   simplify_inequality_rhs_is_constant(const binary_relation_exprt &);
-  NODISCARD resultt<>
+  [[nodiscard]] resultt<>
   simplify_inequality_address_of(const binary_relation_exprt &);
-  NODISCARD resultt<>
+  [[nodiscard]] resultt<>
   simplify_inequality_pointer_object(const binary_relation_exprt &);
 
   // main recursion
-  NODISCARD resultt<> simplify_node(const exprt &);
-  NODISCARD resultt<> simplify_node_preorder(const exprt &);
-  NODISCARD resultt<> simplify_rec(const exprt &);
+  [[nodiscard]] resultt<> simplify_node(const exprt &);
+  [[nodiscard]] resultt<> simplify_node_preorder(const exprt &);
+  [[nodiscard]] resultt<> simplify_rec(const exprt &);
 
   virtual bool simplify(exprt &expr);