diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index e0c3d935164..3e085b964aa 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -81,7 +81,8 @@ void c_typecheck_baset::add_rounding_mode(exprt &expr)
       else
         UNREACHABLE;
 
-      expr.op2()=from_integer(0, unsigned_int_type());
+      to_ieee_float_op_expr(expr).rounding_mode() =
+        from_integer(0, unsigned_int_type());
     }
   }
 }
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index f9bf56d92d4..f69408e88aa 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -782,14 +782,11 @@ std::string expr2ct::convert_typecast(
 }
 
 std::string expr2ct::convert_trinary(
-  const exprt &src,
+  const ternary_exprt &src,
   const std::string &symbol1,
   const std::string &symbol2,
   unsigned precedence)
 {
-  if(src.operands().size()!=3)
-    return convert_norep(src, precedence);
-
   const exprt &op0=src.op0();
   const exprt &op1=src.op1();
   const exprt &op2=src.op2();
@@ -3346,18 +3343,14 @@ std::string expr2ct::convert_extractbit(
   return dest;
 }
 
-std::string expr2ct::convert_extractbits(
-  const exprt &src,
-  unsigned precedence)
+std::string
+expr2ct::convert_extractbits(const extractbits_exprt &src, unsigned precedence)
 {
-  if(src.operands().size()!=3)
-    return convert_norep(src, precedence);
-
-  std::string dest=convert_with_precedence(src.op0(), precedence);
+  std::string dest = convert_with_precedence(src.src(), precedence);
   dest+='[';
-  dest+=convert_with_precedence(src.op1(), precedence);
+  dest += convert_with_precedence(src.upper(), precedence);
   dest+=", ";
-  dest+=convert_with_precedence(src.op2(), precedence);
+  dest += convert_with_precedence(src.lower(), precedence);
   dest+=']';
 
   return dest;
@@ -3758,7 +3751,7 @@ std::string expr2ct::convert_with_precedence(
     return convert_binary(src, "==>", precedence=3, true);
 
   else if(src.id()==ID_if)
-    return convert_trinary(src, "?", ":", precedence=3);
+    return convert_trinary(to_if_expr(src), "?", ":", precedence = 3);
 
   else if(src.id()==ID_forall)
     return convert_quantifier(src, "forall", precedence=2);
@@ -3864,7 +3857,7 @@ std::string expr2ct::convert_with_precedence(
     return convert_extractbit(src, precedence);
 
   else if(src.id()==ID_extractbits)
-    return convert_extractbits(src, precedence);
+    return convert_extractbits(to_extractbits_expr(src), precedence);
 
   else if(src.id()==ID_initializer_list ||
           src.id()==ID_compound_literal)
diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h
index e3716910ff8..8536e79a674 100644
--- a/src/ansi-c/expr2c_class.h
+++ b/src/ansi-c/expr2c_class.h
@@ -118,8 +118,10 @@ class expr2ct
   std::string convert_array_of(const exprt &src, unsigned precedence);
 
   std::string convert_trinary(
-    const exprt &src, const std::string &symbol1,
-    const std::string &symbol2, unsigned precedence);
+    const ternary_exprt &src,
+    const std::string &symbol1,
+    const std::string &symbol2,
+    unsigned precedence);
 
   std::string convert_overflow(
     const exprt &src, unsigned &precedence);
@@ -155,9 +157,8 @@ class expr2ct
     const exprt &src,
     unsigned precedence);
 
-  std::string convert_extractbits(
-    const exprt &src,
-    unsigned precedence);
+  std::string
+  convert_extractbits(const extractbits_exprt &src, unsigned precedence);
 
   std::string convert_unary(
     const exprt &src, const std::string &symbol,
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 9df4c4ff51c..2a16a6f3981 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -65,13 +65,13 @@ bool simplify_exprt::simplify_abs(exprt &expr)
   if(expr.operands().size()!=1)
     return true;
 
-  if(expr.op0().is_constant())
+  if(to_unary_expr(expr).op().is_constant())
   {
-    const typet &type = expr.op0().type();
+    const typet &type = to_unary_expr(expr).op().type();
 
     if(type.id()==ID_floatbv)
     {
-      ieee_floatt value(to_constant_expr(expr.op0()));
+      ieee_floatt value(to_constant_expr(to_unary_expr(expr).op()));
       value.set_sign(false);
       expr=value.to_expr();
       return false;
@@ -79,12 +79,12 @@ bool simplify_exprt::simplify_abs(exprt &expr)
     else if(type.id()==ID_signedbv ||
             type.id()==ID_unsignedbv)
     {
-      auto value = numeric_cast<mp_integer>(expr.op0());
+      auto value = numeric_cast<mp_integer>(to_unary_expr(expr).op());
       if(value.has_value())
       {
         if(*value >= 0)
         {
-          expr=expr.op0();
+          expr = to_unary_expr(expr).op();
           return false;
         }
         else
@@ -1221,55 +1221,56 @@ bool simplify_exprt::simplify_with(exprt &expr)
   if((expr.operands().size()%2)!=1)
     return true;
 
-  const typet op0_type=ns.follow(expr.op0().type());
+  auto &with_expr = to_with_expr(expr);
+
+  const typet old_type_followed = ns.follow(with_expr.old().type());
 
   // now look at first operand
 
-  if(op0_type.id()==ID_struct)
+  if(old_type_followed.id() == ID_struct)
   {
-    if(expr.op0().id()==ID_struct ||
-       expr.op0().id()==ID_constant)
+    if(with_expr.old().id() == ID_struct || with_expr.old().id() == ID_constant)
     {
-      while(expr.operands().size()>1)
+      while(with_expr.operands().size() > 1)
       {
-        const irep_idt &component_name=
-          expr.op1().get(ID_component_name);
+        const irep_idt &component_name =
+          with_expr.where().get(ID_component_name);
 
-        if(!to_struct_type(op0_type).
-           has_component(component_name))
+        if(!to_struct_type(old_type_followed).has_component(component_name))
           return result;
 
-        std::size_t number=to_struct_type(op0_type).
-           component_number(component_name);
+        std::size_t number =
+          to_struct_type(old_type_followed).component_number(component_name);
 
-        expr.op0().operands()[number].swap(expr.op2());
+        with_expr.old().operands()[number].swap(with_expr.new_value());
 
-        expr.operands().erase(++expr.operands().begin());
-        expr.operands().erase(++expr.operands().begin());
+        with_expr.operands().erase(++with_expr.operands().begin());
+        with_expr.operands().erase(++with_expr.operands().begin());
 
         result=false;
       }
     }
   }
-  else if(expr.op0().type().id()==ID_array)
+  else if(with_expr.old().type().id() == ID_array)
   {
     if(expr.op0().id()==ID_array ||
        expr.op0().id()==ID_constant)
     {
       while(expr.operands().size()>1)
       {
-        const auto i = numeric_cast<mp_integer>(expr.op1());
+        const auto i = numeric_cast<mp_integer>(with_expr.where());
 
         if(!i.has_value())
           break;
 
-        if(*i < 0 || *i >= expr.op0().operands().size())
+        if(*i < 0 || *i >= with_expr.old().operands().size())
           break;
 
-        expr.op0().operands()[numeric_cast_v<std::size_t>(*i)].swap(expr.op2());
+        with_expr.old().operands()[numeric_cast_v<std::size_t>(*i)].swap(
+          with_expr.new_value());
 
-        expr.operands().erase(++expr.operands().begin());
-        expr.operands().erase(++expr.operands().begin());
+        with_expr.operands().erase(++with_expr.operands().begin());
+        with_expr.operands().erase(++with_expr.operands().begin());
 
         result=false;
       }
@@ -1663,24 +1664,27 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
 
   // byte_extract(byte_update(root, offset, value), offset) =>
   // value
-  if(((expr.id()==ID_byte_extract_big_endian &&
-       expr.op().id()==ID_byte_update_big_endian) ||
-      (expr.id()==ID_byte_extract_little_endian &&
-       expr.op().id()==ID_byte_update_little_endian)) &&
-     expr.offset()==expr.op().op1())
+  if(
+    ((expr.id() == ID_byte_extract_big_endian &&
+      expr.op().id() == ID_byte_update_big_endian) ||
+     (expr.id() == ID_byte_extract_little_endian &&
+      expr.op().id() == ID_byte_update_little_endian)) &&
+    expr.offset() == to_byte_update_expr(expr.op()).offset())
   {
-    if(base_type_eq(expr.type(), expr.op().op2().type(), ns))
+    const auto &op_byte_update = to_byte_update_expr(expr.op());
+
+    if(base_type_eq(expr.type(), op_byte_update.value().type(), ns))
     {
-      exprt tmp=expr.op().op2();
+      exprt tmp = op_byte_update.value();
       expr.swap(tmp);
 
       return false;
     }
     else if(
       el_size.has_value() &&
-      *el_size <= pointer_offset_bits(expr.op().op2().type(), ns))
+      *el_size <= pointer_offset_bits(op_byte_update.value().type(), ns))
     {
-      expr.op()=expr.op().op2();
+      expr.op() = op_byte_update.value();
       expr.offset()=from_integer(0, expr.offset().type());
 
       simplify_byte_extract(expr);
@@ -1811,9 +1815,11 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
 {
   // byte_update(byte_update(root, offset, value), offset, value2) =>
   // byte_update(root, offset, value2)
-  if(expr.id()==expr.op().id() &&
-     expr.offset()==expr.op().op1() &&
-     base_type_eq(expr.value().type(), expr.op().op2().type(), ns))
+  if(
+    expr.id() == expr.op().id() &&
+    expr.offset() == to_byte_update_expr(expr.op()).offset() &&
+    base_type_eq(
+      expr.value().type(), to_byte_update_expr(expr.op()).value().type(), ns))
   {
     expr.op()=expr.op().op0();
     return false;
diff --git a/src/util/simplify_expr_array.cpp b/src/util/simplify_expr_array.cpp
index 02b9d7634b9..a931439af96 100644
--- a/src/util/simplify_expr_array.cpp
+++ b/src/util/simplify_expr_array.cpp
@@ -65,15 +65,15 @@ bool simplify_exprt::simplify_index(exprt &expr)
   {
     // we have (a WITH [i:=e])[j]
 
-    const exprt &with_expr=array;
-
-    if(with_expr.operands().size()!=3)
+    if(array.operands().size() != 3)
       return true;
 
-    if(with_expr.op1()==expr.op1())
+    const auto &with_expr = to_with_expr(array);
+
+    if(with_expr.where() == expr.op1())
     {
       // simplify (e with [i:=v])[i] to v
-      exprt tmp=with_expr.op2();
+      exprt tmp = with_expr.new_value();
       expr.swap(tmp);
       return false;
     }
@@ -82,19 +82,19 @@ bool simplify_exprt::simplify_index(exprt &expr)
       // Turn (a with i:=x)[j] into (i==j)?x:a[j].
       // watch out that the type of i and j might be different.
       const exprt rhs_casted =
-        typecast_exprt::conditional_cast(with_expr.op1(), expr.op1().type());
+        typecast_exprt::conditional_cast(with_expr.where(), expr.op1().type());
 
       equal_exprt equality_expr(expr.op1(), rhs_casted);
 
       simplify_inequality(equality_expr);
 
-      index_exprt new_index_expr(with_expr.op0(), expr.op1(), expr.type());
+      index_exprt new_index_expr(with_expr.old(), expr.op1(), expr.type());
 
       simplify_index(new_index_expr); // recursive call
 
       if(equality_expr.is_true())
       {
-        expr=with_expr.op2();
+        expr = with_expr.new_value();
         return false;
       }
       else if(equality_expr.is_false())
@@ -103,7 +103,7 @@ bool simplify_exprt::simplify_index(exprt &expr)
         return false;
       }
 
-      if_exprt if_expr(equality_expr, with_expr.op2(), new_index_expr);
+      if_exprt if_expr(equality_expr, with_expr.new_value(), new_index_expr);
       simplify_if(if_expr);
 
       expr.swap(if_expr);
diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp
index 2ffda22887b..d44460f541a 100644
--- a/src/util/simplify_expr_floatbv.cpp
+++ b/src/util/simplify_expr_floatbv.cpp
@@ -293,9 +293,9 @@ bool simplify_exprt::simplify_floatbv_op(exprt &expr)
     "binary operations have two operands, here an addtional parameter "
     "is for the rounding mode");
 
-  exprt op0=expr.op0();
-  exprt op1=expr.op1();
-  exprt op2=expr.op2(); // rounding mode
+  exprt op0 = to_ieee_float_op_expr(expr).lhs();
+  exprt op1 = to_ieee_float_op_expr(expr).rhs();
+  exprt op2 = to_ieee_float_op_expr(expr).rounding_mode(); // rounding mode
 
   INVARIANT(
     op0.type() == type,
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index 5f442689504..e2976c07515 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -142,26 +142,28 @@ bool simplify_exprt::simplify_address_of_arg(exprt &expr)
     if(expr.operands().size()==3)
     {
       bool result=true;
-      if(!simplify_rec(expr.op0()))
+      auto &if_expr = to_if_expr(expr);
+
+      if(!simplify_rec(if_expr.cond()))
         result=false;
-      if(!simplify_address_of_arg(expr.op1()))
+      if(!simplify_address_of_arg(if_expr.true_case()))
         result=false;
-      if(!simplify_address_of_arg(expr.op2()))
+      if(!simplify_address_of_arg(if_expr.false_case()))
         result=false;
 
-      // op0 is a constant?
-      if(expr.op0().is_true())
+      // condition is a constant?
+      if(if_expr.cond().is_true())
       {
         result=false;
         exprt tmp;
-        tmp.swap(expr.op1());
+        tmp.swap(if_expr.true_case());
         expr.swap(tmp);
       }
-      else if(expr.op0().is_false())
+      else if(if_expr.cond().is_false())
       {
         result=false;
         exprt tmp;
-        tmp.swap(expr.op2());
+        tmp.swap(if_expr.false_case());
         expr.swap(tmp);
       }