diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index e0aef679768..41f08f15515 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -170,26 +170,24 @@ std::string graphml_witnesst::convert_assign_rec(
   else if(assign.rhs().id() == ID_with)
   {
     const with_exprt &with_expr = to_with_expr(assign.rhs());
-    const auto &ops = with_expr.operands();
 
-    for(std::size_t i = 1; i < ops.size(); i += 2)
-    {
-      if(!result.empty())
-        result += ' ';
+    if(!result.empty())
+      result += ' ';
 
-      if(ops[i].id() == ID_member_name)
-      {
-        const member_exprt member{
-          assign.lhs(), ops[i].get(ID_component_name), ops[i + 1].type()};
-        result +=
-          convert_assign_rec(identifier, code_assignt(member, ops[i + 1]));
-      }
-      else
-      {
-        const index_exprt index{assign.lhs(), ops[i]};
-        result +=
-          convert_assign_rec(identifier, code_assignt(index, ops[i + 1]));
-      }
+    if(with_expr.where().id() == ID_member_name)
+    {
+      const member_exprt member{
+        assign.lhs(),
+        with_expr.where().get(ID_component_name),
+        with_expr.new_value().type()};
+      result += convert_assign_rec(
+        identifier, code_assignt(member, with_expr.new_value()));
+    }
+    else
+    {
+      const index_exprt index{assign.lhs(), with_expr.where()};
+      result += convert_assign_rec(
+        identifier, code_assignt(index, with_expr.new_value()));
     }
   }
   else
diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp
index ad3562ed4d4..96cb3c8045f 100644
--- a/src/solvers/flattening/arrays.cpp
+++ b/src/solvers/flattening/arrays.cpp
@@ -145,11 +145,8 @@ void arrayst::collect_arrays(const exprt &a)
     collect_arrays(with_expr.old());
 
     // make sure this shows as an application
-    for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
-    {
-      index_exprt index_expr(with_expr.old(), with_expr.operands()[i]);
-      record_array_index(index_expr);
-    }
+    index_exprt index_expr(with_expr.old(), with_expr.where());
+    record_array_index(index_expr);
   }
   else if(a.id()==ID_update)
   {
@@ -574,31 +571,24 @@ void arrayst::add_array_constraints_with(
   const index_sett &index_set,
   const with_exprt &expr)
 {
-  // We got x=(y with [i:=v, j:=w, ...]).
-  // First add constraints x[i]=v, x[j]=w, ...
+  // We got x=(y with [i:=v]).
+  // First add constraint x[i]=v
   std::unordered_set<exprt, irep_hash> updated_indices;
 
-  const exprt::operandst &operands = expr.operands();
-  for(std::size_t i = 1; i + 1 < operands.size(); i += 2)
-  {
-    const exprt &index = operands[i];
-    const exprt &value = operands[i + 1];
-
-    index_exprt index_expr(
-      expr, index, to_array_type(expr.type()).element_type());
+  index_exprt index_expr(
+    expr, expr.where(), to_array_type(expr.type()).element_type());
 
-    DATA_INVARIANT_WITH_DIAGNOSTICS(
-      index_expr.type() == value.type(),
-      "with-expression operand should match array element type",
-      irep_pretty_diagnosticst{expr});
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    index_expr.type() == expr.new_value().type(),
+    "with-expression operand should match array element type",
+    irep_pretty_diagnosticst{expr});
 
-    lazy_constraintt lazy(
-      lazy_typet::ARRAY_WITH, equal_exprt(index_expr, value));
-    add_array_constraint(lazy, false); // added immediately
-    array_constraint_count[constraint_typet::ARRAY_WITH]++;
+  lazy_constraintt lazy(
+    lazy_typet::ARRAY_WITH, equal_exprt(index_expr, expr.new_value()));
+  add_array_constraint(lazy, false); // added immediately
+  array_constraint_count[constraint_typet::ARRAY_WITH]++;
 
-    updated_indices.insert(index);
-  }
+  updated_indices.insert(expr.where());
 
   // For all other indices use the existing value, i.e., add constraints
   // x[I]=y[I] for I!=i,j,...
diff --git a/src/solvers/flattening/boolbv_with.cpp b/src/solvers/flattening/boolbv_with.cpp
index 5eb83b0b3c0..c7c335ff96c 100644
--- a/src/solvers/flattening/boolbv_with.cpp
+++ b/src/solvers/flattening/boolbv_with.cpp
@@ -16,28 +16,16 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bvt boolbvt::convert_with(const with_exprt &expr)
 {
+  DATA_INVARIANT(
+    expr.operands().size() == 3,
+    "with_exprt with more than 3 operands should no longer exist");
+
   auto &type = expr.type();
 
   if(
     type.id() == ID_bv || type.id() == ID_unsignedbv ||
     type.id() == ID_signedbv)
   {
-    if(expr.operands().size() > 3)
-    {
-      std::size_t s = expr.operands().size();
-
-      // strip off the trailing two operands
-      with_exprt tmp = expr;
-      tmp.operands().resize(s - 2);
-
-      with_exprt new_with_expr(
-        tmp, expr.operands()[s - 2], expr.operands().back());
-
-      // recursive call
-      return convert_with(new_with_expr);
-    }
-
-    PRECONDITION(expr.operands().size() == 3);
     if(expr.new_value().type().id() == ID_bool)
     {
       return convert_bv(
@@ -50,7 +38,7 @@ bvt boolbvt::convert_with(const with_exprt &expr)
     }
   }
 
-  bvt bv = convert_bv(expr.old());
+  bvt bv_old = convert_bv(expr.old());
 
   std::size_t width = boolbv_width(type);
 
@@ -61,21 +49,14 @@ bvt boolbvt::convert_with(const with_exprt &expr)
   }
 
   DATA_INVARIANT_WITH_DIAGNOSTICS(
-    bv.size() == width,
+    bv_old.size() == width,
     "unexpected operand 0 width",
     irep_pretty_diagnosticst{expr});
 
-  bvt prev_bv;
-  prev_bv.resize(width);
-
-  const exprt::operandst &ops=expr.operands();
+  bvt bv;
+  bv.resize(width);
 
-  for(std::size_t op_no=1; op_no<ops.size(); op_no+=2)
-  {
-    bv.swap(prev_bv);
-
-    convert_with(expr.old().type(), ops[op_no], ops[op_no + 1], prev_bv, bv);
-  }
+  convert_with(expr.old().type(), expr.where(), expr.new_value(), bv_old, bv);
 
   return bv;
 }
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 14291ee5447..3eb0204573a 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -4308,27 +4308,9 @@ void smt2_convt::convert_floatbv_rem(const binary_exprt &expr)
 
 void smt2_convt::convert_with(const with_exprt &expr)
 {
-  // get rid of "with" that has more than three operands
-
-  if(expr.operands().size()>3)
-  {
-    std::size_t s=expr.operands().size();
-
-    // strip off the trailing two operands
-    with_exprt tmp = expr;
-    tmp.operands().resize(s-2);
-
-    with_exprt new_with_expr(
-      tmp, expr.operands()[s - 2], expr.operands().back());
-
-    // recursive call
-    return convert_with(new_with_expr);
-  }
-
   INVARIANT(
     expr.operands().size() == 3,
-    "with expression should have been converted to a version with three "
-    "operands above");
+    "with expression should have exactly three operands");
 
   const typet &expr_type = expr.type();
 
diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
index 4622c32eb9e..de901db4f59 100644
--- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
+++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
@@ -1005,12 +1005,9 @@ static smt_termt convert_array_update_to_smt(
   const sub_expression_mapt &converted)
 {
   smt_termt array = converted.at(with.old());
-  for(auto it = ++with.operands().begin(); it != with.operands().end(); it += 2)
-  {
-    const smt_termt &index_term = converted.at(it[0]);
-    const smt_termt &value_term = converted.at(it[1]);
-    array = smt_array_theoryt::store(array, index_term, value_term);
-  }
+  const smt_termt &index_term = converted.at(with.where());
+  const smt_termt &value_term = converted.at(with.new_value());
+  array = smt_array_theoryt::store(array, index_term, value_term);
   return array;
 }
 
diff --git a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp
index 7e8e946d86b..baf18f3187d 100644
--- a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp
+++ b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp
@@ -71,52 +71,25 @@ typet struct_encodingt::encode(typet type) const
   return type;
 }
 
-/// \brief Extracts the component/field names and new values from a `with_exprt`
-///        which expresses a new struct value where one or more members of a
-///        struct have had their values substituted with new values.
-/// \note  This is implemented using direct access to the operands and other
-///        underlying irept interfaces, because the interface for `with_exprt`
-///        only supports a single `where` / `new_value` pair and does not
-///        support extracting the name from the `where` operand.
-static std::unordered_map<irep_idt, exprt>
-extricate_updates(const with_exprt &struct_expr)
-{
-  std::unordered_map<irep_idt, exprt> pairs;
-  auto current_operand = struct_expr.operands().begin();
-  // Skip the struct being updated in order to begin with the pairs.
-  current_operand++;
-  while(current_operand != struct_expr.operands().end())
-  {
-    INVARIANT(
-      current_operand->id() == ID_member_name,
-      "operand is expected to be the name of a member");
-    auto name = current_operand->find(ID_component_name).id();
-    ++current_operand;
-    INVARIANT(
-      current_operand != struct_expr.operands().end(),
-      "every name is expected to be followed by a paired value");
-    pairs[name] = *current_operand;
-    ++current_operand;
-  }
-  POSTCONDITION(!pairs.empty());
-  return pairs;
-}
-
 static exprt encode(const with_exprt &with, const namespacet &ns)
 {
   const auto tag_type = type_checked_cast<struct_tag_typet>(with.type());
   const auto struct_type = ns.follow_tag(tag_type);
-  const auto updates = extricate_updates(with);
+  INVARIANT(
+    with.where().id() == ID_member_name,
+    "operand is expected to be the name of a member");
+  const auto update_name = with.where().find(ID_component_name).id();
   const auto components =
     make_range(struct_type.components())
-      .map([&](const struct_union_typet::componentt &component) -> exprt {
-        const auto &update = updates.find(component.get_name());
-        if(update != updates.end())
-          return update->second;
-        else
-          return member_exprt{
-            with.old(), component.get_name(), component.type()};
-      })
+      .map(
+        [&](const struct_union_typet::componentt &component) -> exprt
+        {
+          if(component.get_name() == update_name)
+            return with.new_value();
+          else
+            return member_exprt{
+              with.old(), component.get_name(), component.type()};
+        })
       .collect<exprt::operandst>();
   return struct_exprt{components, tag_type};
 }
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 72575d89f6b..0d8a91a6f89 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -334,16 +334,14 @@ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
 void smt2_incremental_decision_proceduret::define_index_identifiers(
   const exprt &expr)
 {
-  expr.visit_pre([&](const exprt &expr_node) {
-    if(!can_cast_type<array_typet>(expr_node.type()))
-      return;
-    if(const auto with_expr = expr_try_dynamic_cast<with_exprt>(expr_node))
+  expr.visit_post(
+    [&](const exprt &expr_node)
     {
-      for(auto operand_ite = ++with_expr->operands().begin();
-          operand_ite != with_expr->operands().end();
-          operand_ite += 2)
+      if(!can_cast_type<array_typet>(expr_node.type()))
+        return;
+      if(const auto with_expr = expr_try_dynamic_cast<with_exprt>(expr_node))
       {
-        const auto index_expr = *operand_ite;
+        const auto index_expr = with_expr->where();
         const auto index_term = convert_expr_to_smt(index_expr);
         const auto index_identifier =
           "index_" + std::to_string(index_sequence());
@@ -356,8 +354,7 @@ void smt2_incremental_decision_proceduret::define_index_identifiers(
         solver_process->send(
           smt_define_function_commandt{index_identifier, {}, index_term});
       }
-    }
-  });
+    });
 }
 
 exprt smt2_incremental_decision_proceduret::substitute_defined_padding(
diff --git a/src/util/lower_byte_operators.cpp b/src/util/lower_byte_operators.cpp
index 2399796f695..2ba9ecdb6b2 100644
--- a/src/util/lower_byte_operators.cpp
+++ b/src/util/lower_byte_operators.cpp
@@ -1607,10 +1607,7 @@ static exprt lower_byte_update_byte_array_vector(
         index_exprt{src.op(), where}};
     }
 
-    if(result.id() != ID_with)
-      result = with_exprt{result, std::move(where), std::move(update_value)};
-    else
-      result.add_to_operands(std::move(where), std::move(update_value));
+    result = with_exprt{result, std::move(where), std::move(update_value)};
   }
 
   return simplify_expr(std::move(result), ns);
@@ -1892,7 +1889,7 @@ static exprt lower_byte_update_array_vector_non_const(
         src.get_bits_per_byte()},
       ns);
 
-    result.add_to_operands(std::move(where), std::move(element));
+    result = with_exprt{result, std::move(where), std::move(element)};
   };
 
   std::size_t i = 1;
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index b6f19abda7b..18b2cf3fa8c 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -1339,6 +1339,19 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
       return changed(simplify_address_of(result)); // recursive call
     }
   }
+  else if(auto extractbits = expr_try_dynamic_cast<extractbits_exprt>(operand))
+  {
+    if(
+      can_cast_type<bitvector_typet>(expr_type) &&
+      can_cast_type<bitvector_typet>(operand.type()) &&
+      to_bitvector_type(expr_type).get_width() ==
+        to_bitvector_type(operand.type()).get_width())
+    {
+      extractbits_exprt result = *extractbits;
+      result.type() = expr_type;
+      return changed(simplify_extractbits(result));
+    }
+  }
 
   return unchanged(expr);
 }
@@ -1445,84 +1458,52 @@ simplify_exprt::simplify_lambda(const lambda_exprt &expr)
 
 simplify_exprt::resultt<> simplify_exprt::simplify_with(const with_exprt &expr)
 {
-  bool no_change = true;
-
-  if((expr.operands().size()%2)!=1)
-    return unchanged(expr);
-
-  // copy
-  auto with_expr = expr;
-
   // now look at first operand
 
   if(
-    with_expr.old().type().id() == ID_struct ||
-    with_expr.old().type().id() == ID_struct_tag)
+    expr.old().type().id() == ID_struct ||
+    expr.old().type().id() == ID_struct_tag)
   {
-    if(with_expr.old().id() == ID_struct || with_expr.old().is_constant())
+    if(expr.old().id() == ID_struct || expr.old().is_constant())
     {
-      while(with_expr.operands().size() > 1)
-      {
-        const irep_idt &component_name =
-          with_expr.where().get(ID_component_name);
-
-        const struct_typet &old_type_followed =
-          with_expr.old().type().id() == ID_struct_tag
-            ? ns.follow_tag(to_struct_tag_type(with_expr.old().type()))
-            : to_struct_type(with_expr.old().type());
-        if(!old_type_followed.has_component(component_name))
-          return unchanged(expr);
+      const irep_idt &component_name = expr.where().get(ID_component_name);
 
-        std::size_t number = old_type_followed.component_number(component_name);
-
-        if(number >= with_expr.old().operands().size())
-          return unchanged(expr);
+      const struct_typet &old_type_followed =
+        expr.old().type().id() == ID_struct_tag
+          ? ns.follow_tag(to_struct_tag_type(expr.old().type()))
+          : to_struct_type(expr.old().type());
+      if(!old_type_followed.has_component(component_name))
+        return unchanged(expr);
 
-        with_expr.old().operands()[number].swap(with_expr.new_value());
+      std::size_t number = old_type_followed.component_number(component_name);
 
-        with_expr.operands().erase(++with_expr.operands().begin());
-        with_expr.operands().erase(++with_expr.operands().begin());
+      if(number >= expr.old().operands().size())
+        return unchanged(expr);
 
-        no_change = false;
-      }
+      exprt result = expr.old();
+      result.operands()[number] = expr.new_value();
+      return result;
     }
   }
   else if(
-    with_expr.old().type().id() == ID_array ||
-    with_expr.old().type().id() == ID_vector)
+    expr.old().type().id() == ID_array || expr.old().type().id() == ID_vector)
   {
     if(
-      with_expr.old().id() == ID_array || with_expr.old().is_constant() ||
-      with_expr.old().id() == ID_vector)
+      expr.old().id() == ID_array || expr.old().is_constant() ||
+      expr.old().id() == ID_vector)
     {
-      while(with_expr.operands().size() > 1)
-      {
-        const auto i = numeric_cast<mp_integer>(with_expr.where());
-
-        if(!i.has_value())
-          break;
-
-        if(*i < 0 || *i >= with_expr.old().operands().size())
-          break;
-
-        with_expr.old().operands()[numeric_cast_v<std::size_t>(*i)].swap(
-          with_expr.new_value());
+      const auto i = numeric_cast<mp_integer>(expr.where());
 
-        with_expr.operands().erase(++with_expr.operands().begin());
-        with_expr.operands().erase(++with_expr.operands().begin());
-
-        no_change = false;
+      if(i.has_value() && *i >= 0 && *i < expr.old().operands().size())
+      {
+        exprt result = expr.old();
+        result.operands()[numeric_cast_v<std::size_t>(*i)] = expr.new_value();
+        return result;
       }
     }
   }
 
-  if(with_expr.operands().size() == 1)
-    return with_expr.old();
-
-  if(no_change)
-    return unchanged(expr);
-  else
-    return std::move(with_expr);
+  return unchanged(expr);
 }
 
 simplify_exprt::resultt<>
@@ -2263,7 +2244,8 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
 
         for(mp_integer i = 1; i < n_elements; ++i)
         {
-          result_expr.add_to_operands(
+          result_expr = with_exprt{
+            result_expr,
             from_integer(base_offset + i, array_type->index_type()),
             byte_extract_exprt{
               matching_byte_extract_id,
@@ -2271,7 +2253,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
               from_integer(
                 i * (*el_size / expr.get_bits_per_byte()), offset.type()),
               expr.get_bits_per_byte(),
-              array_type->element_type()});
+              array_type->element_type()}};
         }
 
         return changed(simplify_rec(result_expr));
@@ -2337,7 +2319,8 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
           mp_integer n_elements = *val_size / *el_size;
           for(mp_integer i = 1; i < n_elements; ++i)
           {
-            result_expr.add_to_operands(
+            result_expr = with_exprt{
+              result_expr,
               typecast_exprt::conditional_cast(
                 plus_exprt{base_offset, from_integer(i, base_offset.type())},
                 array_type->index_type()),
@@ -2347,7 +2330,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
                 from_integer(
                   i * (*el_size / expr.get_bits_per_byte()), offset.type()),
                 expr.get_bits_per_byte(),
-                array_type->element_type()});
+                array_type->element_type()}};
           }
           return changed(simplify_rec(result_expr));
         }
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index aad92696471..f1fa489bdfc 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -992,10 +992,15 @@ simplify_exprt::simplify_concatenation(const concatenation_exprt &expr)
   }
 
   // { x } = x
-  if(
-    new_expr.operands().size() == 1 && new_expr.op0().type() == new_expr.type())
+  if(new_expr.operands().size() == 1)
   {
-    return new_expr.op0();
+    if(new_expr.op0().type() == new_expr.type())
+      return new_expr.op0();
+    else
+    {
+      return changed(
+        simplify_typecast(typecast_exprt{new_expr.op0(), new_expr.type()}));
+    }
   }
 
   if(no_change)
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index 90cac8a1d8d..c96f16eaf39 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -2649,11 +2649,7 @@ inline bool can_cast_expr<with_exprt>(const exprt &base)
 
 inline void validate_expr(const with_exprt &value)
 {
-  validate_operands(
-    value, 3, "array/structure update must have at least 3 operands", true);
-  DATA_INVARIANT(
-    value.operands().size() % 2 == 1,
-    "array/structure update must have an odd number of operands");
+  validate_operands(value, 3, "array/structure update must have 3 operands");
 }
 
 /// \brief Cast an exprt to a \ref with_exprt
diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp
index a3ab0005dae..4a70592f67c 100644
--- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp
+++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp
@@ -1271,17 +1271,17 @@ TEST_CASE(
       INFO("Expression being converted: " + with.pretty(2, 0));
       CHECK(test.convert(with) == expected);
     }
-    SECTION("Dual where/new_value pair update")
+    SECTION("Nested where/new_value pair update")
     {
       exprt index2 = from_integer(24, unsignedbv_typet{64});
       exprt value2 = from_integer(21, value_type);
-      with.add_to_operands(std::move(index2), std::move(value2));
+      with_exprt with2{with, std::move(index2), std::move(value2)};
       const smt_termt expected2 = smt_array_theoryt::store(
         expected,
         smt_bit_vector_constant_termt{24, 64},
         smt_bit_vector_constant_termt{21, 8});
-      INFO("Expression being converted: " + with.pretty(2, 0));
-      CHECK(test.convert(with) == expected2);
+      INFO("Expression being converted: " + with2.pretty(2, 0));
+      CHECK(test.convert(with2) == expected2);
     }
   }
 }
diff --git a/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp b/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp
index 96d96cb07e1..9355bc93096 100644
--- a/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp
+++ b/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp
@@ -6,6 +6,7 @@
 #include <util/c_types.h>
 #include <util/mathematical_types.h>
 #include <util/namespace.h>
+#include <util/simplify_expr.h>
 #include <util/symbol_table.h>
 
 #include <solvers/smt2_incremental/encoding/nondet_padding.h>
@@ -242,12 +243,16 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
         symbol_expr,
         make_member_name_expression("green"),
         from_integer(0, signedbv_typet{32})};
-      const concatenation_exprt expected{
-        {from_integer(0, signedbv_typet{32}),
-         extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}},
-         extractbits_exprt{symbol_expr_as_bv, 0, signedbv_typet{24}}},
-        bv_typet{72}};
-      REQUIRE(test.struct_encoding.encode(with) == expected);
+      const exprt expected = simplify_expr(
+        concatenation_exprt{
+          {from_integer(0, signedbv_typet{32}),
+           extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}},
+           extractbits_exprt{symbol_expr_as_bv, 0, signedbv_typet{24}}},
+          bv_typet{72}},
+        test.ns);
+      const exprt encoded =
+        simplify_expr(test.struct_encoding.encode(with), test.ns);
+      REQUIRE(encoded == expected);
     }
     SECTION("Second member")
     {
@@ -268,131 +273,175 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
         symbol_expr,
         make_member_name_expression("ham"),
         from_integer(0, signedbv_typet{24})};
-      const concatenation_exprt expected{
-        {extractbits_exprt{symbol_expr_as_bv, 40, signedbv_typet{32}},
-         extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}},
-         from_integer(0, signedbv_typet{24})},
-        bv_typet{72}};
-      REQUIRE(test.struct_encoding.encode(with) == expected);
+      const exprt expected = simplify_expr(
+        concatenation_exprt{
+          {extractbits_exprt{symbol_expr_as_bv, 40, signedbv_typet{32}},
+           extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}},
+           from_integer(0, signedbv_typet{24})},
+          bv_typet{72}},
+        test.ns);
+      const exprt encoded =
+        simplify_expr(test.struct_encoding.encode(with), test.ns);
+      REQUIRE(encoded == expected);
     }
     SECTION("First and second members")
     {
-      const concatenation_exprt expected{
-        {from_integer(0, signedbv_typet{32}),
-         from_integer(1, unsignedbv_typet{16}),
-         extractbits_exprt{symbol_expr_as_bv, 0, signedbv_typet{24}}},
-        bv_typet{72}};
+      const exprt expected = simplify_expr(
+        concatenation_exprt{
+          {from_integer(0, signedbv_typet{32}),
+           from_integer(1, unsignedbv_typet{16}),
+           extractbits_exprt{symbol_expr_as_bv, 0, signedbv_typet{24}}},
+          bv_typet{72}},
+        test.ns);
       SECTION("Operands in field order")
       {
-        with_exprt with_in_order{
+        with_exprt with_in_order_inner{
           symbol_expr,
           make_member_name_expression("green"),
           from_integer(0, signedbv_typet{32})};
-        with_in_order.operands().push_back(make_member_name_expression("eggs"));
-        with_in_order.operands().push_back(
-          from_integer(1, unsignedbv_typet{16}));
-        REQUIRE(test.struct_encoding.encode(with_in_order) == expected);
+        with_exprt with_in_order{
+          with_in_order_inner,
+          make_member_name_expression("eggs"),
+          from_integer(1, unsignedbv_typet{16})};
+        const exprt encoded =
+          simplify_expr(test.struct_encoding.encode(with_in_order), test.ns);
+        REQUIRE(encoded == expected);
       }
       SECTION("Operands in reverse order vs fields")
       {
-        with_exprt with_reversed{
+        with_exprt with_reversed_inner{
           symbol_expr,
           make_member_name_expression("eggs"),
           from_integer(1, unsignedbv_typet{16})};
-        with_reversed.operands().push_back(
-          make_member_name_expression("green"));
-        with_reversed.operands().push_back(from_integer(0, signedbv_typet{32}));
-        REQUIRE(test.struct_encoding.encode(with_reversed) == expected);
+        with_exprt with_reversed{
+          with_reversed_inner,
+          make_member_name_expression("green"),
+          from_integer(0, signedbv_typet{32})};
+        const exprt encoded =
+          simplify_expr(test.struct_encoding.encode(with_reversed), test.ns);
+        REQUIRE(encoded == expected);
       }
     }
     SECTION("First and third members")
     {
-      const concatenation_exprt expected{
-        {from_integer(0, signedbv_typet{32}),
-         extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}},
-         from_integer(1, signedbv_typet{24})},
-        bv_typet{72}};
+      const exprt expected = simplify_expr(
+        concatenation_exprt{
+          {from_integer(0, signedbv_typet{32}),
+           extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}},
+           from_integer(1, signedbv_typet{24})},
+          bv_typet{72}},
+        test.ns);
       SECTION("Operands in field order")
       {
-        with_exprt with_in_order{
+        with_exprt with_in_order_inner{
           symbol_expr,
           make_member_name_expression("green"),
           from_integer(0, signedbv_typet{32})};
-        with_in_order.operands().push_back(make_member_name_expression("ham"));
-        with_in_order.operands().push_back(from_integer(1, signedbv_typet{24}));
-        REQUIRE(test.struct_encoding.encode(with_in_order) == expected);
+        with_exprt with_in_order{
+          with_in_order_inner,
+          make_member_name_expression("ham"),
+          from_integer(1, signedbv_typet{24})};
+        const exprt encoded =
+          simplify_expr(test.struct_encoding.encode(with_in_order), test.ns);
+        REQUIRE(encoded == expected);
       }
       SECTION("Operands in reverse order vs fields")
       {
-        with_exprt with_reversed{
+        with_exprt with_reversed_inner{
           symbol_expr,
           make_member_name_expression("ham"),
           from_integer(1, signedbv_typet{24})};
-        with_reversed.operands().push_back(
-          make_member_name_expression("green"));
-        with_reversed.operands().push_back(from_integer(0, signedbv_typet{32}));
-        REQUIRE(test.struct_encoding.encode(with_reversed) == expected);
+        with_exprt with_reversed{
+          with_reversed_inner,
+          make_member_name_expression("green"),
+          from_integer(0, signedbv_typet{32})};
+        const exprt encoded =
+          simplify_expr(test.struct_encoding.encode(with_reversed), test.ns);
+        REQUIRE(encoded == expected);
       }
     }
     SECTION("Second and third members")
     {
-      const concatenation_exprt expected{
-        {extractbits_exprt{symbol_expr_as_bv, 40, signedbv_typet{32}},
-         from_integer(0, unsignedbv_typet{16}),
-         from_integer(1, signedbv_typet{24})},
-        bv_typet{72}};
+      const exprt expected = simplify_expr(
+        concatenation_exprt{
+          {extractbits_exprt{symbol_expr_as_bv, 40, signedbv_typet{32}},
+           from_integer(0, unsignedbv_typet{16}),
+           from_integer(1, signedbv_typet{24})},
+          bv_typet{72}},
+        test.ns);
       SECTION("Operands in field order")
       {
-        with_exprt with_in_order{
+        with_exprt with_in_order_inner{
           symbol_expr,
           make_member_name_expression("eggs"),
           from_integer(0, unsignedbv_typet{16})};
-        with_in_order.operands().push_back(make_member_name_expression("ham"));
-        with_in_order.operands().push_back(from_integer(1, signedbv_typet{24}));
-        REQUIRE(test.struct_encoding.encode(with_in_order) == expected);
+        with_exprt with_in_order{
+          with_in_order_inner,
+          make_member_name_expression("ham"),
+          from_integer(1, signedbv_typet{24})};
+        const exprt encoded =
+          simplify_expr(test.struct_encoding.encode(with_in_order), test.ns);
+        REQUIRE(encoded == expected);
       }
       SECTION("Operands in reverse order vs fields")
       {
-        with_exprt with_reversed{
+        with_exprt with_reversed_inner{
           symbol_expr,
           make_member_name_expression("ham"),
           from_integer(1, signedbv_typet{24})};
-        with_reversed.operands().push_back(make_member_name_expression("eggs"));
-        with_reversed.operands().push_back(
-          from_integer(0, unsignedbv_typet{16}));
-        REQUIRE(test.struct_encoding.encode(with_reversed) == expected);
+        with_exprt with_reversed{
+          with_reversed_inner,
+          make_member_name_expression("eggs"),
+          from_integer(0, unsignedbv_typet{16})};
+        const exprt encoded =
+          simplify_expr(test.struct_encoding.encode(with_reversed), test.ns);
+        REQUIRE(encoded == expected);
       }
     }
     SECTION("All members")
     {
-      const concatenation_exprt expected{
-        {from_integer(1, signedbv_typet{32}),
-         from_integer(2, unsignedbv_typet{16}),
-         from_integer(3, signedbv_typet{24})},
-        bv_typet{72}};
+      const exprt expected = simplify_expr(
+        concatenation_exprt{
+          {from_integer(1, signedbv_typet{32}),
+           from_integer(2, unsignedbv_typet{16}),
+           from_integer(3, signedbv_typet{24})},
+          bv_typet{72}},
+        test.ns);
       SECTION("Operands in field order")
       {
-        with_exprt with{
+        with_exprt with_innermost{
           symbol_expr,
           make_member_name_expression("green"),
           from_integer(1, signedbv_typet{32})};
-        with.operands().push_back(make_member_name_expression("eggs"));
-        with.operands().push_back(from_integer(2, unsignedbv_typet{16}));
-        with.operands().push_back(make_member_name_expression("ham"));
-        with.operands().push_back(from_integer(3, signedbv_typet{24}));
-        REQUIRE(test.struct_encoding.encode(with) == expected);
+        with_exprt with_inner{
+          with_innermost,
+          make_member_name_expression("eggs"),
+          from_integer(2, unsignedbv_typet{16})};
+        with_exprt with{
+          with_inner,
+          make_member_name_expression("ham"),
+          from_integer(3, signedbv_typet{24})};
+        const exprt encoded =
+          simplify_expr(test.struct_encoding.encode(with), test.ns);
+        REQUIRE(encoded == expected);
       }
       SECTION("Operands out of order vs fields")
       {
-        with_exprt with{
+        with_exprt with_innermost{
           symbol_expr,
           make_member_name_expression("eggs"),
           from_integer(2, unsignedbv_typet{16})};
-        with.operands().push_back(make_member_name_expression("ham"));
-        with.operands().push_back(from_integer(3, signedbv_typet{24}));
-        with.operands().push_back(make_member_name_expression("green"));
-        with.operands().push_back(from_integer(1, signedbv_typet{32}));
-        REQUIRE(test.struct_encoding.encode(with) == expected);
+        with_exprt with_inner{
+          with_innermost,
+          make_member_name_expression("ham"),
+          from_integer(3, signedbv_typet{24})};
+        with_exprt with{
+          with_inner,
+          make_member_name_expression("green"),
+          from_integer(1, signedbv_typet{32})};
+        const exprt encoded =
+          simplify_expr(test.struct_encoding.encode(with), test.ns);
+        REQUIRE(encoded == expected);
       }
     }
   }
diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index a81069e8a99..5fd0a855875 100644
--- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -766,14 +766,16 @@ TEST_CASE(
   const auto original_array_symbol =
     make_test_symbol("original_array", array_type);
   const auto result_array_symbol = make_test_symbol("result_array", array_type);
-  with_exprt with_expr{
+  with_exprt with_expr_innermost{
     original_array_symbol.symbol_expr(),
     from_integer(0, index_type),
     from_integer(0, value_type)};
-  with_expr.add_to_operands(
-    from_integer(1, index_type), from_integer(1, value_type));
-  with_expr.add_to_operands(
-    from_integer(2, index_type), from_integer(2, value_type));
+  with_exprt with_expr_inner{
+    with_expr_innermost,
+    from_integer(1, index_type),
+    from_integer(1, value_type)};
+  with_exprt with_expr{
+    with_expr_inner, from_integer(2, index_type), from_integer(2, value_type)};
   const equal_exprt equal_expr{result_array_symbol.symbol_expr(), with_expr};
   test.sent_commands.clear();
   test.procedure.set_to(equal_expr, true);