diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index 72707e3692f..070ec496694 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -948,30 +948,34 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
     const auto &wexpr=to_with_expr(expr);
 
     mp_vectort dest = evaluate(wexpr.old());
-    mp_vectort where = evaluate(wexpr.where());
-    mp_vectort new_value = evaluate(wexpr.new_value());
 
-    const auto &subtype = to_array_type(expr.type()).element_type();
-
-    if(!new_value.empty() && where.size()==1 && !unbounded_size(subtype))
+    for(std::size_t i = 1; i < wexpr.operands().size(); i += 2)
     {
-      // Ignore indices < 0, which the string solver sometimes produces
-      if(where[0]<0)
-        return {};
+      mp_vectort where = evaluate(wexpr.operands()[i]);
+      mp_vectort new_value = evaluate(wexpr.operands()[i + 1]);
+
+      const auto &subtype = to_array_type(expr.type()).element_type();
 
-      mp_integer where_idx=where[0];
-      mp_integer subtype_size=get_size(subtype);
-      mp_integer need_size=(where_idx+1)*subtype_size;
+      if(!new_value.empty() && where.size() == 1 && !unbounded_size(subtype))
+      {
+        // Ignore indices < 0, which the string solver sometimes produces
+        if(where[0] < 0)
+          return {};
 
-      if(dest.size()<need_size)
-        dest.resize(numeric_cast_v<std::size_t>(need_size), 0);
+        mp_integer where_idx = where[0];
+        mp_integer subtype_size = get_size(subtype);
+        mp_integer need_size = (where_idx + 1) * subtype_size;
 
-      for(std::size_t i=0; i<new_value.size(); ++i)
-        dest[numeric_cast_v<std::size_t>((where_idx * subtype_size) + i)] =
-          new_value[i];
+        if(dest.size() < need_size)
+          dest.resize(numeric_cast_v<std::size_t>(need_size), 0);
 
-      return {};
+        for(std::size_t i = 0; i < new_value.size(); ++i)
+          dest[numeric_cast_v<std::size_t>((where_idx * subtype_size) + i)] =
+            new_value[i];
+      }
     }
+
+    return dest;
   }
   else if(expr.id()==ID_nil)
   {
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 626777ec8bf..a1e36ca96f6 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -973,26 +973,38 @@ void value_sett::get_value_set_rec(
       (expr.type().id() == ID_struct_tag || expr.type().id() == ID_struct) &&
       !suffix.empty())
     {
-      irep_idt component_name = with_expr.where().get(ID_component_name);
-      if(suffix_starts_with_field(suffix, id2string(component_name)))
+      bool any_matching_suffix = false;
+      bool all_matching_component_names = true;
+      for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
       {
-        // Looking for the member overwritten by this WITH expression
-        std::string remaining_suffix =
-          strip_first_field_from_suffix(suffix, id2string(component_name));
-        get_value_set_rec(
-          with_expr.new_value(),
-          dest,
-          includes_nondet_pointer,
-          remaining_suffix,
-          original_type,
-          ns);
+        irep_idt component_name =
+          with_expr.operands()[i].get(ID_component_name);
+        if(suffix_starts_with_field(suffix, id2string(component_name)))
+        {
+          // Looking for the member overwritten by this WITH expression
+          any_matching_suffix = true;
+          std::string remaining_suffix =
+            strip_first_field_from_suffix(suffix, id2string(component_name));
+          get_value_set_rec(
+            with_expr.operands()[i + 1],
+            dest,
+            includes_nondet_pointer,
+            remaining_suffix,
+            original_type,
+            ns);
+        }
+        else if(
+          all_matching_component_names &&
+          (expr.type().id() != ID_struct ||
+           !to_struct_type(expr.type()).has_component(component_name)) &&
+          (expr.type().id() != ID_struct_tag ||
+           !ns.follow_tag(to_struct_tag_type(expr.type()))
+              .has_component(component_name)))
+        {
+          all_matching_component_names = false;
+        }
       }
-      else if(
-        (expr.type().id() == ID_struct &&
-         to_struct_type(expr.type()).has_component(component_name)) ||
-        (expr.type().id() == ID_struct_tag &&
-         ns.follow_tag(to_struct_tag_type(expr.type()))
-           .has_component(component_name)))
+      if(!any_matching_suffix && all_matching_component_names)
       {
         // Looking for a non-overwritten member, look through this expression
         get_value_set_rec(
@@ -1003,7 +1015,7 @@ void value_sett::get_value_set_rec(
           original_type,
           ns);
       }
-      else
+      else if(!any_matching_suffix)
       {
         // Member we're looking for is not defined in this struct -- this
         // must be a reinterpret cast of some sort. Default to conservatively
@@ -1015,13 +1027,16 @@ void value_sett::get_value_set_rec(
           suffix,
           original_type,
           ns);
-        get_value_set_rec(
-          with_expr.new_value(),
-          dest,
-          includes_nondet_pointer,
-          "",
-          original_type,
-          ns);
+        for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
+        {
+          get_value_set_rec(
+            with_expr.operands()[i + 1],
+            dest,
+            includes_nondet_pointer,
+            "",
+            original_type,
+            ns);
+        }
       }
     }
     else if(expr.type().id() == ID_array && !suffix.empty())
@@ -1040,13 +1055,16 @@ void value_sett::get_value_set_rec(
         suffix,
         original_type,
         ns);
-      get_value_set_rec(
-        with_expr.new_value(),
-        dest,
-        includes_nondet_pointer,
-        new_value_suffix,
-        original_type,
-        ns);
+      for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
+      {
+        get_value_set_rec(
+          with_expr.operands()[i + 1],
+          dest,
+          includes_nondet_pointer,
+          new_value_suffix,
+          original_type,
+          ns);
+      }
     }
     else
     {
@@ -1059,13 +1077,16 @@ void value_sett::get_value_set_rec(
         suffix,
         original_type,
         ns);
-      get_value_set_rec(
-        with_expr.new_value(),
-        dest,
-        includes_nondet_pointer,
-        "",
-        original_type,
-        ns);
+      for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
+      {
+        get_value_set_rec(
+          with_expr.operands()[i + 1],
+          dest,
+          includes_nondet_pointer,
+          "",
+          original_type,
+          ns);
+      }
     }
   }
   else if(expr.id()==ID_array)
@@ -1624,14 +1645,18 @@ void value_sett::assign(
       }
       else if(rhs.id()==ID_with)
       {
+        const with_exprt &with_expr = to_with_expr(rhs);
         const index_exprt op0_index(
-          to_with_expr(rhs).old(),
+          with_expr.old(),
           exprt(ID_unknown, c_index_type()),
           to_array_type(lhs.type()).element_type());
 
         assign(lhs_index, op0_index, ns, is_simplified, add_to_sets);
-        assign(
-          lhs_index, to_with_expr(rhs).new_value(), ns, is_simplified, true);
+        for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
+        {
+          assign(
+            lhs_index, with_expr.operands()[i + 1], ns, is_simplified, true);
+        }
       }
       else
       {
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index bf634d07264..dde28bba109 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -1058,17 +1058,21 @@ void value_set_fit::assign(
         {
           // see if this is the member we want
           const auto &rhs_with = to_with_expr(rhs);
-          const exprt &member_operand = rhs_with.where();
+          bool member_found = false;
+          for(std::size_t i = 1; i < rhs_with.operands().size(); i += 2)
+          {
+            const exprt &member_operand = rhs_with.operands()[i];
 
-          const irep_idt &component_name=
-            member_operand.get(ID_component_name);
+            const irep_idt &component_name =
+              member_operand.get(ID_component_name);
 
-          if(component_name==name)
-          {
-            // yes! just take op2
-            rhs_member = rhs_with.new_value();
+            if(component_name == name)
+            {
+              rhs_member = rhs_with.operands()[i + 1];
+              member_found = true;
+            }
           }
-          else
+          if(!member_found)
           {
             // no! do op0
             rhs_member=exprt(ID_member, subtype);
@@ -1126,13 +1130,17 @@ void value_set_fit::assign(
       }
       else if(rhs.id()==ID_with)
       {
+        const with_exprt &with_expr = to_with_expr(rhs);
         const index_exprt op0_index(
-          to_with_expr(rhs).old(),
+          with_expr.old(),
           exprt(ID_unknown, c_index_type()),
           to_array_type(lhs.type()).element_type());
 
         assign(lhs_index, op0_index, ns);
-        assign(lhs_index, to_with_expr(rhs).new_value(), ns);
+        for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
+        {
+          assign(lhs_index, with_expr.operands()[i + 1], ns);
+        }
       }
       else
       {
diff --git a/src/solvers/smt2/smt2_format.cpp b/src/solvers/smt2/smt2_format.cpp
index a4771c632fe..49dbb23194f 100644
--- a/src/solvers/smt2/smt2_format.cpp
+++ b/src/solvers/smt2/smt2_format.cpp
@@ -139,9 +139,14 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
   else if(expr.id() == ID_with && expr.type().id() == ID_array)
   {
     const auto &with_expr = to_with_expr(expr);
-    out << "(store " << smt2_format(with_expr.old()) << ' '
-        << smt2_format(with_expr.where()) << ' '
-        << smt2_format(with_expr.new_value()) << ')';
+    for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
+      out << "(store ";
+    out << smt2_format(with_expr.old()) << ' ';
+    for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
+    {
+      out << smt2_format(with_expr.operands()[i]) << ' '
+          << smt2_format(with_expr.operands()[i + 1]) << ')';
+    }
   }
   else if(expr.id() == ID_array_list)
   {
diff --git a/src/solvers/strings/string_refinement_util.cpp b/src/solvers/strings/string_refinement_util.cpp
index db1cc2a57c1..80b1fc600b0 100644
--- a/src/solvers/strings/string_refinement_util.cpp
+++ b/src/solvers/strings/string_refinement_util.cpp
@@ -70,9 +70,12 @@ sparse_arrayt::sparse_arrayt(const with_exprt &expr)
   while(can_cast_expr<with_exprt>(ref.get()))
   {
     const auto &with_expr = expr_dynamic_cast<with_exprt>(ref.get());
-    const auto current_index =
-      numeric_cast_v<std::size_t>(to_constant_expr(with_expr.where()));
-    entries[current_index] = with_expr.new_value();
+    for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
+    {
+      const auto current_index =
+        numeric_cast_v<std::size_t>(to_constant_expr(with_expr.operands()[i]));
+      entries[current_index] = with_expr.operands()[i + 1];
+    }
     ref = with_expr.old();
   }
 
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index b6f19abda7b..46eb3c11825 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -2157,7 +2157,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
    *             value)
    */
 
-  if(value.id()==ID_with)
+  if(value.id() == ID_with && value.operands().size() == 3)
   {
     const with_exprt &with=to_with_expr(value);
 
@@ -2297,6 +2297,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
 
         if(
           expr_at_offset_C.id() == ID_with &&
+          expr_at_offset_C.operands().size() == 3 &&
           to_with_expr(expr_at_offset_C).where().is_zero())
         {
           tmp.set_op(to_with_expr(expr_at_offset_C).old());