diff --git a/src/solvers/flattening/boolbv_overflow.cpp b/src/solvers/flattening/boolbv_overflow.cpp
index a32dd19a13b..250ba157a11 100644
--- a/src/solvers/flattening/boolbv_overflow.cpp
+++ b/src/solvers/flattening/boolbv_overflow.cpp
@@ -125,15 +125,14 @@ literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr)
       ? bv_utilst::representationt::SIGNED
       : bv_utilst::representationt::UNSIGNED;
 
-  if(
-    const auto plus_overflow = expr_try_dynamic_cast<plus_overflow_exprt>(expr))
+  if(expr_try_dynamic_cast<plus_overflow_exprt>(expr))
   {
     if(bv0.size() != bv1.size())
       return SUB::convert_rest(expr);
 
     return bv_utils.overflow_add(bv0, bv1, rep);
   }
-  if(const auto minus = expr_try_dynamic_cast<minus_overflow_exprt>(expr))
+  if(expr_try_dynamic_cast<minus_overflow_exprt>(expr))
   {
     if(bv0.size() != bv1.size())
       return SUB::convert_rest(expr);
@@ -158,8 +157,7 @@ literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr)
 
     return mult_overflow_result(prop, bv0, bv1, rep).back();
   }
-  else if(
-    const auto shl_overflow = expr_try_dynamic_cast<shl_overflow_exprt>(expr))
+  else if(expr_try_dynamic_cast<shl_overflow_exprt>(expr))
   {
     DATA_INVARIANT(!bv0.empty(), "zero-sized operand");
 
diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
index 3632147c0a8..4622c32eb9e 100644
--- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
+++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
@@ -175,14 +175,14 @@ static smt_termt make_bitvector_resize_cast(
   const bitvector_typet &from_type,
   const bitvector_typet &to_type)
 {
-  if(const auto to_fixedbv_type = type_try_dynamic_cast<fixedbv_typet>(to_type))
+  if(type_try_dynamic_cast<fixedbv_typet>(to_type))
   {
     UNIMPLEMENTED_FEATURE(
       "Generation of SMT formula for type cast to fixed-point bitvector "
       "type: " +
       to_type.pretty());
   }
-  if(const auto to_floatbv_type = type_try_dynamic_cast<floatbv_typet>(to_type))
+  if(type_try_dynamic_cast<floatbv_typet>(to_type))
   {
     UNIMPLEMENTED_FEATURE(
       "Generation of SMT formula for type cast to floating-point bitvector "
@@ -258,7 +258,7 @@ static smt_termt convert_expr_to_smt(
   const auto &from_term = converted.at(cast.op());
   const typet &from_type = cast.op().type();
   const typet &to_type = cast.type();
-  if(const auto bool_type = type_try_dynamic_cast<bool_typet>(to_type))
+  if(type_try_dynamic_cast<bool_typet>(to_type))
     return make_not_zero(from_term, cast.op().type());
   if(const auto c_bool_type = type_try_dynamic_cast<c_bool_typet>(to_type))
     return convert_c_bool_cast(from_term, from_type, *c_bool_type);
@@ -893,9 +893,7 @@ static smt_termt convert_expr_to_smt(
     "Pointer should be wider than object_bits in order to allow for offset "
     "encoding.");
   const size_t offset_bits = type->get_width() - object_bits;
-  if(
-    const auto symbol =
-      expr_try_dynamic_cast<symbol_exprt>(address_of.object()))
+  if(expr_try_dynamic_cast<symbol_exprt>(address_of.object()))
   {
     const smt_bit_vector_constant_termt offset{0, offset_bits};
     return smt_bit_vector_theoryt::concat(object_bit_vector, offset);