diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index 939717f76..71f1c9303 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/src/hw_cbmc_irep_ids.h
@@ -17,6 +17,7 @@ IREP_ID_ONE(F)
 IREP_ID_ONE(E)
 IREP_ID_ONE(G)
 IREP_ID_ONE(X)
+IREP_ID_ONE(smv_next)
 IREP_ID_ONE(smv_iff)
 IREP_ID_TWO(C_smv_iff, "#smv_iff")
 IREP_ID_ONE(smv_setin)
diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index e595c2706..1e25bd731 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -377,10 +377,10 @@ assignment : assignment_head '(' assignment_var ')' BECOMES_Token formula ';'
            {
              binary($$, $3, ID_equal, $6, bool_typet{});
 
-             if(stack_expr($1).id()=="next")
+             if(stack_expr($1).id()==ID_smv_next)
              {
                exprt &op=to_binary_expr(stack_expr($$)).op0();
-               unary_exprt tmp("smv_next", std::move(op));
+               unary_exprt tmp(ID_smv_next, std::move(op));
                tmp.swap(op);
                PARSER.module->add_trans(stack_expr($$));
              }
@@ -393,7 +393,7 @@ assignment_var: variable_name
            ;
 
 assignment_head: init_Token { init($$, ID_init); }
-               | NEXT_Token { init($$, "next"); }
+               | NEXT_Token { init($$, ID_smv_next); }
                ;
 
 defines:     define
@@ -439,7 +439,7 @@ formula    : term
            ;
 
 term       : variable_name
-           | NEXT_Token '(' term ')'  { init($$, "smv_next"); mto($$, $3); }
+           | NEXT_Token '(' term ')'  { init($$, ID_smv_next); mto($$, $3); }
            | '(' formula ')'          { $$=$2; }
            | '{' formula_list '}'     { $$=$2; stack_expr($$).id("smv_nondet_choice"); }
            | INC_Token '(' term ')'   { init($$, "inc"); mto($$, $3); }
diff --git a/src/smvlang/smv_range.h b/src/smvlang/smv_range.h
new file mode 100644
index 000000000..4fec77720
--- /dev/null
+++ b/src/smvlang/smv_range.h
@@ -0,0 +1,89 @@
+/*******************************************************************\
+
+Module: SMV Typechecking
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_SMV_RANGE_H
+#define CPROVER_SMV_RANGE_H
+
+#include <util/arith_tools.h>
+
+class smv_ranget
+{
+public:
+  smv_ranget() : from(0), to(0)
+  {
+  }
+
+  smv_ranget(mp_integer _from, mp_integer _to)
+    : from(std::move(_from)), to(std::move(_to))
+  {
+    PRECONDITION(_from <= _to);
+  }
+
+  mp_integer from, to;
+
+  bool is_contained_in(const smv_ranget &other) const
+  {
+    if(other.from > from)
+      return false;
+    if(other.to < to)
+      return false;
+    return true;
+  }
+
+  void make_union(const smv_ranget &other)
+  {
+    mp_min(from, other.from);
+    mp_max(to, other.to);
+  }
+
+  void to_type(typet &dest) const
+  {
+    dest = typet(ID_range);
+    dest.set(ID_from, integer2string(from));
+    dest.set(ID_to, integer2string(to));
+  }
+
+  bool is_bool() const
+  {
+    return from == 0 && to == 1;
+  }
+
+  bool is_singleton() const
+  {
+    return from == to;
+  }
+
+  smv_ranget &operator+(const smv_ranget &other)
+  {
+    from += other.from;
+    to += other.to;
+    return *this;
+  }
+
+  smv_ranget &operator-(const smv_ranget &other)
+  {
+    from -= other.from;
+    to -= other.to;
+    return *this;
+  }
+
+  smv_ranget &operator*(const smv_ranget &other)
+  {
+    mp_integer p1 = from * other.from;
+    mp_integer p2 = from * other.to;
+    mp_integer p3 = to * other.from;
+    mp_integer p4 = to * other.to;
+
+    from = std::min(p1, std::min(p2, std::min(p3, p4)));
+    to = std::max(p1, std::max(p2, std::max(p3, p4)));
+
+    return *this;
+  }
+};
+
+#endif // CPROVER_SMV_RANGE_H
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index d888a1351..6549716f3 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/typecheck.h>
 
 #include "expr2smv.h"
+#include "smv_range.h"
 
 #include <algorithm>
 #include <cassert>
@@ -39,7 +40,9 @@ class smv_typecheckt:public typecheckt
     nondet_count=0;
   }
 
-  virtual ~smv_typecheckt() { }
+  ~smv_typecheckt() override
+  {
+  }
 
   typedef enum
   {
@@ -50,25 +53,24 @@ class smv_typecheckt:public typecheckt
     CTL
   } modet;
 
-  void convert(smv_parse_treet::modulet &smv_module);
-  void convert(smv_parse_treet::mc_varst &vars);
+  void convert(smv_parse_treet::modulet &);
+  void convert(smv_parse_treet::mc_varst &);
 
-  void collect_define(const exprt &expr);
+  void collect_define(const exprt &);
   void convert_defines(exprt::operandst &invar);
   void convert_define(const irep_idt &identifier);
 
   typedef enum { NORMAL, NEXT } expr_modet;
-  virtual void convert(exprt &exprt, expr_modet expr_mode);
+  void convert(exprt &, expr_modet);
 
-  virtual void typecheck(exprt &exprt, const typet &type, modet mode);
-  virtual void typecheck_op(exprt &exprt, const typet &type, modet mode);
+  void typecheck(exprt &, const typet &, modet);
+  void typecheck_op(exprt &, const typet &, modet);
 
-  virtual void typecheck();
+  void typecheck() override;
 
-  // overload to use SMV syntax
-  
-  virtual std::string to_string(const typet &type);
-  virtual std::string to_string(const exprt &expr);
+  // These output SMV syntax
+  std::string to_string(const typet &);
+  std::string to_string(const exprt &);
 
 protected:
   smv_parse_treet &smv_parse_tree;
@@ -76,82 +78,17 @@ class smv_typecheckt:public typecheckt
   const std::string &module;
   bool do_spec;
 
-  class smv_ranget
-  {
-  public:
-    smv_ranget():from(0), to(0)
-    {
-    }
-  
-    mp_integer from, to;
-    
-    bool is_contained_in(const smv_ranget &other) const
-    {
-      if(other.from>from) return false;
-      if(other.to<to) return false;
-      return true;
-    }
-    
-    void make_union(const smv_ranget &other)
-    {
-      mp_min(from, other.from);
-      mp_max(to, other.to);
-    }
-    
-    void to_type(typet &dest) const
-    {
-      dest=typet(ID_range);
-      dest.set(ID_from, integer2string(from));
-      dest.set(ID_to, integer2string(to));
-    }
-    
-    bool is_bool() const
-    {
-      return from==0 && to==1;
-    }
-    
-    bool is_singleton() const
-    {
-      return from==to;
-    }
-    
-    smv_ranget &operator+(const smv_ranget &other)
-    {
-      from+=other.from;
-      to+=other.to;
-      return *this;
-    }
-
-    smv_ranget &operator-(const smv_ranget &other)
-    {
-      from-=other.from;
-      to-=other.to;
-      return *this;
-    }
-
-    smv_ranget &operator*(const smv_ranget &other)
-    {
-      mp_integer p1=from*other.from;
-      mp_integer p2=from*other.to;
-      mp_integer p3=to*other.from;
-      mp_integer p4=to*other.to;
-
-      from=std::min(p1, std::min(p2, std::min(p3, p4)));
-      to=std::max(p1, std::max(p2, std::max(p3, p4)));
-      
-      return *this;
-    }
-  };
-  
-  smv_ranget convert_type(const typet &type);
-  void convert(smv_parse_treet::modulet::itemt &item);
-  void typecheck(smv_parse_treet::modulet::itemt &item);
+  smv_ranget convert_type(const typet &);
+  void convert(smv_parse_treet::modulet::itemt &);
+  void typecheck(smv_parse_treet::modulet::itemt &);
+  void typecheck_expr_rec(exprt &, const typet &, modet);
+  void convert_expr_to(exprt &, const typet &dest);
 
   smv_parse_treet::modulet *modulep;
 
   unsigned nondet_count;
 
-  void flatten_hierarchy(smv_parse_treet::modulet &module);
+  void flatten_hierarchy(smv_parse_treet::modulet &);
 
   void instantiate(
     smv_parse_treet::modulet &,
@@ -166,11 +103,9 @@ class smv_typecheckt:public typecheckt
 
   typedef std::map<irep_idt, exprt> rename_mapt;
 
-  void instantiate_rename(exprt &expr,
-                          const rename_mapt &rename_map);
+  void instantiate_rename(exprt &, const rename_mapt &rename_map);
 
-  void convert_ports(smv_parse_treet::modulet &smv_module,
-                     typet &dest);
+  void convert_ports(smv_parse_treet::modulet &, typet &dest);
 
   // for defines
   class definet
@@ -220,14 +155,12 @@ void smv_typecheckt::convert_ports(
 
   ports.reserve(smv_module.ports.size());
 
-  for(std::list<irep_idt>::const_iterator
-      it=smv_module.ports.begin();
-      it!=smv_module.ports.end();
-      it++)
+  for(const auto &port_name : smv_module.ports)
   {
     ports.push_back(exprt(ID_symbol));
-    ports.back().set(ID_identifier,
-      id2string(smv_module.name)+"::var::"+id2string(*it));
+    ports.back().set(
+      ID_identifier,
+      id2string(smv_module.name) + "::var::" + id2string(port_name));
   }
 }
 
@@ -245,25 +178,23 @@ Function: smv_typecheckt::flatten_hierarchy
 
 void smv_typecheckt::flatten_hierarchy(smv_parse_treet::modulet &smv_module)
 {
-  for(smv_parse_treet::mc_varst::iterator
-      it=smv_module.vars.begin();
-      it!=smv_module.vars.end();
-      it++)
+  for(auto &var_it : smv_module.vars)
   {
-    smv_parse_treet::mc_vart &var=it->second;
+    smv_parse_treet::mc_vart &var = var_it.second;
 
     if(var.type.id()=="submodule")
     {
       exprt &inst=static_cast<exprt &>(static_cast<irept &>(var.type));
 
-      Forall_operands(o_it, inst)
-        convert(*o_it, NORMAL);
+      for(auto &op : inst.operands())
+        convert(op, NORMAL);
 
-      instantiate(smv_module,
-                  inst.get(ID_identifier),
-                  it->first,
-                  inst.operands(),
-                  inst.find_source_location());
+      instantiate(
+        smv_module,
+        inst.get(ID_identifier),
+        var_it.first,
+        inst.operands(),
+        inst.find_source_location());
     }
   }
 }
@@ -292,20 +223,14 @@ void smv_typecheckt::instantiate(
 
   if(s_it==symbol_table.symbols.end())
   {
-    error().source_location=location;
-    error() << "submodule `"
-            << identifier
-            << "' not found" << eom;
-    throw 0;
+    throw errort().with_location(location)
+      << "submodule `" << identifier << "' not found";
   }
 
   if(s_it->second.type.id()!=ID_module)
   {
-    error().source_location=location;
-    error() << "submodule `"
-            << identifier
-            << "' not a module" << eom;
-    throw 0;
+    throw errort().with_location(location)
+      << "submodule `" << identifier << "' not a module";
   }
 
   const irept::subt &ports=s_it->second.type.find(ID_ports).get_sub();
@@ -314,16 +239,14 @@ void smv_typecheckt::instantiate(
 
   if(ports.size()!=operands.size())
   {
-    error().source_location=location;
-    error() << "submodule `" << identifier
-            << "' has wrong number of arguments" << eom;
-    throw 0;
+    throw errort().with_location(location)
+      << "submodule `" << identifier << "' has wrong number of arguments";
   }
 
   std::set<irep_idt> port_identifiers;
   rename_mapt rename_map;
 
-  for(unsigned i=0; i<ports.size(); i++)
+  for(std::size_t i = 0; i < ports.size(); i++)
   {
     const irep_idt &identifier=ports[i].get(ID_identifier);
     rename_map.insert(std::pair<irep_idt, exprt>(identifier, operands[i]));
@@ -346,12 +269,14 @@ void smv_typecheckt::instantiate(
 
     if(s_it2==symbol_table.symbols.end())
     {
-      error() << "symbol `" << v_it->second << "' not found" << eom;
-      throw 0;
+      throw errort() << "symbol `" << v_it->second << "' not found";
     }
 
-    if (port_identifiers.find(s_it2->first) != port_identifiers.end()) {
-    } else if (s_it2->second.type.id() == ID_module) {
+    if(port_identifiers.find(s_it2->first) != port_identifiers.end())
+    {
+    }
+    else if(s_it2->second.type.id() == ID_module)
+    {
     }
     else
     {
@@ -381,18 +306,13 @@ void smv_typecheckt::instantiate(
 
   // fix values (macros)
 
-  for(std::set<irep_idt>::const_iterator
-      v_it=var_identifiers.begin();
-      v_it!=var_identifiers.end();
-      v_it++)
+  for(const auto &v_id : var_identifiers)
   {
-    auto s_it2=
-      symbol_table.get_writeable(*v_it);
+    auto s_it2 = symbol_table.get_writeable(v_id);
 
     if(s_it2==nullptr)
     {
-      error() << "symbol `" << *v_it << "' not found" << eom;
-      throw 0;
+      throw errort() << "symbol `" << v_id << "' not found";
     }
 
     symbolt &symbol=*s_it2;
@@ -451,8 +371,8 @@ void smv_typecheckt::instantiate_rename(
   exprt &expr,
   const rename_mapt &rename_map)
 {
-  Forall_operands(it, expr)
-    instantiate_rename(*it, rename_map);
+  for(auto &op : expr.operands())
+    instantiate_rename(op, rename_map);
 
   if(expr.id()==ID_symbol || expr.id()==ID_next_symbol)
   {
@@ -475,10 +395,9 @@ void smv_typecheckt::instantiate_rename(
         }
         else
         {
-          error().source_location=expr.find_source_location();
-          error() << "expected symbol expression here, but got "
-                  << to_string(it->second) << eom;
-          throw 0;
+          throw errort().with_location(expr.find_source_location())
+            << "expected symbol expression here, but got "
+            << to_string(it->second);
         }
       }
       else
@@ -506,14 +425,12 @@ void smv_typecheckt::typecheck_op(
 {
   if(expr.operands().size()==0)
   {
-    error().source_location=expr.find_source_location();
-    error() << "Expected operands for " << expr.id()
-            << " operator" << eom;
-    throw 0;
+    throw errort().with_location(expr.find_source_location())
+      << "Expected operands for " << expr.id() << " operator";
   }
 
-  Forall_operands(it, expr)
-    typecheck(*it, type, mode);
+  for(auto &op : expr.operands())
+    typecheck_expr_rec(op, type, mode);
 
   expr.type()=type;
 
@@ -523,10 +440,10 @@ void smv_typecheckt::typecheck_op(
   {
     // figure out types
 
-    forall_operands(it, expr)
-      if(!it->type().is_nil())
+    for(const auto &op : expr.operands())
+      if(!op.type().is_nil())
       {
-        expr.type()=it->type();
+        expr.type() = op.type();
         break;
       }
   }
@@ -544,7 +461,7 @@ Function: smv_typecheckt::convert_type
 
 \*******************************************************************/
 
-smv_typecheckt::smv_ranget smv_typecheckt::convert_type(const typet &src)
+smv_ranget smv_typecheckt::convert_type(const typet &src)
 {
   smv_ranget dest;
   
@@ -572,9 +489,8 @@ smv_typecheckt::smv_ranget smv_typecheckt::convert_type(const typet &src)
   }
   else
   {
-    error().source_location=src.source_location();
-    error() << "Unexpected type: `" << to_string(src) << "'" << eom;
-    throw 0;
+    throw errort().with_location(src.source_location())
+      << "Unexpected type: `" << to_string(src) << "'";
   }
   
   return dest;
@@ -648,6 +564,26 @@ void smv_typecheckt::typecheck(
   exprt &expr,
   const typet &type,
   modet mode)
+{
+  typecheck_expr_rec(expr, type, mode);
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::typecheck_expr_rec
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::typecheck_expr_rec(
+  exprt &expr,
+  const typet &dest_type,
+  modet mode)
 {
   const auto static nil_type = static_cast<const typet &>(get_nil_irep());
 
@@ -664,9 +600,8 @@ void smv_typecheckt::typecheck(
 
     if(s_it==nullptr)
     {
-      error().source_location=expr.find_source_location();
-      error() << "variable `" << identifier << "' not found" << eom;
-      throw 0;
+      throw errort().with_location(expr.find_source_location())
+        << "variable `" << identifier << "' not found";
     }
 
     symbolt &symbol=*s_it;
@@ -697,34 +632,33 @@ void smv_typecheckt::typecheck(
   }
   else if(expr.id()==ID_nondet_symbol)
   {
-    if(!type.is_nil())
-      expr.type()=type;
+    if(!dest_type.is_nil())
+      expr.type() = dest_type;
   }
   else if(expr.id()==ID_constraint_select_one)
   {
-    typecheck_op(expr, type, mode);
+    typecheck_op(expr, dest_type, mode);
 
     typet op_type;
     op_type.make_nil();
 
-    forall_operands(it, expr)
+    for(const auto &op : expr.operands())
     {
-      typet tmp=type_union(it->type(), op_type);
+      typet tmp = type_union(op.type(), op_type);
       op_type=tmp;
     }
-    
-    Forall_operands(it, expr)
-      typecheck(*it, op_type, mode);
-      
+
+    for(auto &op : expr.operands())
+      typecheck_expr_rec(op, op_type, mode);
+
     expr.type()=op_type;
   }
   else if(expr.id()==ID_implies)
   {
     if(expr.operands().size()!=2)
     {
-      error().source_location=expr.find_source_location();
-      error() << "Expected two operands for -> operator" << eom;
-      throw 0;
+      throw errort().with_location(expr.find_source_location())
+        << "Expected two operands for -> operator";
     }
 
     typecheck_op(expr, bool_typet(), mode);
@@ -733,14 +667,13 @@ void smv_typecheckt::typecheck(
           expr.id()==ID_lt || expr.id()==ID_le ||
           expr.id()==ID_gt || expr.id()==ID_ge)
   {
-    Forall_operands(it, expr)
-      typecheck(*it, static_cast<const typet &>(get_nil_irep()), mode);
+    for(auto &op : expr.operands())
+      typecheck_expr_rec(op, static_cast<const typet &>(get_nil_irep()), mode);
 
     if(expr.operands().size()!=2)
     {
-      error().source_location=expr.find_source_location();
-      error() << "Expected two operands for " << expr.id() << eom;
-      throw 0;
+      throw errort().with_location(expr.find_source_location())
+        << "Expected two operands for " << expr.id();
     }
 
     expr.type()=bool_typet();
@@ -748,9 +681,9 @@ void smv_typecheckt::typecheck(
     exprt &op0 = to_binary_expr(expr).op0(), &op1 = to_binary_expr(expr).op1();
 
     typet op_type=type_union(op0.type(), op1.type());
-    
-    typecheck(op0, op_type, mode);
-    typecheck(op1, op_type, mode);
+
+    typecheck_expr_rec(op0, op_type, mode);
+    typecheck_expr_rec(op1, op_type, mode);
 
     INVARIANT(op0.type() == op1.type(), "type of operands of relational operators");
 
@@ -759,9 +692,8 @@ void smv_typecheckt::typecheck(
     {
       if(op0.type().id()!=ID_range)
       {
-        error().source_location=expr.find_source_location();
-        error() << "Expected number type for " << to_string(expr) << eom;
-        throw 0;
+        throw errort().with_location(expr.find_source_location())
+          << "Expected number type for " << to_string(expr);
       }
     }
   }
@@ -770,25 +702,24 @@ void smv_typecheckt::typecheck(
     auto &if_expr = to_if_expr(expr);
     auto &true_case = if_expr.true_case();
     auto &false_case = if_expr.false_case();
-    typecheck(if_expr.cond(), bool_typet{}, mode);
-    typecheck(true_case, type, mode);
-    typecheck(false_case, type, mode);
-    expr.type() = type;
+    typecheck_expr_rec(if_expr.cond(), bool_typet{}, mode);
+    typecheck_expr_rec(true_case, dest_type, mode);
+    typecheck_expr_rec(false_case, dest_type, mode);
+    expr.type() = dest_type;
   }
   else if(expr.id()==ID_plus || expr.id()==ID_minus ||
           expr.id()==ID_mult || expr.id()==ID_div ||
           expr.id()==ID_mod)
   {
-    typecheck_op(expr, type, mode);
-    
+    typecheck_op(expr, dest_type, mode);
+
     if(expr.operands().size()!=2)
     {
-      error().source_location=expr.find_source_location();
-      error() << "Expected two operands for " << expr.id() << eom;
-      throw 0;
+      throw errort().with_location(expr.find_source_location())
+        << "Expected two operands for " << expr.id();
     }
-    
-    if(type.is_nil())
+
+    if(dest_type.is_nil())
     {
       if(expr.type().id()==ID_range ||
          expr.type().id()==ID_bool)
@@ -815,11 +746,10 @@ void smv_typecheckt::typecheck(
         new_range.to_type(expr.type());
       }
     }
-    else if(type.id()!=ID_range)
+    else if(dest_type.id() != ID_range)
     {
-      error().source_location=expr.find_source_location();
-      error() << "Expected number type for " << to_string(expr) << eom;
-      throw 0;
+      throw errort().with_location(expr.find_source_location())
+        << "Expected number type for " << to_string(expr);
     }
   }
   else if(expr.id()==ID_constant)
@@ -829,7 +759,7 @@ void smv_typecheckt::typecheck(
       const std::string &value=expr.get_string(ID_value);
       mp_integer int_value=string2integer(value);
 
-      if(type.is_nil())
+      if(dest_type.is_nil())
       {
         expr.type()=typet(ID_range);
         expr.type().set(ID_from, integer2string(int_value));
@@ -837,9 +767,9 @@ void smv_typecheckt::typecheck(
       }
       else
       {
-        expr.type()=type;
+        expr.type() = dest_type;
 
-        if(type.id()==ID_bool)
+        if(dest_type.id() == ID_bool)
         {
           if(int_value==0)
             expr=false_exprt();
@@ -847,40 +777,37 @@ void smv_typecheckt::typecheck(
             expr=true_exprt();
           else
           {
-            error().source_location=expr.find_source_location();
-            error() << "expected 0 or 1 here, but got " << value << eom;
-            throw 0;
+            throw errort().with_location(expr.find_source_location())
+              << "expected 0 or 1 here, but got " << value;
           }
         }
-        else if(type.id()==ID_range)
+        else if(dest_type.id() == ID_range)
         {
-          smv_ranget smv_range=convert_type(type);
+          smv_ranget smv_range = convert_type(dest_type);
 
           if(int_value<smv_range.from || int_value>smv_range.to)
           {
-            error().source_location=expr.find_source_location();
-            error() << "expected " << smv_range.from << ".." << smv_range.to 
-                    << " here, but got " << value << eom;
-            throw 0;
+            throw errort().with_location(expr.find_source_location())
+              << "expected " << smv_range.from << ".." << smv_range.to
+              << " here, but got " << value;
           }
         }
         else
         {
-          error().source_location=expr.find_source_location();
-          error() << "Unexpected constant: " << value << eom;
-          throw 0;
+          throw errort().with_location(expr.find_source_location())
+            << "Unexpected constant: " << value;
         }
       }
     }
     else if(expr.type().id()==ID_enumeration)
     {
-      if(type.id()==ID_enumeration)
+      if(dest_type.id() == ID_enumeration)
       {
         if(to_enumeration_type(expr.type()).elements().empty())
-          expr.type()=type;
+          expr.type() = dest_type;
       }
     }
-    else if(type.is_not_nil() && type!=expr.type())
+    else if(dest_type.is_not_nil() && dest_type != expr.type())
     {
       // already done, but maybe need to change the type
       mp_integer int_value;
@@ -899,21 +826,21 @@ void smv_typecheckt::typecheck(
 
       if(have_int_value)
       {
-        if(type.id()==ID_bool)
+        if(dest_type.id() == ID_bool)
         {
           if(int_value==0)
             expr=false_exprt();
           else if(int_value==1)
             expr=true_exprt();
         }
-        else if(type.id()==ID_range)
+        else if(dest_type.id() == ID_range)
         {
-          mp_integer from=string2integer(type.get_string(ID_from)),
-                     to=string2integer(type.get_string(ID_to));
+          mp_integer from = string2integer(dest_type.get_string(ID_from)),
+                     to = string2integer(dest_type.get_string(ID_to));
 
           if(int_value>=from && int_value<=to)
           {
-            expr=exprt(ID_constant, type);
+            expr = exprt(ID_constant, dest_type);
             expr.set(ID_value, integer2string(int_value));
           }
         }
@@ -922,20 +849,21 @@ void smv_typecheckt::typecheck(
   }
   else if(expr.id()==ID_cond)
   {
-    if(type.is_nil())
+    if(dest_type.is_nil())
     {
       bool condition=true;
       
       expr.type().make_nil();
 
-      Forall_operands(it, expr)
+      for(auto &op : expr.operands())
       {
         if(condition)
-          typecheck(*it, bool_typet(), mode);
+          typecheck_expr_rec(op, bool_typet(), mode);
         else
         {
-          typecheck(*it, static_cast<const typet &>(get_nil_irep()), mode);
-          expr.type()=type_union(expr.type(), it->type());
+          typecheck_expr_rec(
+            op, static_cast<const typet &>(get_nil_irep()), mode);
+          expr.type() = type_union(expr.type(), op.type());
         }
 
         condition=!condition;
@@ -943,16 +871,16 @@ void smv_typecheckt::typecheck(
     }
     else
     {
-      expr.type()=type;
+      expr.type() = dest_type;
 
       bool condition=true;
 
-      Forall_operands(it, expr)
+      for(auto &op : expr.operands())
       {
         if(condition)
-          typecheck(*it, bool_typet(), mode);
+          typecheck_expr_rec(op, bool_typet(), mode);
         else
-          typecheck(*it, expr.type(), mode);
+          typecheck_expr_rec(op, expr.type(), mode);
 
         condition=!condition;
       }
@@ -966,7 +894,7 @@ void smv_typecheckt::typecheck(
       throw errort().with_location(expr.source_location())
         << "CTL operator not permitted here";
     expr.type() = bool_typet();
-    typecheck(to_unary_expr(expr).op(), expr.type(), mode);
+    typecheck_expr_rec(to_unary_expr(expr).op(), expr.type(), mode);
   }
   else if(expr.id() == ID_X || expr.id() == ID_F || expr.id() == ID_G)
   {
@@ -974,7 +902,7 @@ void smv_typecheckt::typecheck(
       throw errort().with_location(expr.source_location())
         << "LTL operator not permitted here";
     expr.type() = bool_typet();
-    typecheck(to_unary_expr(expr).op(), expr.type(), mode);
+    typecheck_expr_rec(to_unary_expr(expr).op(), expr.type(), mode);
   }
   else if(
     expr.id() == ID_EU || expr.id() == ID_ER || expr.id() == ID_AU ||
@@ -985,8 +913,8 @@ void smv_typecheckt::typecheck(
         << "CTL operator not permitted here";
     auto &binary_expr = to_binary_expr(expr);
     expr.type() = bool_typet();
-    typecheck(binary_expr.lhs(), expr.type(), mode);
-    typecheck(binary_expr.rhs(), expr.type(), mode);
+    typecheck_expr_rec(binary_expr.lhs(), expr.type(), mode);
+    typecheck_expr_rec(binary_expr.rhs(), expr.type(), mode);
   }
   else if(expr.id() == ID_U || expr.id() == ID_R)
   {
@@ -995,8 +923,8 @@ void smv_typecheckt::typecheck(
         << "LTL operator not permitted here";
     auto &binary_expr = to_binary_expr(expr);
     expr.type() = bool_typet();
-    typecheck(binary_expr.lhs(), expr.type(), mode);
-    typecheck(binary_expr.rhs(), expr.type(), mode);
+    typecheck_expr_rec(binary_expr.lhs(), expr.type(), mode);
+    typecheck_expr_rec(binary_expr.rhs(), expr.type(), mode);
   }
   else if(expr.id()==ID_typecast)
   {
@@ -1011,12 +939,31 @@ void smv_typecheckt::typecheck(
   }
   else
   {
-    error().source_location=expr.find_source_location();
-    error() << "No type checking for " << expr.id() << eom;
-    throw 0;
+    throw errort().with_location(expr.find_source_location())
+      << "No type checking for " << expr.id();
   }
 
-  if(!type.is_nil() && expr.type()!=type)
+  if(!dest_type.is_nil())
+    convert_expr_to(expr, dest_type);
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::convert_expr_to
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::convert_expr_to(exprt &expr, const typet &type)
+{
+  PRECONDITION(type.is_not_nil());
+
+  if(expr.type() != type)
   {
     smv_ranget e=convert_type(expr.type());
     smv_ranget t=convert_type(type);
@@ -1044,12 +991,10 @@ void smv_typecheckt::typecheck(
       return;      
     }
 
-    error().source_location=expr.find_source_location();
-    error() << "Expected expression of type `" << to_string(type)
-            << "', but got expression `" << to_string(expr)
-            << "', which is of type `" << to_string(expr.type())
-            << "'" << eom;
-    throw 0;
+    throw errort().with_location(expr.find_source_location())
+      << "Expected expression of type `" << to_string(type)
+      << "', but got expression `" << to_string(expr) << "', which is of type `"
+      << to_string(expr.type()) << "'";
   }
 }
 
@@ -1067,13 +1012,12 @@ Function: smv_typecheckt::convert
 
 void smv_typecheckt::convert(exprt &expr, expr_modet expr_mode)
 {
-  if(expr.id()=="smv_next")
+  if(expr.id() == ID_smv_next)
   {
     if(expr_mode!=NORMAL)
     {
-      error().source_location=expr.find_source_location();
-      error() << "next(next(...)) encountered" << eom;
-      throw 0;
+      throw errort().with_location(expr.find_source_location())
+        << "next(next(...)) encountered";
     }
     
     assert(expr.operands().size()==1);
@@ -1086,8 +1030,8 @@ void smv_typecheckt::convert(exprt &expr, expr_modet expr_mode)
     return;
   }
 
-  Forall_operands(it, expr)
-    convert(*it, expr_mode);
+  for(auto &op : expr.operands())
+    convert(op, expr_mode);
 
   if(expr.id()==ID_symbol)
   {
@@ -1119,9 +1063,8 @@ void smv_typecheckt::convert(exprt &expr, expr_modet expr_mode)
   {
     if(expr.operands().size()==0)
     {
-      error().source_location=expr.find_source_location();
-      error() << "expected operand here" << eom;
-      throw 0;
+      throw errort().with_location(expr.find_source_location())
+        << "expected operand here";
     }
 
     std::string identifier=
@@ -1136,26 +1079,24 @@ void smv_typecheckt::convert(exprt &expr, expr_modet expr_mode)
   {
     if(expr.operands().size()<1)
     {
-      error().source_location=expr.find_source_location();
-      error() << "Expected at least one operand for " << expr.id()
-              << " expression" << eom;
-      throw 0;
+      throw errort().with_location(expr.find_source_location())
+        << "Expected at least one operand for " << expr.id() << " expression";
     }
 
     exprt tmp;
     tmp.operands().swap(expr.operands());
     expr.reserve_operands(tmp.operands().size()*2);
 
-    Forall_operands(it, tmp)
+    for(auto &op : tmp.operands())
     {
-      if(it->operands().size()!=2)
+      if(op.operands().size() != 2)
       {
-        error().source_location=it->find_source_location();
-        throw "case expected to have two operands";
+        throw errort().with_location(op.find_source_location())
+          << "case expected to have two operands";
       }
 
-      exprt &condition = to_binary_expr(*it).op0();
-      exprt &value = to_binary_expr(*it).op1();
+      exprt &condition = to_binary_expr(op).op0();
+      exprt &value = to_binary_expr(op).op1();
 
       expr.add_to_operands(std::move(condition));
       expr.add_to_operands(std::move(value));
@@ -1287,12 +1228,11 @@ void smv_typecheckt::convert(smv_parse_treet::mc_varst &vars)
   symbol.mode="SMV";
   symbol.module=modulep->name;
 
-  for(smv_parse_treet::mc_varst::const_iterator it=vars.begin();
-      it!=vars.end(); it++)
+  for(const auto &var_it : vars)
   {
-    const smv_parse_treet::mc_vart &var=it->second;
+    const smv_parse_treet::mc_vart &var = var_it.second;
 
-    symbol.base_name=it->first;
+    symbol.base_name = var_it.first;
 
     if(var.identifier=="")
     {
@@ -1330,23 +1270,22 @@ Function: smv_typecheckt::collect_define
 void smv_typecheckt::collect_define(const exprt &expr)
 {
   if(expr.id()!=ID_equal || expr.operands().size()!=2)
-    throw "collect_define expects equality";
+    throw errort() << "collect_define expects equality";
 
   const exprt &op0 = to_equal_expr(expr).op0();
   const exprt &op1 = to_equal_expr(expr).op1();
 
   if(op0.id()!=ID_symbol)
-    throw "collect_define expects symbol on left hand side";
+    throw errort() << "collect_define expects symbol on left hand side";
 
-  const irep_idt &identifier=op0.get(ID_identifier);
+  const irep_idt &identifier = to_symbol_expr(op0).get_identifier();
 
   auto it=symbol_table.get_writeable(identifier);
 
   if(it==nullptr)
   {
-    error() << "collect_define failed to find symbol `"
-            << identifier << "'" << eom;
-    throw 0;
+    throw errort() << "collect_define failed to find symbol `" << identifier
+                   << "'";
   }
 
   symbolt &symbol=*it;
@@ -1361,9 +1300,8 @@ void smv_typecheckt::collect_define(const exprt &expr)
 
   if(!result.second)
   {
-    error().source_location=expr.find_source_location();
-    error() << "symbol `" << identifier << "' defined twice" << eom;
-    throw 0;
+    throw errort().with_location(expr.find_source_location())
+      << "symbol `" << identifier << "' defined twice";
   }  
 }
 
@@ -1387,17 +1325,15 @@ void smv_typecheckt::convert_define(const irep_idt &identifier)
   
   if(d.in_progress)
   {
-    error() << "definition of `" << identifier << "' is cyclic" << eom;
-    throw 0;
+    throw errort() << "definition of `" << identifier << "' is cyclic";
   }
   
   auto it=symbol_table.get_writeable(identifier);
 
   if(it==nullptr)
   {
-    error() << "convert_define failed to find symbol `"
-            << identifier << "'" << eom;
-    throw 0;
+    throw errort() << "convert_define failed to find symbol `" << identifier
+                   << "'";
   }
 
   symbolt &symbol=*it;
@@ -1409,6 +1345,8 @@ void smv_typecheckt::convert_define(const irep_idt &identifier)
   d.in_progress=false;
   d.typechecked=true;
 
+  // VAR x : type; ASSIGN x := ... does come with a type.
+  // DEFINE x := ... doesn't come with a type.
   if(symbol.type.is_nil())
     symbol.type=d.value.type();
 }
@@ -1427,15 +1365,14 @@ Function: smv_typecheckt::convert_defines
 
 void smv_typecheckt::convert_defines(exprt::operandst &invar)
 {
-  for(define_mapt::iterator it=define_map.begin();
-      it!=define_map.end();
-      it++)
+  for(auto &define_it : define_map)
   {
-    convert_define(it->first);
+    convert_define(define_it.first);
 
     // generate constraint
-    equal_exprt equality{symbol_exprt{it->first, it->second.value.type()},
-                         it->second.value};
+    equal_exprt equality{
+      symbol_exprt{define_it.first, define_it.second.value.type()},
+      define_it.second.value};
     invar.push_back(equality);
   }
 }
@@ -1568,8 +1505,7 @@ void smv_typecheckt::typecheck()
 
   if(it==smv_parse_tree.modules.end())
   {
-    error() << "failed to find module " << module << eom;
-    throw 0;
+    throw errort() << "failed to find module " << module;
   }
 
   convert(it->second);