diff --git a/src/cbmc/bv_cbmc.cpp b/src/cbmc/bv_cbmc.cpp
index 06a32d52686..019982f6fd7 100644
--- a/src/cbmc/bv_cbmc.cpp
+++ b/src/cbmc/bv_cbmc.cpp
@@ -20,13 +20,11 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr)
     throw 0;
   }
 
-  exprt new_cycle;
   const exprt &old_cycle=expr.op0();
   const exprt &cycle_var=expr.op1();
   const exprt &bound=expr.op2();
   const exprt &predicate=expr.op3();
-
-  make_free_bv_expr(expr.type(), new_cycle);
+  const exprt new_cycle = make_free_bv_expr(expr.type());
 
   mp_integer bound_value;
   if(to_integer(bound, bound_value))
@@ -98,18 +96,9 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr)
 
 bvt bv_cbmct::convert_waitfor_symbol(const exprt &expr)
 {
-  if(expr.operands().size()!=1)
-  {
-    error().source_location=expr.find_source_location();
-    error() << "waitfor_symbol expected to have one operand" << eom;
-    throw 0;
-  }
-
-  exprt result;
+  PRECONDITION(expr.operands().size() == 1);
   const exprt &bound=expr.op0();
-
-  make_free_bv_expr(expr.type(), result);
-
+  const exprt result = make_free_bv_expr(expr.type());
   // constraint: result<=bound
 
   set_to_true(binary_relation_exprt(result, ID_le, bound));
diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index 12571a7c01d..a61e50a0f33 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -631,54 +631,33 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr)
 
 void boolbvt::set_to(const exprt &expr, bool value)
 {
-  if(expr.type().id()!=ID_bool)
-  {
-    error() << "boolbvt::set_to got non-boolean operand: "
-            << expr.pretty() << eom;
-    throw 0;
-  }
+  PRECONDITION(expr.type().id() == ID_bool);
 
-  if(value)
-  {
-    if(expr.id()==ID_equal)
-    {
-      if(!boolbv_set_equality_to_true(to_equal_expr(expr)))
-        return;
-    }
-  }
-
-  return SUB::set_to(expr, value);
+  const auto equal_expr = expr_try_dynamic_cast<equal_exprt>(expr);
+  if(value && equal_expr && !boolbv_set_equality_to_true(*equal_expr))
+    return;
+  SUB::set_to(expr, value);
 }
 
-void boolbvt::make_bv_expr(const typet &type, const bvt &bv, exprt &dest)
+exprt boolbvt::make_bv_expr(const typet &type, const bvt &bv)
 {
-  dest=exprt(ID_bv_literals, type);
+  exprt dest(ID_bv_literals, type);
   irept::subt &bv_sub=dest.add(ID_bv).get_sub();
-
   bv_sub.resize(bv.size());
 
   for(std::size_t i=0; i<bv.size(); i++)
     bv_sub[i].id(std::to_string(bv[i].get()));
+  return dest;
 }
 
-void boolbvt::make_free_bv_expr(const typet &type, exprt &dest)
+exprt boolbvt::make_free_bv_expr(const typet &type)
 {
-  std::size_t width=boolbv_width(type);
-
-  if(width==0)
-  {
-    error() << "failed to get width of " << type.pretty() << eom;
-    throw 0;
-  }
-
-  bvt bv;
-  bv.resize(width);
-
-  // make result free variables
-  Forall_literals(it, bv)
-    *it=prop.new_variable();
-
-  make_bv_expr(type, bv, dest);
+  const std::size_t width = boolbv_width(type);
+  PRECONDITION(width != 0);
+  bvt bv(width);
+  for(auto &lit : bv)
+    lit = prop.new_variable();
+  return make_bv_expr(type, bv);
 }
 
 bool boolbvt::is_unbounded_array(const typet &type) const
@@ -708,12 +687,8 @@ bool boolbvt::is_unbounded_array(const typet &type) const
 void boolbvt::print_assignment(std::ostream &out) const
 {
   arrayst::print_assignment(out);
-
-  for(const auto &it : map.mapping)
-  {
-    out << it.first << "="
-        << it.second.get_value(prop) << '\n';
-  }
+  for(const auto &pair : map.mapping)
+    out << pair.first << "=" << pair.second.get_value(prop) << '\n';
 }
 
 void boolbvt::build_offset_map(const struct_typet &src, offset_mapt &dest)
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
index 08a39d05c80..f6e85baf83d 100644
--- a/src/solvers/flattening/boolbv.h
+++ b/src/solvers/flattening/boolbv.h
@@ -99,7 +99,7 @@ class boolbvt:public arrayst
   boolbv_mapt map;
 
   // overloading
-  virtual literalt convert_rest(const exprt &expr) override;
+  literalt convert_rest(const exprt &expr) override;
   virtual bool boolbv_set_equality_to_true(const equal_exprt &expr);
 
   // NOLINTNEXTLINE(readability/identifiers)
@@ -176,8 +176,8 @@ class boolbvt:public arrayst
   virtual bvt convert_function_application(
     const function_application_exprt &expr);
 
-  virtual void make_bv_expr(const typet &type, const bvt &bv, exprt &dest);
-  virtual void make_free_bv_expr(const typet &type, exprt &dest);
+  virtual exprt make_bv_expr(const typet &type, const bvt &bv);
+  virtual exprt make_free_bv_expr(const typet &type);
 
   void convert_with(
     const typet &type,
diff --git a/src/solvers/prop/prop.h b/src/solvers/prop/prop.h
index 7ac5d88848e..cef918c0459 100644
--- a/src/solvers/prop/prop.h
+++ b/src/solvers/prop/prop.h
@@ -87,7 +87,7 @@ class propt:public messaget, public prop_assignmentt
 
   // variables
   virtual literalt new_variable()=0;
-  virtual void set_variable_name(literalt a, const std::string &name) { }
+  virtual void set_variable_name(literalt a, const irep_idt &name) { }
   virtual size_t no_variables() const=0;
   bvt new_variables(std::size_t width);
 
diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp
index 1469b25e040..0e929871f53 100644
--- a/src/solvers/prop/prop_conv.cpp
+++ b/src/solvers/prop/prop_conv.cpp
@@ -7,40 +7,30 @@ Author: Daniel Kroening, kroening@kroening.com
 \*******************************************************************/
 
 #include "prop_conv.h"
-
-#include <cassert>
-#include <cstdlib>
-#include <map>
-
-#include <util/std_expr.h>
-#include <util/symbol.h>
-#include <util/threeval.h>
-
-#include "prop.h"
-#include "literal_expr.h"
+#include <algorithm>
 
 /// determine whether a variable is in the final conflict
 bool prop_convt::is_in_conflict(literalt l) const
 {
-  assert(false);
+  UNREACHABLE;
   return false;
 }
 
 void prop_convt::set_assumptions(const bvt &)
 {
-  assert(false);
+  UNREACHABLE;
 }
 
 void prop_convt::set_frozen(const literalt)
 {
-  assert(false);
+  UNREACHABLE;
 }
 
 void prop_convt::set_frozen(const bvt &bv)
 {
-  for(unsigned i=0; i<bv.size(); i++)
-    if(!bv[i].is_constant())
-      set_frozen(bv[i]);
+  for(const auto &bit : bv)
+    if(!bit.is_constant())
+      set_frozen(bit);
 }
 
 bool prop_conv_solvert::literal(const exprt &expr, literalt &dest) const
@@ -65,17 +55,14 @@ bool prop_conv_solvert::literal(const exprt &expr, literalt &dest) const
 
 literalt prop_conv_solvert::get_literal(const irep_idt &identifier)
 {
-  std::pair<symbolst::iterator, bool> result=
+  auto result =
     symbols.insert(std::pair<irep_idt, literalt>(identifier, literalt()));
 
   if(!result.second)
     return result.first->second;
 
-  // produce new variable
   literalt literal=prop.new_variable();
-
-  // set the name of the new variable
-  prop.set_variable_name(literal, id2string(identifier));
+  prop.set_variable_name(literal, identifier);
 
   // insert
   result.first->second=literal;
@@ -183,10 +170,9 @@ literalt prop_conv_solvert::convert(const exprt &expr)
       prop.set_frozen(literal);
     return literal;
   }
-  // check cache first
 
-  std::pair<cachet::iterator, bool> result=
-    cache.insert(std::pair<exprt, literalt>(expr, literalt()));
+  // check cache first
+  auto result = cache.insert({expr, literalt()});
 
   if(!result.second)
     return result.first->second;
@@ -208,13 +194,7 @@ literalt prop_conv_solvert::convert(const exprt &expr)
 
 literalt prop_conv_solvert::convert_bool(const exprt &expr)
 {
-  if(expr.type().id()!=ID_bool)
-  {
-    std::string msg="prop_convt::convert_bool got "
-                    "non-boolean expression: ";
-    msg+=expr.pretty();
-    throw msg;
-  }
+  PRECONDITION(expr.type().id() == ID_bool);
 
   const exprt::operandst &op=expr.operands();
 
@@ -280,8 +260,9 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
   else if(expr.id()==ID_or || expr.id()==ID_and || expr.id()==ID_xor ||
           expr.id()==ID_nor || expr.id()==ID_nand)
   {
-    if(op.empty())
-      throw "operator `"+expr.id_string()+"' takes at least one operand";
+    INVARIANT(
+      !op.empty(),
+      "operator `" + expr.id_string() + "' takes at least one operand");
 
     bvt bv;
 
@@ -304,16 +285,12 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
   }
   else if(expr.id()==ID_not)
   {
-    if(op.size()!=1)
-      throw "not takes one operand";
-
+    INVARIANT(op.size() == 1, "not takes one operand");
     return !convert(op.front());
   }
   else if(expr.id()==ID_equal || expr.id()==ID_notequal)
   {
-    if(op.size()!=2)
-      throw "equality takes two operands";
-
+    INVARIANT(op.size() == 2, "equality takes two operands");
     bool equal=(expr.id()==ID_equal);
 
     if(op[0].type().id()==ID_bool &&
@@ -387,24 +364,14 @@ bool prop_conv_solvert::set_equality_to_true(const equal_exprt &expr)
 
 void prop_conv_solvert::set_to(const exprt &expr, bool value)
 {
-  if(expr.type().id()!=ID_bool)
-  {
-    std::string msg="prop_convt::set_to got "
-                    "non-boolean expression: ";
-    msg+=expr.pretty();
-    throw msg;
-  }
+  PRECONDITION(expr.type().id() == ID_bool);
 
-  bool boolean=true;
-
-  forall_operands(it, expr)
-    if(it->type().id()!=ID_bool)
-    {
-      boolean=false;
-      break;
-    }
+  const bool has_only_boolean_operands = std::all_of(
+    expr.operands().begin(),
+    expr.operands().end(),
+    [](const exprt &expr) { return expr.type().id() == ID_bool; });
 
-  if(boolean)
+  if(has_only_boolean_operands)
   {
     if(expr.id()==ID_not)
     {
@@ -507,16 +474,12 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve()
 
   statistics() << "Solving with " << prop.solver_text() << eom;
 
-  propt::resultt result=prop.prop_solve();
-
-  switch(result)
+  switch(prop.prop_solve())
   {
     case propt::resultt::P_SATISFIABLE: return resultt::D_SATISFIABLE;
     case propt::resultt::P_UNSATISFIABLE: return resultt::D_UNSATISFIABLE;
     default: return resultt::D_ERROR;
   }
-
-  return resultt::D_ERROR;
 }
 
 exprt prop_conv_solvert::get(const exprt &expr) const
@@ -534,19 +497,17 @@ exprt prop_conv_solvert::get(const exprt &expr) const
     }
   }
 
-  exprt tmp=expr;
-
-  Forall_operands(it, tmp)
+  exprt tmp = expr;
+  for(auto &op : tmp.operands())
   {
-    exprt tmp_op=get(*it);
-    it->swap(tmp_op);
+    exprt tmp_op = get(op);
+    op.swap(tmp_op);
   }
-
   return tmp;
 }
 
 void prop_conv_solvert::print_assignment(std::ostream &out) const
 {
-  for(const auto &it : symbols)
-    out << it.first << " = " << prop.l_get(it.second) << "\n";
+  for(const auto &symbol : symbols)
+    out << symbol.first << " = " << prop.l_get(symbol.second) << '\n';
 }
diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/prop_conv.h
index 816b7481a0e..261771040a6 100644
--- a/src/solvers/prop/prop_conv.h
+++ b/src/solvers/prop/prop_conv.h
@@ -72,43 +72,45 @@ class prop_conv_solvert:public prop_convt
 public:
   prop_conv_solvert(const namespacet &_ns, propt &_prop):
     prop_convt(_ns),
-    use_cache(true),
-    equality_propagation(true),
-    freeze_all(false),
-    post_processing_done(false),
     prop(_prop) { }
 
-  virtual ~prop_conv_solvert() { }
+  virtual ~prop_conv_solvert() = default;
 
   // overloading from decision_proceduret
-  virtual void set_to(const exprt &expr, bool value) override;
-  virtual decision_proceduret::resultt dec_solve() override;
-  virtual void print_assignment(std::ostream &out) const override;
-  virtual std::string decision_procedure_text() const override
+  void set_to(const exprt &expr, bool value) override;
+  decision_proceduret::resultt dec_solve() override;
+  void print_assignment(std::ostream &out) const override;
+  std::string decision_procedure_text() const override
   { return "propositional reduction"; }
-  virtual exprt get(const exprt &expr) const override;
+  exprt get(const exprt &expr) const override;
 
   // overloading from prop_convt
   using prop_convt::set_frozen;
   virtual tvt l_get(literalt a) const override { return prop.l_get(a); }
-  virtual void set_frozen(literalt a) override { prop.set_frozen(a); }
-  virtual void set_assumptions(const bvt &_assumptions) override
+  void set_frozen(literalt a) override
+  {
+    prop.set_frozen(a);
+  }
+  void set_assumptions(const bvt &_assumptions) override
   { prop.set_assumptions(_assumptions); }
-  virtual bool has_set_assumptions() const override
+  bool has_set_assumptions() const override
   { return prop.has_set_assumptions(); }
-  virtual void set_all_frozen() override { freeze_all = true; }
-  virtual literalt convert(const exprt &expr) override;
-  virtual bool is_in_conflict(literalt l) const override
+  void set_all_frozen() override
+  {
+    freeze_all = true;
+  }
+  literalt convert(const exprt &expr) override;
+  bool is_in_conflict(literalt l) const override
   { return prop.is_in_conflict(l); }
-  virtual bool has_is_in_conflict() const override
+  bool has_is_in_conflict() const override
   { return prop.has_is_in_conflict(); }
 
   // get literal for expression, if available
   virtual bool literal(const exprt &expr, literalt &literal) const;
 
-  bool use_cache;
-  bool equality_propagation;
-  bool freeze_all; // freezing variables (for incremental solving)
+  bool use_cache = true;
+  bool equality_propagation = true;
+  bool freeze_all = false; // freezing variables (for incremental solving)
 
   virtual void clear_cache() { cache.clear();}
 
@@ -126,7 +128,7 @@ class prop_conv_solvert:public prop_convt
 protected:
   virtual void post_process();
 
-  bool post_processing_done;
+  bool post_processing_done = false;
 
   // get a _boolean_ value from counterexample if not valid
   virtual bool get_bool(const exprt &expr, tvt &value) const;