diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
index fb88fa73fd76..2daa9d26cc1d 100644
--- a/src/solvers/flattening/boolbv.h
+++ b/src/solvers/flattening/boolbv.h
@@ -198,34 +198,34 @@ class boolbvt:public arrayst
 
   void convert_with(
     const typet &type,
-    const exprt &op1,
-    const exprt &op2,
+    const exprt &where,
+    const exprt &new_value,
     const bvt &prev_bv,
     bvt &next_bv);
 
   void convert_with_bv(
-    const exprt &op1,
-    const exprt &op2,
+    const exprt &index,
+    const exprt &new_value,
     const bvt &prev_bv,
     bvt &next_bv);
 
   void convert_with_array(
     const array_typet &type,
-    const exprt &op1,
-    const exprt &op2,
+    const exprt &index,
+    const exprt &new_value,
     const bvt &prev_bv,
     bvt &next_bv);
 
   void convert_with_union(
     const union_typet &type,
-    const exprt &op2,
+    const exprt &new_value,
     const bvt &prev_bv,
     bvt &next_bv);
 
   void convert_with_struct(
     const struct_typet &type,
-    const exprt &op1,
-    const exprt &op2,
+    const exprt &where,
+    const exprt &new_value,
     const bvt &prev_bv,
     bvt &next_bv);
 
diff --git a/src/solvers/flattening/boolbv_with.cpp b/src/solvers/flattening/boolbv_with.cpp
index 578004eec988..3d298937ffc0 100644
--- a/src/solvers/flattening/boolbv_with.cpp
+++ b/src/solvers/flattening/boolbv_with.cpp
@@ -47,8 +47,8 @@ bvt boolbvt::convert_with(const with_exprt &expr)
 
 void boolbvt::convert_with(
   const typet &type,
-  const exprt &op1,
-  const exprt &op2,
+  const exprt &where,
+  const exprt &new_value,
   const bvt &prev_bv,
   bvt &next_bv)
 {
@@ -57,22 +57,31 @@ void boolbvt::convert_with(
   next_bv.resize(prev_bv.size());
 
   if(type.id()==ID_array)
-    return convert_with_array(to_array_type(type), op1, op2, prev_bv, next_bv);
+    return convert_with_array(
+      to_array_type(type), where, new_value, prev_bv, next_bv);
   else if(type.id()==ID_bv ||
           type.id()==ID_unsignedbv ||
           type.id()==ID_signedbv)
-    return convert_with_bv(op1, op2, prev_bv, next_bv);
+    return convert_with_bv(where, new_value, prev_bv, next_bv);
   else if(type.id()==ID_struct)
-    return
-      convert_with_struct(to_struct_type(type), op1, op2, prev_bv, next_bv);
+    return convert_with_struct(
+      to_struct_type(type), where, new_value, prev_bv, next_bv);
   else if(type.id() == ID_struct_tag)
     return convert_with(
-      ns.follow_tag(to_struct_tag_type(type)), op1, op2, prev_bv, next_bv);
+      ns.follow_tag(to_struct_tag_type(type)),
+      where,
+      new_value,
+      prev_bv,
+      next_bv);
   else if(type.id()==ID_union)
-    return convert_with_union(to_union_type(type), op2, prev_bv, next_bv);
+    return convert_with_union(to_union_type(type), new_value, prev_bv, next_bv);
   else if(type.id() == ID_union_tag)
     return convert_with(
-      ns.follow_tag(to_union_tag_type(type)), op1, op2, prev_bv, next_bv);
+      ns.follow_tag(to_union_tag_type(type)),
+      where,
+      new_value,
+      prev_bv,
+      next_bv);
 
   DATA_INVARIANT_WITH_DIAGNOSTICS(
     false, "unexpected with type", irep_pretty_diagnosticst{type});
@@ -80,8 +89,8 @@ void boolbvt::convert_with(
 
 void boolbvt::convert_with_array(
   const array_typet &type,
-  const exprt &op1,
-  const exprt &op2,
+  const exprt &index,
+  const exprt &new_value,
   const bvt &prev_bv,
   bvt &next_bv)
 {
@@ -100,72 +109,73 @@ void boolbvt::convert_with_array(
     "convert_with_array expects constant array size",
     irep_pretty_diagnosticst{type});
 
-  const bvt &op2_bv=convert_bv(op2);
+  const bvt &new_value_bv = convert_bv(new_value);
 
   DATA_INVARIANT_WITH_DIAGNOSTICS(
-    *size * op2_bv.size() == prev_bv.size(),
-    "convert_with_array: unexpected operand 2 width",
+    *size * new_value_bv.size() == prev_bv.size(),
+    "convert_with_array: unexpected new_value operand width",
     irep_pretty_diagnosticst{type});
 
   // Is the index a constant?
-  if(const auto op1_value = numeric_cast<mp_integer>(op1))
+  if(const auto index_value_opt = numeric_cast<mp_integer>(index))
   {
     // Yes, it is!
     next_bv=prev_bv;
 
-    if(*op1_value >= 0 && *op1_value < *size) // bounds check
+    if(*index_value_opt >= 0 && *index_value_opt < *size) // bounds check
     {
       const std::size_t offset =
-        numeric_cast_v<std::size_t>(*op1_value * op2_bv.size());
+        numeric_cast_v<std::size_t>(*index_value_opt * new_value_bv.size());
 
-      for(std::size_t j=0; j<op2_bv.size(); j++)
-        next_bv[offset+j]=op2_bv[j];
+      for(std::size_t j = 0; j < new_value_bv.size(); j++)
+        next_bv[offset + j] = new_value_bv[j];
     }
 
     return;
   }
 
-  typet counter_type=op1.type();
+  typet counter_type = index.type();
 
   for(mp_integer i=0; i<size; i=i+1)
   {
     exprt counter=from_integer(i, counter_type);
 
-    literalt eq_lit=convert(equal_exprt(op1, counter));
+    literalt eq_lit = convert(equal_exprt(index, counter));
 
-    const std::size_t offset = numeric_cast_v<std::size_t>(i * op2_bv.size());
+    const std::size_t offset =
+      numeric_cast_v<std::size_t>(i * new_value_bv.size());
 
-    for(std::size_t j=0; j<op2_bv.size(); j++)
-      next_bv[offset+j]=
-        prop.lselect(eq_lit, op2_bv[j], prev_bv[offset+j]);
+    for(std::size_t j = 0; j < new_value_bv.size(); j++)
+      next_bv[offset + j] =
+        prop.lselect(eq_lit, new_value_bv[j], prev_bv[offset + j]);
   }
 }
 
 void boolbvt::convert_with_bv(
-  const exprt &op1,
-  const exprt &op2,
+  const exprt &index,
+  const exprt &new_value,
   const bvt &prev_bv,
   bvt &next_bv)
 {
-  literalt l=convert(op2);
+  literalt l = convert(new_value);
 
-  if(const auto op1_value = numeric_cast<mp_integer>(op1))
+  if(const auto index_value_opt = numeric_cast<mp_integer>(index))
   {
     next_bv=prev_bv;
 
-    if(*op1_value < next_bv.size())
-      next_bv[numeric_cast_v<std::size_t>(*op1_value)] = l;
+    if(*index_value_opt >= 0 && *index_value_opt < next_bv.size())
+      next_bv[numeric_cast_v<std::size_t>(*index_value_opt)] = l;
 
     return;
   }
 
-  typet counter_type=op1.type();
+  typet counter_type = index.type();
 
   for(std::size_t i=0; i<prev_bv.size(); i++)
   {
     exprt counter=from_integer(i, counter_type);
 
-    literalt eq_lit=convert(equal_exprt(op1, counter));
+    literalt eq_lit = convert(equal_exprt(index, counter));
 
     next_bv[i]=prop.lselect(eq_lit, l, prev_bv[i]);
   }
@@ -173,16 +183,16 @@ void boolbvt::convert_with_bv(
 
 void boolbvt::convert_with_struct(
   const struct_typet &type,
-  const exprt &op1,
-  const exprt &op2,
+  const exprt &where,
+  const exprt &new_value,
   const bvt &prev_bv,
   bvt &next_bv)
 {
   next_bv=prev_bv;
 
-  const bvt &op2_bv=convert_bv(op2);
+  const bvt &new_value_bv = convert_bv(new_value);
 
-  const irep_idt &component_name=op1.get(ID_component_name);
+  const irep_idt &component_name = where.get(ID_component_name);
   const struct_typet::componentst &components=
     type.components();
 
@@ -197,19 +207,19 @@ void boolbvt::convert_with_struct(
     if(c.get_name() == component_name)
     {
       DATA_INVARIANT_WITH_DIAGNOSTICS(
-        subtype == op2.type(),
+        subtype == new_value.type(),
         "with/struct: component '" + id2string(component_name) +
           "' type does not match",
         irep_pretty_diagnosticst{subtype},
-        irep_pretty_diagnosticst{op2.type()});
+        irep_pretty_diagnosticst{new_value.type()});
 
       DATA_INVARIANT_WITH_DIAGNOSTICS(
-        sub_width == op2_bv.size(),
-        "convert_with_struct: unexpected operand op2 width",
+        sub_width == new_value_bv.size(),
+        "convert_with_struct: unexpected new_value operand width",
         irep_pretty_diagnosticst{type});
 
       for(std::size_t i=0; i<sub_width; i++)
-        next_bv[offset+i]=op2_bv[i];
+        next_bv[offset + i] = new_value_bv[i];
 
       break; // done
     }
@@ -220,22 +230,22 @@ void boolbvt::convert_with_struct(
 
 void boolbvt::convert_with_union(
   const union_typet &type,
-  const exprt &op2,
+  const exprt &new_value,
   const bvt &prev_bv,
   bvt &next_bv)
 {
   next_bv=prev_bv;
 
-  const bvt &op2_bv=convert_bv(op2);
+  const bvt &new_value_bv = convert_bv(new_value);
 
   DATA_INVARIANT_WITH_DIAGNOSTICS(
-    next_bv.size() >= op2_bv.size(),
-    "convert_with_union: unexpected operand op2 width",
+    next_bv.size() >= new_value_bv.size(),
+    "convert_with_union: unexpected new_value operand width",
     irep_pretty_diagnosticst{type});
 
   endianness_mapt map_u = endianness_map(type);
-  endianness_mapt map_op2 = endianness_map(op2.type());
+  endianness_mapt map_new_value = endianness_map(new_value.type());
 
-  for(std::size_t i = 0; i < op2_bv.size(); i++)
-    next_bv[map_u.map_bit(i)] = op2_bv[map_op2.map_bit(i)];
+  for(std::size_t i = 0; i < new_value_bv.size(); i++)
+    next_bv[map_u.map_bit(i)] = new_value_bv[map_new_value.map_bit(i)];
 }