diff --git a/src/solvers/flattening/boolbv_array.cpp b/src/solvers/flattening/boolbv_array.cpp
index c6a62419738..983cfae9e0a 100644
--- a/src/solvers/flattening/boolbv_array.cpp
+++ b/src/solvers/flattening/boolbv_array.cpp
@@ -27,7 +27,6 @@ bvt boolbvt::convert_array(const exprt &expr)
       expr.has_operands(),
       "the bit width being nonzero implies that the array has a nonzero size "
       "in which case the array shall have operands");
-    const exprt::operandst &operands=expr.operands();
     const std::size_t op_width = width / operands.size();
 
     bvt bv;
diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp
index ec455047d70..f9e7749d928 100644
--- a/src/solvers/flattening/boolbv_byte_extract.cpp
+++ b/src/solvers/flattening/boolbv_byte_extract.cpp
@@ -103,7 +103,6 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   }
 
   const exprt &op=expr.op();
-  const exprt &offset=expr.offset();
   PRECONDITION(
     expr.id() == ID_byte_extract_little_endian ||
     expr.id() == ID_byte_extract_big_endian);
@@ -145,9 +144,10 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
       // add implications
 
       equal_exprt equality;
-      equality.lhs()=offset; // index operand
+      equality.lhs() = expr.offset(); // index operand
 
-      typet constant_type=offset.type(); // type of index operand
+      // type of index operand
+      const typet &constant_type = expr.offset().type();
 
       bvt equal_bv;
       equal_bv.resize(width);
@@ -171,9 +171,10 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
     else
     {
       equal_exprt equality;
-      equality.lhs()=offset; // index operand
+      equality.lhs() = expr.offset(); // index operand
 
-      typet constant_type(offset.type()); // type of index operand
+      // type of index operand
+      const typet &constant_type = expr.offset().type();
 
       for(std::size_t i=0; i<bytes; i++)
       {
diff --git a/src/solvers/flattening/boolbv_cond.cpp b/src/solvers/flattening/boolbv_cond.cpp
index 29a36f72588..8798abbece1 100644
--- a/src/solvers/flattening/boolbv_cond.cpp
+++ b/src/solvers/flattening/boolbv_cond.cpp
@@ -74,8 +74,8 @@ bvt boolbvt::convert_cond(const cond_exprt &expr)
 
       const bvt &op = convert_bv(value, bv.size());
 
-      for(std::size_t i=0; i<bv.size(); i++)
-        bv[i]=prop.lselect(cond_literal, op[i], bv[i]);
+      for(std::size_t j = 0; j < bv.size(); j++)
+        bv[j] = prop.lselect(cond_literal, op[j], bv[j]);
     }
   }
 
diff --git a/src/solvers/flattening/bv_dimacs.cpp b/src/solvers/flattening/bv_dimacs.cpp
index 60079185227..d0d627f6a35 100644
--- a/src/solvers/flattening/bv_dimacs.cpp
+++ b/src/solvers/flattening/bv_dimacs.cpp
@@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <solvers/sat/dimacs_cnf.h>
 
-bool bv_dimacst::write_dimacs(const std::string &filename)
+bool bv_dimacst::write_dimacs()
 {
   if(filename.empty() || filename == "-")
     return write_dimacs(std::cout);
diff --git a/src/solvers/flattening/bv_dimacs.h b/src/solvers/flattening/bv_dimacs.h
index c6fded199aa..c7dbedb8a0d 100644
--- a/src/solvers/flattening/bv_dimacs.h
+++ b/src/solvers/flattening/bv_dimacs.h
@@ -24,12 +24,12 @@ class bv_dimacst : public bv_pointerst
 
   virtual ~bv_dimacst()
   {
-    write_dimacs(filename);
+    write_dimacs();
   }
 
 protected:
-  std::string filename;
-  bool write_dimacs(const std::string &filename);
+  const std::string filename;
+  bool write_dimacs();
   bool write_dimacs(std::ostream &);
 };
 
diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp
index 00883e1e427..7da44f745c5 100644
--- a/src/solvers/lowering/byte_operators.cpp
+++ b/src/solvers/lowering/byte_operators.cpp
@@ -648,8 +648,7 @@ exprt lower_byte_operators(const exprt &src, const namespacet &ns)
   // destroys any sharing, should use hash table
   Forall_operands(it, tmp)
   {
-    exprt tmp=lower_byte_operators(*it, ns);
-    it->swap(tmp);
+    *it = lower_byte_operators(*it, ns);
   }
 
   if(src.id()==ID_byte_update_little_endian ||
diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp
index a11bf4b04db..0c9f20884f4 100644
--- a/src/solvers/prop/prop_conv.cpp
+++ b/src/solvers/prop/prop_conv.cpp
@@ -238,11 +238,10 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
       "constraint_select_one should have at least two operands");
 
     std::vector<literalt> op_bv;
-    op_bv.resize(op.size());
+    op_bv.reserve(op.size());
 
-    unsigned i=0;
     forall_operands(it, expr)
-      op_bv[i++]=convert(*it);
+      op_bv.push_back(convert(*it));
 
     // add constraints
 
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index f75b8dbd1ec..c47986a21b1 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -40,12 +40,12 @@ Author: Daniel Kroening, kroening@kroening.com
 // General todos
 #define SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S)
 
-void smt2_convt::print_assignment(std::ostream &out) const
+void smt2_convt::print_assignment(std::ostream &os) const
 {
   // Boolean stuff
 
   for(std::size_t v=0; v<boolean_assignment.size(); v++)
-    out << "b" << v << "=" << boolean_assignment[v] << "\n";
+    os << "b" << v << "=" << boolean_assignment[v] << "\n";
 
   // others
 }
@@ -93,20 +93,21 @@ void smt2_convt::write_header()
     out << "(set-logic " << logic << ")" << "\n";
 }
 
-void smt2_convt::write_footer(std::ostream &out)
+void smt2_convt::write_footer(std::ostream &os)
 {
-  out << "\n";
+  os << "\n";
 
   // add the assumptions, if any
   if(!assumptions.empty())
   {
-    out << "; assumptions\n";
+    os << "; assumptions\n";
 
     forall_literals(it, assumptions)
     {
-      out << "(assert ";
+      os << "(assert ";
       convert_literal(*it);
-      out << ")" << "\n";
+      os << ")"
+         << "\n";
     }
   }
 
@@ -114,20 +115,23 @@ void smt2_convt::write_footer(std::ostream &out)
   for(const auto &object : object_sizes)
     define_object_size(object.second, object.first);
 
-  out << "(check-sat)" << "\n";
-  out << "\n";
+  os << "(check-sat)"
+     << "\n";
+  os << "\n";
 
   if(solver!=solvert::BOOLECTOR)
   {
     for(const auto &id : smt2_identifiers)
-      out << "(get-value (|" << id << "|))" << "\n";
+      os << "(get-value (|" << id << "|))"
+         << "\n";
   }
 
-  out << "\n";
+  os << "\n";
 
-  out << "(exit)\n";
+  os << "(exit)\n";
 
-  out << "; end of SMT2 file" << "\n";
+  os << "; end of SMT2 file"
+     << "\n";
 }
 
 void smt2_convt::define_object_size(
@@ -1503,8 +1507,6 @@ void smt2_convt::convert_expr(const exprt &expr)
     DATA_INVARIANT(
       expr.operands().size() == 1, "width expression should have one operand");
 
-    boolbv_widtht boolbv_width(ns);
-
     std::size_t result_width=boolbv_width(expr.type());
     CHECK_RETURN(result_width != 0);
 
@@ -2671,8 +2673,6 @@ void smt2_convt::convert_union(const union_exprt &expr)
   const union_typet &union_type = to_union_type(ns.follow(expr.type()));
   const exprt &op=expr.op();
 
-  boolbv_widtht boolbv_width(ns);
-
   std::size_t total_width=boolbv_width(union_type);
   CHECK_RETURN_WITH_DIAGNOSTICS(
     total_width != 0, "failed to get union width for union");
@@ -3633,8 +3633,6 @@ void smt2_convt::convert_with(const with_exprt &expr)
 
     const exprt &value=expr.op2();
 
-    boolbv_widtht boolbv_width(ns);
-
     std::size_t total_width=boolbv_width(union_type);
     CHECK_RETURN_WITH_DIAGNOSTICS(
       total_width != 0, "failed to get union width for with");
@@ -4453,8 +4451,6 @@ void smt2_convt::convert_type(const typet &type)
     }
     else
     {
-      boolbv_widtht boolbv_width(ns);
-
       std::size_t width=boolbv_width(type);
       CHECK_RETURN_WITH_DIAGNOSTICS(
         width != 0, "failed to get width of vector");
@@ -4471,8 +4467,6 @@ void smt2_convt::convert_type(const typet &type)
   }
   else if(type.id() == ID_union || type.id() == ID_union_tag)
   {
-    boolbv_widtht boolbv_width(ns);
-
     std::size_t width=boolbv_width(type);
     CHECK_RETURN_WITH_DIAGNOSTICS(width != 0, "failed to get width of union");
 
@@ -4529,8 +4523,6 @@ void smt2_convt::convert_type(const typet &type)
     }
     else
     {
-      boolbv_widtht boolbv_width(ns);
-
       std::size_t width=boolbv_width(type);
       CHECK_RETURN_WITH_DIAGNOSTICS(
         width != 0, "failed to get width of complex");
@@ -4806,11 +4798,11 @@ void smt2_convt::collect_bindings(
   seen_expressionst &map,
   std::vector<exprt> &let_order)
 {
-  seen_expressionst::iterator it = map.find(expr);
+  seen_expressionst::iterator entry = map.find(expr);
 
-  if(it!=map.end())
+  if(entry != map.end())
   {
-    let_count_idt &count_id=it->second;
+    let_count_idt &count_id = entry->second;
     ++(count_id.count);
     return;
   }
diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h
index f8758d04bcc..30a35babee9 100644
--- a/src/solvers/smt2/smt2_conv.h
+++ b/src/solvers/smt2/smt2_conv.h
@@ -118,7 +118,7 @@ class smt2_convt:public prop_convt
   virtual void set_to(const exprt &expr, bool value);
   virtual exprt get(const exprt &expr) const;
   virtual std::string decision_procedure_text() const { return "SMT2"; }
-  virtual void print_assignment(std::ostream &out) const;
+  virtual void print_assignment(std::ostream &) const;
   virtual tvt l_get(literalt l) const;
   virtual void set_assumptions(const bvt &bv) { assumptions=bv; }
 
diff --git a/src/solvers/smt2/smt2_format.cpp b/src/solvers/smt2/smt2_format.cpp
index 1efab965720..a8a3f5ea78d 100644
--- a/src/solvers/smt2/smt2_format.cpp
+++ b/src/solvers/smt2/smt2_format.cpp
@@ -54,9 +54,9 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
     {
       const std::size_t width = to_unsignedbv_type(expr_type).get_width();
 
-      const auto value = numeric_cast_v<mp_integer>(expr);
+      const auto int_value = numeric_cast_v<mp_integer>(expr);
 
-      out << "(_ bv" << value << " " << width << ")";
+      out << "(_ bv" << int_value << " " << width << ")";
     }
     else if(expr_type.id() == ID_bool)
     {