diff --git a/src/util/expr_cast.h b/src/util/expr_cast.h
new file mode 100644
index 00000000000..e5cc222c49a
--- /dev/null
+++ b/src/util/expr_cast.h
@@ -0,0 +1,172 @@
+/*******************************************************************\
+
+Module:
+
+Author: Nathan Phillips <Nathan.Phillips@diffblue.com>
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_EXPR_CAST_H
+#define CPROVER_UTIL_EXPR_CAST_H
+
+/// \file util/expr_cast.h
+/// \brief Templated functions to cast to specific exprt-derived classes
+
+#include <typeinfo>
+#include <type_traits>
+#include <functional>
+
+#include "invariant.h"
+#include "expr.h"
+#include "optional.h"
+
+/// \brief Check whether a reference to a generic \ref exprt is of a specific
+///   derived class.
+///
+///   Implement template specializations of this function to enable casting
+///
+/// \tparam T The exprt-derived class to check for
+/// \param base Reference to a generic \ref exprt
+/// \return true if \a base is of type \a T
+template<typename T> bool can_cast_expr(const exprt &base);
+
+
+/// \brief Try to cast a constant reference to a generic exprt to a specific
+///   derived class
+/// \tparam T The exprt-derived class to cast to
+/// \param base Reference to a generic \ref exprt
+/// \return Reference to object of type \a T or valueless optional if \a base
+///   is not an instance of \a T
+template<typename T>
+optionalt<std::reference_wrapper<typename std::remove_reference<T>::type>>
+expr_try_dynamic_cast(const exprt &base)
+{
+  return expr_try_dynamic_cast<
+    T,
+    typename std::remove_reference<T>::type,
+    typename std::remove_const<typename std::remove_reference<T>::type>::type,
+    const exprt>(base);
+}
+
+/// \brief Try to cast a reference to a generic exprt to a specific derived
+///   class
+/// \tparam T The exprt-derived class to cast to
+/// \param base Reference to a generic \ref exprt
+/// \return Reference to object of type \a T or valueless optional if \a base is
+///   not an instance of \a T
+template<typename T>
+optionalt<std::reference_wrapper<typename std::remove_reference<T>::type>>
+expr_try_dynamic_cast(exprt &base)
+{
+  return expr_try_dynamic_cast<
+    T,
+    typename std::remove_reference<T>::type,
+    typename std::remove_const<typename std::remove_reference<T>::type>::type,
+    exprt>(base);
+}
+
+/// \brief Try to cast a reference to a generic exprt to a specific derived
+///    class
+/// \tparam T The reference or const reference type to \a TUnderlying to cast
+///    to
+/// \tparam TUnderlying An exprt-derived class type
+/// \tparam TExpr The original type to cast from, either exprt or const exprt
+/// \param base Reference to a generic \ref exprt
+/// \return Reference to object of type \a TUnderlying
+///   or valueless optional if \a base is not an instance of \a TUnderlying
+template<typename T, typename TConst, typename TUnderlying, typename TExpr>
+optionalt<std::reference_wrapper<TConst>> expr_try_dynamic_cast(TExpr &base)
+{
+  static_assert(
+    std::is_same<typename std::remove_const<TExpr>::type, exprt>::value,
+    "Tried to expr_try_dynamic_cast from something that wasn't an exprt");
+  static_assert(
+    std::is_reference<T>::value,
+    "Tried to convert exprt & to non-reference type");
+  static_assert(
+    std::is_base_of<exprt, TUnderlying>::value,
+    "The template argument T must be derived from exprt.");
+  if(!can_cast_expr<TUnderlying>(base))
+    return optionalt<std::reference_wrapper<TConst>>();
+  T value=static_cast<T>(base);
+  validate_expr(value);
+  return optionalt<std::reference_wrapper<TConst>>(value);
+}
+
+/// \brief Cast a constant reference to a generic exprt to a specific derived
+///   class
+/// \tparam T The exprt-derived class to cast to
+/// \param base Reference to a generic \ref exprt
+/// \return Reference to object of type \a T
+/// \throw std::bad_cast If \a base is not an instance of \a T
+/// \remark If CBMC assertions (PRECONDITION) are set to abort then this will
+///   abort rather than throw if \a base is not an instance of \a T
+template<typename T>
+T expr_dynamic_cast(const exprt &base)
+{
+  return expr_dynamic_cast<
+    T,
+    typename std::remove_const<typename std::remove_reference<T>::type>::type,
+    const exprt>(base);
+}
+
+/// \brief Cast a reference to a generic exprt to a specific derived class
+/// \tparam T The exprt-derived class to cast to
+/// \param base Reference to a generic \ref exprt
+/// \return Reference to object of type \a T
+/// \throw std::bad_cast If \a base is not an instance of \a T
+/// \remark If CBMC assertions (PRECONDITION) are set to abort then this will
+///   abort rather than throw if \a base is not an instance of \a T
+template<typename T>
+T expr_dynamic_cast(exprt &base)
+{
+  return expr_dynamic_cast<
+    T,
+    typename std::remove_const<typename std::remove_reference<T>::type>::type,
+    exprt>(base);
+}
+
+/// \brief Cast a reference to a generic exprt to a specific derived class
+/// \tparam T The reference or const reference type to \a TUnderlying to cast to
+/// \tparam TUnderlying An exprt-derived class type
+/// \tparam TExpr The original type to cast from, either exprt or const exprt
+/// \param base Reference to a generic \ref exprt
+/// \return Reference to object of type \a T
+/// \throw std::bad_cast If \a base is not an instance of \a TUnderlying
+/// \remark If CBMC assertions (PRECONDITION) are set to abort then this will
+///   abort rather than throw if \a base is not an instance of \a TUnderlying
+template<typename T, typename TUnderlying, typename TExpr>
+T expr_dynamic_cast(TExpr &base)
+{
+  static_assert(
+    std::is_same<typename std::remove_const<TExpr>::type, exprt>::value,
+    "Tried to expr_dynamic_cast from something that wasn't an exprt");
+  static_assert(
+    std::is_reference<T>::value,
+    "Tried to convert exprt & to non-reference type");
+  static_assert(
+    std::is_base_of<exprt, TUnderlying>::value,
+    "The template argument T must be derived from exprt.");
+  PRECONDITION(can_cast_expr<TUnderlying>(base));
+  if(!can_cast_expr<TUnderlying>(base))
+    throw std::bad_cast();
+  T value=static_cast<T>(base);
+  validate_expr(value);
+  return value;
+}
+
+
+inline void validate_operands(
+  const exprt &value,
+  exprt::operandst::size_type number,
+  const char *message,
+  bool allow_more=false)
+{
+  DATA_INVARIANT(
+    allow_more
+      ? value.operands().size()==number
+      : value.operands().size()>=number,
+    message);
+}
+
+#endif  // CPROVER_UTIL_EXPR_CAST_H
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index 3396398e73b..e1d6e06c912 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "invariant.h"
 #include "std_types.h"
+#include "expr_cast.h"
+
 
 /*! \defgroup gr_std_expr Conversion to specific expressions
  *  Conversion to subclasses of @ref exprt
@@ -77,6 +79,16 @@ inline transt &to_trans_expr(exprt &expr)
   return static_cast<transt &>(expr);
 }
 
+template<> inline bool can_cast_expr<transt>(const exprt &base)
+{
+  return base.id()==ID_trans;
+}
+inline void validate_expr(const transt &value)
+{
+  validate_operands(value, 3, "Transition systems must have three operands");
+}
+
+
 /*! \brief Expression to hold a symbol (variable)
 */
 class symbol_exprt:public exprt
@@ -216,6 +228,16 @@ inline symbol_exprt &to_symbol_expr(exprt &expr)
   return static_cast<symbol_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<symbol_exprt>(const exprt &base)
+{
+  return base.id()==ID_symbol;
+}
+inline void validate_expr(const symbol_exprt &value)
+{
+  validate_operands(value, 0, "Symbols must not have operands");
+}
+
+
 /*! \brief Generic base class for unary expressions
 */
 class unary_exprt:public exprt
@@ -295,6 +317,12 @@ inline unary_exprt &to_unary_expr(exprt &expr)
   return static_cast<unary_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<unary_exprt>(const exprt &base)
+{
+  return base.operands().size()==1;
+}
+
+
 /*! \brief absolute value
 */
 class abs_exprt:public unary_exprt
@@ -341,6 +369,16 @@ inline abs_exprt &to_abs_expr(exprt &expr)
   return static_cast<abs_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<abs_exprt>(const exprt &base)
+{
+  return base.id()==ID_abs;
+}
+inline void validate_expr(const abs_exprt &value)
+{
+  validate_operands(value, 1, "Absolute value must have one operand");
+}
+
+
 /*! \brief The unary minus expression
 */
 class unary_minus_exprt:public unary_exprt
@@ -394,6 +432,16 @@ inline unary_minus_exprt &to_unary_minus_expr(exprt &expr)
   return static_cast<unary_minus_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<unary_minus_exprt>(const exprt &base)
+{
+  return base.id()==ID_unary_minus;
+}
+inline void validate_expr(const unary_minus_exprt &value)
+{
+  validate_operands(value, 1, "Unary minus must have one operand");
+}
+
+
 /*! \brief A generic base class for expressions that are predicates,
            i.e., boolean-typed.
 */
@@ -540,6 +588,12 @@ inline binary_exprt &to_binary_expr(exprt &expr)
   return static_cast<binary_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<binary_exprt>(const exprt &base)
+{
+  return base.operands().size()==2;
+}
+
+
 /*! \brief A generic base class for expressions that are predicates,
            i.e., boolean-typed, and that take exactly two arguments.
 */
@@ -635,6 +689,12 @@ inline binary_relation_exprt &to_binary_relation_expr(exprt &expr)
   return static_cast<binary_relation_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<binary_relation_exprt>(const exprt &base)
+{
+  return can_cast_expr<binary_exprt>(base);
+}
+
+
 /*! \brief A generic base class for multi-ary expressions
 */
 class multi_ary_exprt:public exprt
@@ -697,6 +757,7 @@ inline multi_ary_exprt &to_multi_ary_expr(exprt &expr)
   return static_cast<multi_ary_exprt &>(expr);
 }
 
+
 /*! \brief The plus expression
 */
 class plus_exprt:public multi_ary_exprt
@@ -753,6 +814,16 @@ inline plus_exprt &to_plus_expr(exprt &expr)
   return static_cast<plus_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<plus_exprt>(const exprt &base)
+{
+  return base.id()==ID_plus;
+}
+inline void validate_expr(const plus_exprt &value)
+{
+  validate_operands(value, 2, "Plus must have two or more operands", true);
+}
+
+
 /*! \brief binary minus
 */
 class minus_exprt:public binary_exprt
@@ -801,6 +872,16 @@ inline minus_exprt &to_minus_expr(exprt &expr)
   return static_cast<minus_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<minus_exprt>(const exprt &base)
+{
+  return base.id()==ID_minus;
+}
+inline void validate_expr(const minus_exprt &value)
+{
+  validate_operands(value, 2, "Minus must have two or more operands", true);
+}
+
+
 /*! \brief binary multiplication
 */
 class mult_exprt:public multi_ary_exprt
@@ -849,6 +930,16 @@ inline mult_exprt &to_mult_expr(exprt &expr)
   return static_cast<mult_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<mult_exprt>(const exprt &base)
+{
+  return base.id()==ID_mult;
+}
+inline void validate_expr(const mult_exprt &value)
+{
+  validate_operands(value, 2, "Multiply must have two or more operands", true);
+}
+
+
 /*! \brief division (integer and real)
 */
 class div_exprt:public binary_exprt
@@ -897,6 +988,16 @@ inline div_exprt &to_div_expr(exprt &expr)
   return static_cast<div_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<div_exprt>(const exprt &base)
+{
+  return base.id()==ID_div;
+}
+inline void validate_expr(const div_exprt &value)
+{
+  validate_operands(value, 2, "Divide must have two operands");
+}
+
+
 /*! \brief binary modulo
 */
 class mod_exprt:public binary_exprt
@@ -941,6 +1042,16 @@ inline mod_exprt &to_mod_expr(exprt &expr)
   return static_cast<mod_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<mod_exprt>(const exprt &base)
+{
+  return base.id()==ID_mod;
+}
+inline void validate_expr(const mod_exprt &value)
+{
+  validate_operands(value, 2, "Modulo must have two operands");
+}
+
+
 /*! \brief remainder of division
 */
 class rem_exprt:public binary_exprt
@@ -985,6 +1096,16 @@ inline rem_exprt &to_rem_expr(exprt &expr)
   return static_cast<rem_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<rem_exprt>(const exprt &base)
+{
+  return base.id()==ID_rem;
+}
+inline void validate_expr(const rem_exprt &value)
+{
+  validate_operands(value, 2, "Remainder must have two operands");
+}
+
+
 /*! \brief exponentiation
  */
 class power_exprt:public binary_exprt
@@ -1029,6 +1150,16 @@ inline power_exprt &to_power_expr(exprt &expr)
   return static_cast<power_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<power_exprt>(const exprt &base)
+{
+  return base.id()==ID_power;
+}
+inline void validate_expr(const power_exprt &value)
+{
+  validate_operands(value, 2, "Power must have two operands");
+}
+
+
 /*! \brief falling factorial power
  */
 class factorial_power_exprt:public binary_exprt
@@ -1077,6 +1208,17 @@ inline factorial_power_exprt &to_factorial_expr(exprt &expr)
   return static_cast<factorial_power_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<factorial_power_exprt>(
+  const exprt &base)
+{
+  return base.id()==ID_factorial_power;
+}
+inline void validate_expr(const factorial_power_exprt &value)
+{
+  validate_operands(value, 2, "Factorial power must have two operands");
+}
+
+
 /*! \brief equality
 */
 class equal_exprt:public binary_relation_exprt
@@ -1119,6 +1261,16 @@ inline equal_exprt &to_equal_expr(exprt &expr)
   return static_cast<equal_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<equal_exprt>(const exprt &base)
+{
+  return base.id()==ID_equal;
+}
+inline void validate_expr(const equal_exprt &value)
+{
+  validate_operands(value, 2, "Equality must have two operands");
+}
+
+
 /*! \brief inequality
 */
 class notequal_exprt:public binary_relation_exprt
@@ -1165,6 +1317,16 @@ inline notequal_exprt &to_notequal_expr(exprt &expr)
   return static_cast<notequal_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<notequal_exprt>(const exprt &base)
+{
+  return base.id()==ID_notequal;
+}
+inline void validate_expr(const notequal_exprt &value)
+{
+  validate_operands(value, 2, "Inequality must have two operands");
+}
+
+
 /*! \brief array index operator
 */
 class index_exprt:public exprt
@@ -1247,6 +1409,16 @@ inline index_exprt &to_index_expr(exprt &expr)
   return static_cast<index_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<index_exprt>(const exprt &base)
+{
+  return base.id()==ID_index;
+}
+inline void validate_expr(const index_exprt &value)
+{
+  validate_operands(value, 2, "Array index must have two operands");
+}
+
+
 /*! \brief array constructor from single element
 */
 class array_of_exprt:public unary_exprt
@@ -1304,6 +1476,16 @@ inline array_of_exprt &to_array_of_expr(exprt &expr)
   return static_cast<array_of_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<array_of_exprt>(const exprt &base)
+{
+  return base.id()==ID_array_of;
+}
+inline void validate_expr(const array_of_exprt &value)
+{
+  validate_operands(value, 1, "'Array of' must have one operand");
+}
+
+
 /*! \brief array constructor from list of elements
 */
 class array_exprt:public exprt
@@ -1344,6 +1526,12 @@ inline array_exprt &to_array_expr(exprt &expr)
   return static_cast<array_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<array_exprt>(const exprt &base)
+{
+  return base.id()==ID_array;
+}
+
+
 /*! \brief vector constructor from list of elements
 */
 class vector_exprt:public exprt
@@ -1384,6 +1572,12 @@ inline vector_exprt &to_vector_expr(exprt &expr)
   return static_cast<vector_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<vector_exprt>(const exprt &base)
+{
+  return base.id()==ID_vector;
+}
+
+
 /*! \brief union constructor from single element
 */
 class union_exprt:public unary_exprt
@@ -1459,6 +1653,16 @@ inline union_exprt &to_union_expr(exprt &expr)
   return static_cast<union_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<union_exprt>(const exprt &base)
+{
+  return base.id()==ID_union;
+}
+inline void validate_expr(const union_exprt &value)
+{
+  validate_operands(value, 1, "Union constructor must have one operand");
+}
+
+
 /*! \brief struct constructor from list of elements
 */
 class struct_exprt:public exprt
@@ -1499,6 +1703,12 @@ inline struct_exprt &to_struct_expr(exprt &expr)
   return static_cast<struct_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<struct_exprt>(const exprt &base)
+{
+  return base.id()==ID_struct;
+}
+
+
 /*! \brief complex constructor from a pair of numbers
 */
 class complex_exprt:public binary_exprt
@@ -1571,6 +1781,16 @@ inline complex_exprt &to_complex_expr(exprt &expr)
   return static_cast<complex_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<complex_exprt>(const exprt &base)
+{
+  return base.id()==ID_complex;
+}
+inline void validate_expr(const complex_exprt &value)
+{
+  validate_operands(value, 2, "Complex constructor must have two operands");
+}
+
+
 class namespacet;
 
 /*! \brief split an expression into a base object and a (byte) offset
@@ -1653,6 +1873,17 @@ inline object_descriptor_exprt &to_object_descriptor_expr(exprt &expr)
   return static_cast<object_descriptor_exprt &>(expr);
 }
 
+template<>
+inline bool can_cast_expr<object_descriptor_exprt>(const exprt &base)
+{
+  return base.id()==ID_object_descriptor;
+}
+inline void validate_expr(const object_descriptor_exprt &value)
+{
+  validate_operands(value, 2, "Object descriptor must have two operands");
+}
+
+
 /*! \brief TO_BE_DOCUMENTED
 */
 class dynamic_object_exprt:public exprt
@@ -1720,6 +1951,16 @@ inline dynamic_object_exprt &to_dynamic_object_expr(exprt &expr)
   return static_cast<dynamic_object_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<dynamic_object_exprt>(const exprt &base)
+{
+  return base.id()==ID_dynamic_object;
+}
+inline void validate_expr(const dynamic_object_exprt &value)
+{
+  validate_operands(value, 2, "Dynamic object must have two operands");
+}
+
+
 /*! \brief semantic type conversion
 */
 class typecast_exprt:public exprt
@@ -1778,6 +2019,16 @@ inline typecast_exprt &to_typecast_expr(exprt &expr)
   return static_cast<typecast_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<typecast_exprt>(const exprt &base)
+{
+  return base.id()==ID_typecast;
+}
+inline void validate_expr(const typecast_exprt &value)
+{
+  validate_operands(value, 1, "Typecast must have one operand");
+}
+
+
 /*! \brief semantic type conversion from/to floating-point formats
 */
 class floatbv_typecast_exprt:public binary_exprt
@@ -1846,6 +2097,17 @@ inline floatbv_typecast_exprt &to_floatbv_typecast_expr(exprt &expr)
   return static_cast<floatbv_typecast_exprt &>(expr);
 }
 
+template<>
+inline bool can_cast_expr<floatbv_typecast_exprt>(const exprt &base)
+{
+  return base.id()==ID_floatbv_typecast;
+}
+inline void validate_expr(const floatbv_typecast_exprt &value)
+{
+  validate_operands(value, 2, "Float typecast must have two operands");
+}
+
+
 /*! \brief boolean AND
 */
 class and_exprt:public multi_ary_exprt
@@ -1920,6 +2182,16 @@ inline and_exprt &to_and_expr(exprt &expr)
   return static_cast<and_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<and_exprt>(const exprt &base)
+{
+  return base.id()==ID_and;
+}
+// inline void validate_expr(const and_exprt &value)
+// {
+//   validate_operands(value, 2, "And must have two or more operands", true);
+// }
+
+
 /*! \brief boolean implication
 */
 class implies_exprt:public binary_exprt
@@ -1962,6 +2234,16 @@ inline implies_exprt &to_implies_expr(exprt &expr)
   return static_cast<implies_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<implies_exprt>(const exprt &base)
+{
+  return base.id()==ID_implies;
+}
+inline void validate_expr(const implies_exprt &value)
+{
+  validate_operands(value, 2, "Implies must have two operands");
+}
+
+
 /*! \brief boolean OR
 */
 class or_exprt:public multi_ary_exprt
@@ -2036,6 +2318,16 @@ inline or_exprt &to_or_expr(exprt &expr)
   return static_cast<or_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<or_exprt>(const exprt &base)
+{
+  return base.id()==ID_or;
+}
+// inline void validate_expr(const or_exprt &value)
+// {
+//   validate_operands(value, 2, "Or must have two or more operands", true);
+// }
+
+
 /*! \brief Bit-wise negation of bit-vectors
 */
 class bitnot_exprt:public unary_exprt
@@ -2080,6 +2372,15 @@ inline bitnot_exprt &to_bitnot_expr(exprt &expr)
   return static_cast<bitnot_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<bitnot_exprt>(const exprt &base)
+{
+  return base.id()==ID_bitnot;
+}
+// inline void validate_expr(const bitnot_exprt &value)
+// {
+//   validate_operands(value, 1, "Bit-wise not must have one operand");
+// }
+
 
 /*! \brief Bit-wise OR
 */
@@ -2128,6 +2429,20 @@ inline bitor_exprt &to_bitor_expr(exprt &expr)
   return static_cast<bitor_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<bitor_exprt>(const exprt &base)
+{
+  return base.id()==ID_bitor;
+}
+// inline void validate_expr(const bitor_exprt &value)
+// {
+//   validate_operands(
+//     value,
+//     2,
+//     "Bit-wise or must have two or more operands",
+//     true);
+// }
+
+
 /*! \brief Bit-wise XOR
 */
 class bitxor_exprt:public multi_ary_exprt
@@ -2174,6 +2489,20 @@ inline bitxor_exprt &to_bitxor_expr(exprt &expr)
   return static_cast<bitxor_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<bitxor_exprt>(const exprt &base)
+{
+  return base.id()==ID_bitxor;
+}
+// inline void validate_expr(const bitxor_exprt &value)
+// {
+//   validate_operands(
+//     value,
+//     2,
+//     "Bit-wise xor must have two or more operands",
+//     true);
+// }
+
+
 /*! \brief Bit-wise AND
 */
 class bitand_exprt:public multi_ary_exprt
@@ -2221,6 +2550,20 @@ inline bitand_exprt &to_bitand_expr(exprt &expr)
   return static_cast<bitand_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<bitand_exprt>(const exprt &base)
+{
+  return base.id()==ID_bitand;
+}
+// inline void validate_expr(const bitand_exprt &value)
+// {
+//   validate_operands(
+//     value,
+//     2,
+//     "Bit-wise and must have two or more operands",
+//     true);
+// }
+
+
 /*! \brief A base class for shift operators
 */
 class shift_exprt:public binary_exprt
@@ -2295,6 +2638,15 @@ inline shift_exprt &to_shift_expr(exprt &expr)
   return static_cast<shift_exprt &>(expr);
 }
 
+// The to_*_expr function for this type doesn't do any checks before casting,
+// therefore the implementation is essentially a static_cast.
+// Enabling expr_dynamic_cast would hide this; instead use static_cast directly.
+// inline void validate_expr(const shift_exprt &value)
+// {
+//   validate_operands(value, 2, "Shifts must have two operands");
+// }
+
+
 /*! \brief Left shift
 */
 class shl_exprt:public shift_exprt
@@ -2428,6 +2780,16 @@ inline replication_exprt &to_replication_expr(exprt &expr)
   return static_cast<replication_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<replication_exprt>(const exprt &base)
+{
+  return base.id()==ID_replication;
+}
+inline void validate_expr(const replication_exprt &value)
+{
+  validate_operands(value, 2, "Bit-wise replication must have two operands");
+}
+
+
 /*! \brief Extracts a single bit of a bit-vector operand
 */
 class extractbit_exprt:public binary_predicate_exprt
@@ -2499,6 +2861,16 @@ inline extractbit_exprt &to_extractbit_expr(exprt &expr)
   return static_cast<extractbit_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<extractbit_exprt>(const exprt &base)
+{
+  return base.id()==ID_extractbit;
+}
+inline void validate_expr(const extractbit_exprt &value)
+{
+  validate_operands(value, 2, "Extract bit must have two operands");
+}
+
+
 /*! \brief Extracts a sub-range of a bit-vector operand
 */
 class extractbits_exprt:public exprt
@@ -2587,6 +2959,16 @@ inline extractbits_exprt &to_extractbits_expr(exprt &expr)
   return static_cast<extractbits_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<extractbits_exprt>(const exprt &base)
+{
+  return base.id()==ID_extractbits;
+}
+inline void validate_expr(const extractbits_exprt &value)
+{
+  validate_operands(value, 3, "Extract bits must have three operands");
+}
+
+
 /*! \brief Operator to return the address of an object
 */
 class address_of_exprt:public unary_exprt
@@ -2637,6 +3019,16 @@ inline address_of_exprt &to_address_of_expr(exprt &expr)
   return static_cast<address_of_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<address_of_exprt>(const exprt &base)
+{
+  return base.id()==ID_address_of;
+}
+inline void validate_expr(const address_of_exprt &value)
+{
+  validate_operands(value, 1, "Address of must have one operand");
+}
+
+
 /*! \brief Boolean negation
 */
 class not_exprt:public exprt
@@ -2690,6 +3082,16 @@ inline not_exprt &to_not_expr(exprt &expr)
   return static_cast<not_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<not_exprt>(const exprt &base)
+{
+  return base.id()==ID_not;
+}
+inline void validate_expr(const not_exprt &value)
+{
+  validate_operands(value, 1, "Not must have one operand");
+}
+
+
 /*! \brief Operator to dereference a pointer
 */
 class dereference_exprt:public exprt
@@ -2760,6 +3162,16 @@ inline dereference_exprt &to_dereference_expr(exprt &expr)
   return static_cast<dereference_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<dereference_exprt>(const exprt &base)
+{
+  return base.id()==ID_dereference;
+}
+inline void validate_expr(const dereference_exprt &value)
+{
+  validate_operands(value, 1, "Dereference must have one operand");
+}
+
+
 /*! \brief The trinary if-then-else operator
 */
 class if_exprt:public exprt
@@ -2848,6 +3260,16 @@ inline if_exprt &to_if_expr(exprt &expr)
   return static_cast<if_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<if_exprt>(const exprt &base)
+{
+  return base.id()==ID_if;
+}
+inline void validate_expr(const if_exprt &value)
+{
+  validate_operands(value, 3, "If-then-else must have three operands");
+}
+
+
 /*! \brief Operator to update elements in structs and arrays
     \remark This expression will eventually be replaced by separate
             array and struct update operators.
@@ -2931,6 +3353,19 @@ inline with_exprt &to_with_expr(exprt &expr)
   return static_cast<with_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<with_exprt>(const exprt &base)
+{
+  return base.id()==ID_with;
+}
+inline void validate_expr(const with_exprt &value)
+{
+  validate_operands(
+    value,
+    3,
+    "Array/structure update must have three operands");
+}
+
+
 class index_designatort:public exprt
 {
 public:
@@ -2982,6 +3417,16 @@ inline index_designatort &to_index_designator(exprt &expr)
   return static_cast<index_designatort &>(expr);
 }
 
+template<> inline bool can_cast_expr<index_designatort>(const exprt &base)
+{
+  return base.id()==ID_index_designator;
+}
+inline void validate_expr(const index_designatort &value)
+{
+  validate_operands(value, 1, "Index designator must have one operand");
+}
+
+
 class member_designatort:public exprt
 {
 public:
@@ -3028,6 +3473,16 @@ inline member_designatort &to_member_designator(exprt &expr)
   return static_cast<member_designatort &>(expr);
 }
 
+template<> inline bool can_cast_expr<member_designatort>(const exprt &base)
+{
+  return base.id()==ID_member_designator;
+}
+inline void validate_expr(const member_designatort &value)
+{
+  validate_operands(value, 0, "Member designator must not have operands");
+}
+
+
 /*! \brief Operator to update elements in structs and arrays
 */
 class update_exprt:public exprt
@@ -3120,6 +3575,19 @@ inline update_exprt &to_update_expr(exprt &expr)
   return static_cast<update_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<update_exprt>(const exprt &base)
+{
+  return base.id()==ID_update;
+}
+inline void validate_expr(const update_exprt &value)
+{
+  validate_operands(
+    value,
+    3,
+    "Array/structure update must have three operands");
+}
+
+
 #if 0
 /*! \brief update of one element of an array
 */
@@ -3201,8 +3669,19 @@ inline array_update_exprt &to_array_update_expr(exprt &expr)
     "Array update must have three operands");
   return static_cast<array_update_exprt &>(expr);
 }
+
+template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
+{
+  return base.id()==ID_array_update;
+}
+inline void validate_expr(const array_update_exprt &value)
+{
+  validate_operands(value, 3, "Array update must have three operands");
+}
+
 #endif
 
+
 /*! \brief Extract member of struct or union
 */
 class member_exprt:public exprt
@@ -3325,6 +3804,16 @@ inline member_exprt &to_member_expr(exprt &expr)
   return static_cast<member_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<member_exprt>(const exprt &base)
+{
+  return base.id()==ID_member;
+}
+inline void validate_expr(const member_exprt &value)
+{
+  validate_operands(value, 1, "Extract member must have one operand");
+}
+
+
 /*! \brief Evaluates to true if the operand is NaN
 */
 class isnan_exprt:public unary_predicate_exprt
@@ -3367,6 +3856,16 @@ inline isnan_exprt &to_isnan_expr(exprt &expr)
   return static_cast<isnan_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<isnan_exprt>(const exprt &base)
+{
+  return base.id()==ID_isnan;
+}
+inline void validate_expr(const isnan_exprt &value)
+{
+  validate_operands(value, 1, "Is NaN must have one operand");
+}
+
+
 /*! \brief Evaluates to true if the operand is infinite
 */
 class isinf_exprt:public unary_predicate_exprt
@@ -3413,6 +3912,16 @@ inline isinf_exprt &to_isinf_expr(exprt &expr)
   return static_cast<isinf_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<isinf_exprt>(const exprt &base)
+{
+  return base.id()==ID_isinf;
+}
+inline void validate_expr(const isinf_exprt &value)
+{
+  validate_operands(value, 1, "Is infinite must have one operand");
+}
+
+
 /*! \brief Evaluates to true if the operand is finite
 */
 class isfinite_exprt:public unary_predicate_exprt
@@ -3455,6 +3964,16 @@ inline isfinite_exprt &to_isfinite_expr(exprt &expr)
   return static_cast<isfinite_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<isfinite_exprt>(const exprt &base)
+{
+  return base.id()==ID_isfinite;
+}
+inline void validate_expr(const isfinite_exprt &value)
+{
+  validate_operands(value, 1, "Is finite must have one operand");
+}
+
+
 /*! \brief Evaluates to true if the operand is a normal number
 */
 class isnormal_exprt:public unary_predicate_exprt
@@ -3497,6 +4016,16 @@ inline isnormal_exprt &to_isnormal_expr(exprt &expr)
   return static_cast<isnormal_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<isnormal_exprt>(const exprt &base)
+{
+  return base.id()==ID_isnormal;
+}
+inline void validate_expr(const isnormal_exprt &value)
+{
+  validate_operands(value, 1, "Is normal must have one operand");
+}
+
+
 /*! \brief IEEE-floating-point equality
 */
 class ieee_float_equal_exprt:public binary_relation_exprt
@@ -3543,6 +4072,17 @@ inline ieee_float_equal_exprt &to_ieee_float_equal_expr(exprt &expr)
   return static_cast<ieee_float_equal_exprt &>(expr);
 }
 
+template<>
+inline bool can_cast_expr<ieee_float_equal_exprt>(const exprt &base)
+{
+  return base.id()==ID_ieee_float_equal;
+}
+inline void validate_expr(const ieee_float_equal_exprt &value)
+{
+  validate_operands(value, 2, "IEEE equality must have two operands");
+}
+
+
 /*! \brief IEEE floating-point disequality
 */
 class ieee_float_notequal_exprt:public binary_relation_exprt
@@ -3591,6 +4131,17 @@ inline ieee_float_notequal_exprt &to_ieee_float_notequal_expr(exprt &expr)
   return static_cast<ieee_float_notequal_exprt &>(expr);
 }
 
+template<>
+inline bool can_cast_expr<ieee_float_notequal_exprt>(const exprt &base)
+{
+  return base.id()==ID_ieee_float_notequal;
+}
+inline void validate_expr(const ieee_float_notequal_exprt &value)
+{
+  validate_operands(value, 2, "IEEE inequality must have two operands");
+}
+
+
 /*! \brief IEEE floating-point operations
 */
 class ieee_float_op_exprt:public exprt
@@ -3671,6 +4222,20 @@ inline ieee_float_op_exprt &to_ieee_float_op_expr(exprt &expr)
   return static_cast<ieee_float_op_exprt &>(expr);
 }
 
+// The to_*_expr function for this type doesn't do any checks before casting,
+// therefore the implementation is essentially a static_cast.
+// Enabling expr_dynamic_cast would hide this; instead use static_cast directly.
+// template<>
+// inline void validate_expr<ieee_float_op_exprt>(
+//   const ieee_float_op_exprt &value)
+// {
+//   validate_operands(
+//     value,
+//     3,
+//     "IEEE float operations must have three arguments");
+// }
+
+
 /*! \brief An expression denoting a type
 */
 class type_exprt:public exprt
@@ -3743,6 +4308,12 @@ inline constant_exprt &to_constant_expr(exprt &expr)
   return static_cast<constant_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<constant_exprt>(const exprt &base)
+{
+  return base.id()==ID_constant;
+}
+
+
 /*! \brief The boolean constant true
 */
 class true_exprt:public constant_exprt
@@ -3864,6 +4435,17 @@ inline function_application_exprt &to_function_application_expr(exprt &expr)
   return static_cast<function_application_exprt &>(expr);
 }
 
+template<>
+inline bool can_cast_expr<function_application_exprt>(const exprt &base)
+{
+  return base.id()==ID_function_application;
+}
+inline void validate_expr(const function_application_exprt &value)
+{
+  validate_operands(value, 2, "Function application must have two operands");
+}
+
+
 /*! \brief Concatenation of bit-vector operands
  *
  * This expression takes any number of operands
@@ -3922,6 +4504,22 @@ inline concatenation_exprt &to_concatenation_expr(exprt &expr)
   return static_cast<concatenation_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<concatenation_exprt>(const exprt &base)
+{
+  return base.id()==ID_concatenation;
+}
+// template<>
+// inline void validate_expr<concatenation_exprt>(
+//   const concatenation_exprt &value)
+// {
+//   validate_operands(
+//     value,
+//     2,
+//     "Concatenation must have two or more operands",
+//     true);
+// }
+
+
 /*! \brief An expression denoting infinity
 */
 class infinity_exprt:public exprt
@@ -4002,6 +4600,16 @@ inline let_exprt &to_let_expr(exprt &expr)
   return static_cast<let_exprt &>(expr);
 }
 
+template<> inline bool can_cast_expr<let_exprt>(const exprt &base)
+{
+  return base.id()==ID_let;
+}
+inline void validate_expr(const let_exprt &value)
+{
+  validate_operands(value, 3, "Let must have three operands");
+}
+
+
 /*! \brief A forall expression
 */
 class forall_exprt:public exprt
diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt
index 623e57ecb50..010ef336546 100644
--- a/unit/CMakeLists.txt
+++ b/unit/CMakeLists.txt
@@ -21,6 +21,9 @@ list(REMOVE_ITEM sources
     ${CMAKE_CURRENT_SOURCE_DIR}/cpp_scanner.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/float_utils.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/ieee_float.cpp
+
+    # Intended to fail to compile
+    ${CMAKE_CURRENT_SOURCE_DIR}/util/expr_cast/expr_undefined_casts.cpp
 )
 
 add_executable(unit ${sources} ${headers})
diff --git a/unit/Makefile b/unit/Makefile
index 52c60febfda..0f81813e67e 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -26,6 +26,7 @@ SRC += unit_tests.cpp \
        solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \
        solvers/refinement/string_refinement/concretize_array.cpp \
        solvers/refinement/string_refinement/substitute_array_list.cpp \
+       util/expr_cast/expr_cast.cpp \
        util/expr_iterator.cpp \
        util/simplify_expr.cpp \
        catch_example.cpp \
diff --git a/unit/util/expr_cast/expr_cast.cpp b/unit/util/expr_cast/expr_cast.cpp
new file mode 100644
index 00000000000..658e35a5057
--- /dev/null
+++ b/unit/util/expr_cast/expr_cast.cpp
@@ -0,0 +1,95 @@
+/*
+  Author: Nathan Phillips <Nathan.Phillips@diffblue.com>
+*/
+
+/// \file
+/// expr_dynamic_cast Unit Tests
+
+#include <catch.hpp>
+#include <util/std_expr.h>
+#include <util/std_code.h>
+#include <util/std_types.h>
+
+
+SCENARIO("expr_dynamic_cast",
+  "[core][utils][expr_cast][expr_dynamic_cast]")
+{
+  symbol_exprt symbol_expr;
+
+  GIVEN("A const exprt reference to a symbolt")
+  {
+    const exprt &expr=symbol_expr;
+
+    THEN("Try-casting from exprt reference to symbol_exprt pointer "
+         "returns a value")
+    {
+      REQUIRE(expr_try_dynamic_cast<const symbol_exprt &>(expr).has_value());
+    }
+
+    THEN("Casting from exprt pointer to transt pointer doesn't return a value")
+    {
+      REQUIRE(!expr_try_dynamic_cast<const transt &>(expr).has_value());
+    }
+  }
+  GIVEN("A exprt reference to a symbolt")
+  {
+    exprt &expr=symbol_expr;
+
+    THEN("Casting from exprt reference to symbol_exprt reference "
+         "returns a value")
+    {
+      REQUIRE(expr_try_dynamic_cast<symbol_exprt &>(expr).has_value());
+    }
+
+    THEN("Casting from exprt reference to transt reference "
+         "doesn't return a value")
+    {
+      REQUIRE(!expr_try_dynamic_cast<transt &>(expr).has_value());
+    }
+  }
+  GIVEN("A const exprt reference to a symbolt")
+  {
+    const exprt &expr_ref=symbol_expr;
+
+    THEN(
+      "Casting from exprt reference to symbol_exprt reference should not throw")
+    {
+      REQUIRE_NOTHROW(expr_dynamic_cast<const symbol_exprt &>(expr_ref));
+    }
+
+    THEN("Casting from exprt reference to transt reference should throw")
+    {
+      // This no longer throws exceptions when our custom asserts are set to
+      //  abort the program
+      // REQUIRE_THROWS_AS(
+      //   expr_dynamic_cast<const transt &>(expr_ref),
+      //   std::bad_cast);
+    }
+  }
+  GIVEN("A exprt reference to a symbolt")
+  {
+    exprt &expr_ref=symbol_expr;
+
+    THEN(
+      "Casting from exprt reference to symbol_exprt reference should not throw")
+    {
+      REQUIRE_NOTHROW(expr_dynamic_cast<symbol_exprt &>(expr_ref));
+    }
+
+    THEN("Casting from exprt reference to transt reference should throw")
+    {
+      // This no longer throws exceptions when our custom asserts are set to
+      //  abort the program
+      // REQUIRE_THROWS_AS(
+      //   expr_dynamic_cast<transt &>(expr_ref),
+      //   std::bad_cast);
+    }
+
+    THEN(
+      "Casting from non-const exprt reference to const symbol_exprt reference "
+      "should be fine")
+    {
+      REQUIRE_NOTHROW(expr_dynamic_cast<const symbol_exprt &>(expr_ref));
+    }
+  }
+}
diff --git a/unit/util/expr_cast/expr_undefined_casts.cpp b/unit/util/expr_cast/expr_undefined_casts.cpp
new file mode 100644
index 00000000000..4f1dc7165b8
--- /dev/null
+++ b/unit/util/expr_cast/expr_undefined_casts.cpp
@@ -0,0 +1,50 @@
+/*
+  Author: Nathan Phillips <Nathan.Phillips@diffblue.com>
+*/
+
+/// \file
+/// expr_dynamic_cast for types that don't have a cast
+
+// This could have a unit test that consisted of trying to compile the file
+// and checking that the compiler gave the right error messages.
+
+#include <catch.hpp>
+#include <util/std_expr.h>
+#include <util/std_code.h>
+#include <util/std_types.h>
+
+
+SCENARIO("expr_dynamic_cast",
+  "[core][utils][expr_cast][expr_dynamic_cast]")
+{
+  symbol_exprt symbol_expr;
+
+  GIVEN("A const exprt reference to a symbolt")
+  {
+    const exprt &expr=symbol_expr;
+
+    THEN("Casting from exprt reference to ieee_float_op_exprt "
+         "should not compile")
+    {
+      // This shouldn't compile
+      expr_dynamic_cast<const ieee_float_op_exprt &>(expr);
+    }
+    THEN("Casting from exprt reference to shift_exprt should not compile")
+    {
+      // This shouldn't compile
+      expr_dynamic_cast<const shift_exprt &>(expr);
+    }
+    THEN(
+      "Casting from exprt reference to non-reference should not compile")
+    {
+      // This shouldn't compile
+      expr_dynamic_cast<symbol_exprt>(expr);
+    }
+    THEN(
+      "Casting from const exprt reference to non-const symbol_exprt reference "
+      "should not compile")
+    {
+      expr_dynamic_cast<symbol_exprt &>(expr);
+    }
+  }
+}