diff --git a/src/cpp/cpp_template_args.h b/src/cpp/cpp_template_args.h
index 18c27b83cae..b30e17b7f4e 100644
--- a/src/cpp/cpp_template_args.h
+++ b/src/cpp/cpp_template_args.h
@@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #ifndef CPROVER_CPP_CPP_TEMPLATE_ARGS_H
 #define CPROVER_CPP_CPP_TEMPLATE_ARGS_H
 
-#include <util/irep.h>
+#include <util/expr.h>
 
 // A data structures for template arguments, i.e.,
 // a sequence of types/expressions of the form <E1, T2, ...>.
@@ -22,7 +22,7 @@ class cpp_template_args_baset:public irept
   {
   }
 
-  typedef std::vector<exprt> argumentst;
+  typedef exprt::operandst argumentst;
 
   argumentst &arguments()
   {
diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp
index 3a2adda985f..6a53c0aa04d 100644
--- a/src/cpp/cpp_typecheck.cpp
+++ b/src/cpp/cpp_typecheck.cpp
@@ -343,7 +343,7 @@ void cpp_typecheckt::do_not_typechecked()
         }
         else if(symbol.value.operands().size()==1)
         {
-          exprt tmp = symbol.value.operands()[0];
+          exprt tmp = symbol.value.op0();
           symbol.value.swap(tmp);
           convert_function(symbol);
           cont=true;
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
index 8e98bf1a937..1bc298665f3 100644
--- a/src/cpp/cpp_typecheck_expr.cpp
+++ b/src/cpp/cpp_typecheck_expr.cpp
@@ -2577,28 +2577,31 @@ void cpp_typecheckt::typecheck_function_call_arguments(
     }
   }
 
-  for(std::size_t i=0; i<parameters.size(); i++)
+  exprt::operandst::iterator arg_it=expr.arguments().begin();
+  for(const auto &parameter : parameters)
   {
-    if(parameters[i].get_bool("#call_by_value"))
+    if(parameter.get_bool("#call_by_value"))
     {
-      assert(is_reference(parameters[i].type()));
+      assert(is_reference(parameter.type()));
 
-      if(expr.arguments()[i].id()!=ID_temporary_object)
+      if(arg_it->id()!=ID_temporary_object)
       {
         // create a temporary for the parameter
 
         exprt arg("already_typechecked");
-        arg.copy_to_operands(expr.arguments()[i]);
+        arg.copy_to_operands(*arg_it);
 
         exprt temporary;
-        new_temporary(expr.arguments()[i].source_location(),
-                      parameters[i].type().subtype(),
-                      arg,
-                      temporary);
-        expr.arguments()[i].swap(temporary);
+        new_temporary(
+          arg_it->source_location(),
+          parameter.type().subtype(),
+          arg,
+          temporary);
+        arg_it->swap(temporary);
       }
-
     }
+
+    ++arg_it;
   }
 
   c_typecheck_baset::typecheck_function_call_arguments(expr);
diff --git a/src/cpp/cpp_typecheck_fargs.cpp b/src/cpp/cpp_typecheck_fargs.cpp
index 48088cd3e6f..b0beff42864 100644
--- a/src/cpp/cpp_typecheck_fargs.cpp
+++ b/src/cpp/cpp_typecheck_fargs.cpp
@@ -83,7 +83,7 @@ bool cpp_typecheck_fargst::match(
 {
   distance=0;
 
-  exprt::operandst ops = operands;
+  exprt::operandst ops=operands;
   const code_typet::parameterst &parameters=code_type.parameters();
 
   if(parameters.size()>ops.size())
@@ -109,7 +109,8 @@ bool cpp_typecheck_fargst::match(
       return false;
   }
 
-  for(std::size_t i=0; i<ops.size(); i++)
+  exprt::operandst::iterator it=ops.begin();
+  for(const auto &parameter : parameters)
   {
     // read
     // http://publib.boulder.ibm.com/infocenter/comphelp/v8v101/topic/com.ibm.xlcpp8a.doc/language/ref/implicit_conversion_sequences.htm
@@ -119,16 +120,9 @@ bool cpp_typecheck_fargst::match(
     // * User-defined conversion sequences
     // * Ellipsis conversion sequences
 
-    if(i>=parameters.size())
-    {
-      // Ellipsis is the 'worst' of the conversion sequences
-      distance+=1000;
-      continue;
-    }
-
-    exprt parameter=parameters[i];
-
-    exprt &operand=ops[i];
+    assert(it!=ops.end());
+    const exprt &operand=*it;
+    typet type=parameter.type();
 
     #if 0
     // unclear, todo
@@ -140,13 +134,13 @@ bool cpp_typecheck_fargst::match(
 
     // "this" is a special case -- we turn the pointer type
     // into a reference type to do the type matching
-    if(i==0 && parameter.get(ID_C_base_name)==ID_this)
+    if(it==ops.begin() && parameter.get(ID_C_base_name)==ID_this)
     {
-      parameter.type().set(ID_C_reference, true);
-      parameter.type().set("#this", true);
+      type.set(ID_C_reference, true);
+      type.set("#this", true);
     }
 
-    unsigned rank = 0;
+    unsigned rank=0;
     exprt new_expr;
 
     #if 0
@@ -156,7 +150,7 @@ bool cpp_typecheck_fargst::match(
 
     // can we do the standard conversion sequence?
     if(cpp_typecheck.implicit_conversion_sequence(
-        operand, parameter.type(), new_expr, rank))
+        operand, type, new_expr, rank))
     {
       // ok
       distance+=rank;
@@ -171,7 +165,14 @@ bool cpp_typecheck_fargst::match(
       #endif
       return false; // no conversion possible
     }
+
+    ++it;
   }
 
+  // we may not have used all operands
+  for( ; it!=ops.end(); ++it)
+    // Ellipsis is the 'worst' of the conversion sequences
+    distance+=1000;
+
   return true;
 }
diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp
index 3974920870c..e8502c1419a 100644
--- a/src/cpp/cpp_typecheck_resolve.cpp
+++ b/src/cpp/cpp_typecheck_resolve.cpp
@@ -358,7 +358,7 @@ exprt cpp_typecheck_resolvet::convert_identifier(
       {
         // the object is given to us in fargs
         assert(!fargs.operands.empty());
-        object=fargs.operands[0];
+        object=fargs.operands.front();
       }
       else if(this_expr.is_not_nil())
       {
@@ -841,7 +841,7 @@ exprt cpp_typecheck_resolvet::do_builtin(
       throw 0;
     }
 
-    const exprt &argument=arguments[0];
+    const exprt &argument=arguments.front();
 
     if(argument.id()==ID_type)
     {
@@ -2193,13 +2193,16 @@ exprt cpp_typecheck_resolvet::guess_function_template_args(
   const irept::subt &parameters=
     function_declarator.type().find(ID_parameters).get_sub();
 
-  for(std::size_t i=0; i<parameters.size(); i++)
+  exprt::operandst::const_iterator it=fargs.operands.begin();
+  for(const auto & parameter : parameters)
   {
-    if(i<fargs.operands.size() &&
-       parameters[i].id()==ID_cpp_declaration)
+    if(it==fargs.operands.end())
+      break;
+
+    if(parameter.id()==ID_cpp_declaration)
     {
       const cpp_declarationt &arg_declaration=
-        to_cpp_declaration(parameters[i]);
+        to_cpp_declaration(parameter);
 
       // again, there should be one declarator
       assert(arg_declaration.declarators().size()==1);
@@ -2214,8 +2217,10 @@ exprt cpp_typecheck_resolvet::guess_function_template_args(
       // sorts of trouble.
       cpp_convert_plain_type(arg_type);
 
-      guess_template_args(arg_type, fargs.operands[i].type());
+      guess_template_args(arg_type, it->type());
     }
+
+    ++it;
   }
 
   // see if that has worked out
@@ -2633,10 +2638,9 @@ void cpp_typecheck_resolvet::resolve_with_arguments(
   const cpp_typecheck_fargst &fargs)
 {
   // not clear what this is good for
-  for(std::size_t i=0; i<fargs.operands.size(); i++)
+  for(const auto & arg : fargs.operands)
   {
-    const typet &final_type=
-      cpp_typecheck.follow(fargs.operands[i].type());
+    const typet &final_type=cpp_typecheck.follow(arg.type());
 
     if(final_type.id()!=ID_struct && final_type.id()!=ID_union)
       continue;
diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp
index 49e7b8331ee..6787d658db5 100644
--- a/src/solvers/flattening/boolbv_get.cpp
+++ b/src/solvers/flattening/boolbv_get.cpp
@@ -213,11 +213,11 @@ exprt boolbvt::bv_get_rec(
       {
         std::size_t size=width/sub_width;
         exprt value(ID_vector, type);
-        value.operands().resize(size);
+        value.reserve_operands(size);
 
         for(std::size_t i=0; i<size; i++)
-          value.operands()[i]=
-            bv_get_rec(bv, unknown, i*sub_width, subtype);
+          value.operands().push_back(
+            bv_get_rec(bv, unknown, i*sub_width, subtype));
 
         return value;
       }
diff --git a/src/solvers/flattening/boolbv_struct.cpp b/src/solvers/flattening/boolbv_struct.cpp
index caf13889d86..73d929504b0 100644
--- a/src/solvers/flattening/boolbv_struct.cpp
+++ b/src/solvers/flattening/boolbv_struct.cpp
@@ -41,15 +41,13 @@ bvt boolbvt::convert_struct(const struct_exprt &expr)
   bvt bv;
   bv.resize(width);
 
-  std::size_t offset=0, i=0;
+  std::size_t offset=0;
 
-  for(struct_typet::componentst::const_iterator
-      it=components.begin();
-      it!=components.end();
-      it++)
+  exprt::operandst::const_iterator op_it=expr.operands().begin();
+  for(const auto & comp : components)
   {
-    const typet &subtype=it->type();
-    const exprt &op=expr.operands()[i];
+    const typet &subtype=comp.type();
+    const exprt &op=*op_it;
 
     if(!base_type_eq(subtype, op.type(), ns))
     {
@@ -76,7 +74,7 @@ bvt boolbvt::convert_struct(const struct_exprt &expr)
       offset+=op_bv.size();
     }
 
-    i++;
+    ++op_it;
   }
 
   assert(offset==width);
diff --git a/src/solvers/flattening/flatten_byte_operators.cpp b/src/solvers/flattening/flatten_byte_operators.cpp
index 2f27e88b05b..bd3d4198da6 100644
--- a/src/solvers/flattening/flatten_byte_operators.cpp
+++ b/src/solvers/flattening/flatten_byte_operators.cpp
@@ -87,7 +87,7 @@ exprt flatten_byte_extract(
       // TODO this doesn't seem correct if size_bits%8!=0 as more
       // bits than the original expression will be returned.
       if(width_bytes==1)
-        return op[0];
+        return op.front();
       else // width_bytes>=2
       {
         concatenation_exprt concatenation(src.type());
diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp
index b717ff6f836..e8bdcbdfb11 100644
--- a/src/solvers/prop/prop_conv.cpp
+++ b/src/solvers/prop/prop_conv.cpp
@@ -399,7 +399,7 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
     if(op.size()!=1)
       throw "not takes one operand";
 
-    return !convert(op[0]);
+    return !convert(op.front());
   }
   else if(expr.id()==ID_equal || expr.id()==ID_notequal)
   {
diff --git a/src/util/base_type.cpp b/src/util/base_type.cpp
index 898c235db05..2090d863339 100644
--- a/src/util/base_type.cpp
+++ b/src/util/base_type.cpp
@@ -301,11 +301,16 @@ bool base_type_eqt::base_type_eq_rec(
   if(!base_type_eq(expr1.type(), expr2.type()))
     return false;
 
-  if(expr1.operands().size()!=expr2.operands().size())
+  const exprt::operandst &expr1_op=expr1.operands();
+  const exprt::operandst &expr2_op=expr2.operands();
+  if(expr1_op.size()!=expr2_op.size())
     return false;
 
-  for(unsigned i=0; i<expr1.operands().size(); i++)
-    if(!base_type_eq(expr1.operands()[i], expr2.operands()[i]))
+  for(exprt::operandst::const_iterator
+      it1=expr1_op.begin(), it2=expr2_op.begin();
+      it1!=expr1_op.end() && it2!=expr2_op.end();
+      ++it1, ++it2)
+    if(!base_type_eq(*it1, *it2))
       return false;
 
   if(expr1.id()==ID_constant)
diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp
index 135f64a6313..b7034bda43c 100644
--- a/src/util/expr_util.cpp
+++ b/src/util/expr_util.cpp
@@ -234,15 +234,18 @@ exprt make_binary(const exprt &expr)
 
   if(operands.size()<=2) return expr;
 
-  exprt previous=operands[0];
+  exprt previous=operands.front();
 
-  for(std::size_t i=1; i<operands.size(); i++)
+  for(exprt::operandst::const_iterator
+      it=++operands.begin();
+      it!=operands.end();
+      ++it)
   {
     exprt tmp=expr;
     tmp.operands().clear();
     tmp.operands().resize(2);
     tmp.op0().swap(previous);
-    tmp.op1()=operands[i];
+    tmp.op1()=*it;
     previous.swap(tmp);
   }
 
diff --git a/src/util/std_code.h b/src/util/std_code.h
index b7786cb6571..2f58d71352e 100644
--- a/src/util/std_code.h
+++ b/src/util/std_code.h
@@ -69,7 +69,7 @@ class code_blockt:public codet
   explicit code_blockt(const std::list<codet> &_list):codet(ID_block)
   {
     operandst &o=operands();
-    o.reserve(_list.size());
+    reserve_operands(_list.size());
     for(std::list<codet>::const_iterator
         it=_list.begin();
         it!=_list.end();
@@ -281,8 +281,7 @@ class code_assumet:public codet
 public:
   inline code_assumet():codet(ID_assume)
   {
-    // will change to resize(1) in the future
-    operands().reserve(1);
+    operands().resize(1);
   }
 
   inline explicit code_assumet(const exprt &expr):codet(ID_assume)
@@ -320,8 +319,7 @@ class code_assertt:public codet
 public:
   inline code_assertt():codet(ID_assert)
   {
-    // will change to resize(1) in the future
-    operands().reserve(1);
+    operands().resize(1);
   }
 
   inline explicit code_assertt(const exprt &expr):codet(ID_assert)
@@ -723,7 +721,8 @@ class code_returnt:public codet
 public:
   inline code_returnt():codet(ID_return)
   {
-    operands().reserve(1);
+    operands().resize(1);
+    op0().make_nil();
   }
 
   explicit inline code_returnt(const exprt &_op):codet(ID_return)
@@ -738,13 +737,14 @@ class code_returnt:public codet
 
   inline exprt &return_value()
   {
-    operands().resize(1);
     return op0();
   }
 
   inline bool has_return_value() const
   {
-    return operands().size()==1;
+    if(operands().empty())
+      return false; // backwards compatibility
+    return return_value().is_not_nil();
   }
 };
 
@@ -931,7 +931,7 @@ class code_asmt:public codet
 
   inline explicit code_asmt(const exprt &expr):codet(ID_asm)
   {
-    operands().push_back(expr);
+    copy_to_operands(expr);
   }
 
   inline const irep_idt &get_flavor() const
@@ -969,7 +969,7 @@ class code_expressiont:public codet
 
   inline explicit code_expressiont(const exprt &expr):codet(ID_expression)
   {
-    operands().push_back(expr);
+    copy_to_operands(expr);
   }
 
   inline friend code_expressiont &to_code_expression(codet &code)