diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
index d76391c6446..dedb2da9a3c 100644
--- a/src/analyses/ai.cpp
+++ b/src/analyses/ai.cpp
@@ -365,8 +365,7 @@ bool ai_baset::visit(
       // initialize state, if necessary
       get_state(to_l);
 
-      new_values.transform(
-        l, to_l, *this, ns, ai_domain_baset::edge_typet::FUNCTION_LOCAL);
+      new_values.transform(l, to_l, *this, ns);
 
       if(merge(new_values, l, to_l))
         have_new_values=true;
@@ -399,8 +398,7 @@ bool ai_baset::do_function_call(
   {
     // if we don't have a body, we just do an edige call -> return
     std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
-    tmp_state->transform(
-      l_call, l_return, *this, ns, ai_domain_baset::edge_typet::FUNCTION_LOCAL);
+    tmp_state->transform(l_call, l_return, *this, ns);
 
     return merge(*tmp_state, l_call, l_return);
   }
@@ -417,8 +415,7 @@ bool ai_baset::do_function_call(
 
     // do the edge from the call site to the beginning of the function
     std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
-    tmp_state->transform(
-      l_call, l_begin, *this, ns, ai_domain_baset::edge_typet::CALL);
+    tmp_state->transform(l_call, l_begin, *this, ns);
 
     bool new_data=false;
 
@@ -445,8 +442,7 @@ bool ai_baset::do_function_call(
       return false; // function exit point not reachable
 
     std::unique_ptr<statet> tmp_state(make_temporary_state(end_state));
-    tmp_state->transform(
-      l_end, l_return, *this, ns, ai_domain_baset::edge_typet::RETURN);
+    tmp_state->transform(l_end, l_return, *this, ns);
 
     // Propagate those
     return merge(*tmp_state, l_end, l_return);
diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index 99d1b130345..dfe5e183a3d 100644
--- a/src/analyses/ai.h
+++ b/src/analyses/ai.h
@@ -31,13 +31,6 @@ class ai_baset;
 class ai_domain_baset
 {
 public:
-  enum class edge_typet
-  {
-    FUNCTION_LOCAL,
-    CALL,
-    RETURN,
-  };
-
   // The constructor is expected to produce 'false'
   // or 'bottom'
   ai_domain_baset()
@@ -55,13 +48,21 @@ class ai_domain_baset
   // b) there is an edge from the last instruction (END_FUNCTION)
   //    of the function to the instruction _following_ the call site
   //    (this also needs to set the LHS, if applicable)
+  //
+  // "this" is the domain before the instruction "from"
+  // "from" is the instruction to be interpretted
+  // "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)
+  //
+  // PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
+  // PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
+  // PRECONDITION(are_comparable(from,to) ||
+  //              (from->is_function_call() || from->is_end_function())
 
   virtual void transform(
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns,
-    edge_typet edge_type) = 0;
+    const namespacet &ns) = 0;
 
   virtual void output(
     std::ostream &out,
@@ -98,6 +99,11 @@ class ai_domain_baset
   //
   // This computes the join between "this" and "b".
   // Return true if "this" has changed.
+  // In the usual case, "b" is the updated state after "from"
+  // and "this" is the state before "to".
+  //
+  // PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
+  // PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
 
   // This method allows an expression to be simplified / evaluated using the
   // current state.  It is used to evaluate assertions and in program
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index c4174dc8f91..fa410762bf2 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -45,8 +45,7 @@ void constant_propagator_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns,
-  ai_domain_baset::edge_typet edge_type)
+  const namespacet &ns)
 {
 #ifdef DEBUG
   std::cout << "Transform from/to:\n";
@@ -94,6 +93,8 @@ void constant_propagator_domaint::transform(
   {
     exprt g;
 
+    // Comparing iterators is safe as the target must be within the same list
+    // of instructions because this is a GOTO.
     if(from->get_target()==to)
       g=simplify_expr(from->guard, ns);
     else
@@ -122,15 +123,14 @@ void constant_propagator_domaint::transform(
     const code_function_callt &function_call=to_code_function_call(from->code);
     const exprt &function=function_call.function();
 
-    const locationt& next=std::next(from);
-
     if(function.id()==ID_symbol)
     {
       // called function identifier
       const symbol_exprt &symbol_expr=to_symbol_expr(function);
       const irep_idt id=symbol_expr.get_identifier();
 
-      if(edge_type == ai_domain_baset::edge_typet::FUNCTION_LOCAL)
+      // Functions with no body
+      if(from->function == to->function)
       {
         if(id==CPROVER_PREFIX "set_must" ||
            id==CPROVER_PREFIX "get_must" ||
@@ -178,7 +178,9 @@ void constant_propagator_domaint::transform(
     else
     {
       // unresolved call
-      INVARIANT(to==next, "Unresolved call can only be approximated if a skip");
+      INVARIANT(
+        from->function == to->function,
+        "Unresolved call can only be approximated if a skip");
 
       if(have_dirty)
         values.set_dirty_to_top(cp->dirty, ns);
diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h
index 1431783f918..0fc4796e8b7 100644
--- a/src/analyses/constant_propagator.h
+++ b/src/analyses/constant_propagator.h
@@ -25,8 +25,7 @@ class constant_propagator_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai_base,
-    const namespacet &ns,
-    ai_domain_baset::edge_typet edge_type) final override;
+    const namespacet &ns) final override;
 
   virtual void output(
     std::ostream &out,
diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp
index 0b45099302b..ae452b36002 100644
--- a/src/analyses/custom_bitvector_analysis.cpp
+++ b/src/analyses/custom_bitvector_analysis.cpp
@@ -269,8 +269,7 @@ void custom_bitvector_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns,
-  ai_domain_baset::edge_typet edge_type)
+  const namespacet &ns)
 {
   // upcast of ai
   custom_bitvector_analysist &cba=
@@ -397,7 +396,7 @@ void custom_bitvector_domaint::transform(
         else
         {
           // only if there is an actual call, i.e., we have a body
-          if(edge_type != ai_domain_baset::edge_typet::FUNCTION_LOCAL)
+          if(from->function != to->function)
           {
             const code_typet &code_type=
               to_code_type(ns.lookup(identifier).type);
@@ -520,6 +519,8 @@ void custom_bitvector_domaint::transform(
     {
       exprt guard=instruction.guard;
 
+      // Comparing iterators is safe as the target must be within the same list
+      // of instructions because this is a GOTO.
       if(to!=from->get_target())
         guard.make_not();
 
diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h
index e64a83e585c..4142d6930c1 100644
--- a/src/analyses/custom_bitvector_analysis.h
+++ b/src/analyses/custom_bitvector_analysis.h
@@ -23,12 +23,9 @@ class custom_bitvector_analysist;
 class custom_bitvector_domaint:public ai_domain_baset
 {
 public:
-  void transform(
-    locationt from,
-    locationt to,
-    ai_baset &ai,
-    const namespacet &ns,
-    ai_domain_baset::edge_typet edge_type) final override;
+  void
+  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
+    final override;
 
   void output(
     std::ostream &out,
diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp
index 6d691528ca8..f4af2913fa0 100644
--- a/src/analyses/dependence_graph.cpp
+++ b/src/analyses/dependence_graph.cpp
@@ -187,8 +187,7 @@ void dep_graph_domaint::transform(
   goto_programt::const_targett from,
   goto_programt::const_targett to,
   ai_baset &ai,
-  const namespacet &ns,
-  ai_domain_baset::edge_typet edge_type)
+  const namespacet &ns)
 {
   dependence_grapht *dep_graph=dynamic_cast<dependence_grapht*>(&ai);
   assert(dep_graph!=nullptr);
@@ -196,15 +195,14 @@ void dep_graph_domaint::transform(
   // propagate control dependencies across function calls
   if(from->is_function_call())
   {
-    const goto_programt::const_targett next = std::next(from);
-
-    if(edge_type == ai_domain_baset::edge_typet::FUNCTION_LOCAL)
+    if(from->function == to->function)
     {
       control_dependencies(from, to, *dep_graph);
     }
     else
     {
       // edge to function entry point
+      const goto_programt::const_targett next = std::next(from);
 
       dep_graph_domaint *s=
         dynamic_cast<dep_graph_domaint*>(&(dep_graph->get_state(next)));
diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h
index 97f7548e0f7..30b97108776 100644
--- a/src/analyses/dependence_graph.h
+++ b/src/analyses/dependence_graph.h
@@ -83,8 +83,7 @@ class dep_graph_domaint:public ai_domain_baset
     goto_programt::const_targett from,
     goto_programt::const_targett to,
     ai_baset &ai,
-    const namespacet &ns,
-    ai_domain_baset::edge_typet edge_type) final override;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp
index 90fc7f5f87c..1598b9ededa 100644
--- a/src/analyses/escape_analysis.cpp
+++ b/src/analyses/escape_analysis.cpp
@@ -165,8 +165,7 @@ void escape_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns,
-  ai_domain_baset::edge_typet /*edge_type*/)
+  const namespacet &ns)
 {
   if(has_values.is_false())
     return;
diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h
index 0020859bf8f..bbf05973b13 100644
--- a/src/analyses/escape_analysis.h
+++ b/src/analyses/escape_analysis.h
@@ -28,12 +28,9 @@ class escape_domaint:public ai_domain_baset
   {
   }
 
-  void transform(
-    locationt from,
-    locationt to,
-    ai_baset &ai,
-    const namespacet &ns,
-    ai_domain_baset::edge_typet edge_type) final override;
+  void
+  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
+    final override;
 
   void output(
     std::ostream &out,
diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp
index 32f4f32589b..82c1f5a72dc 100644
--- a/src/analyses/global_may_alias.cpp
+++ b/src/analyses/global_may_alias.cpp
@@ -79,8 +79,7 @@ void global_may_alias_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns,
-  ai_domain_baset::edge_typet /*edge_type*/)
+  const namespacet &ns)
 {
   if(has_values.is_false())
     return;
diff --git a/src/analyses/global_may_alias.h b/src/analyses/global_may_alias.h
index 5ab40edbe57..b8f3480bb1c 100644
--- a/src/analyses/global_may_alias.h
+++ b/src/analyses/global_may_alias.h
@@ -28,12 +28,9 @@ class global_may_alias_domaint:public ai_domain_baset
   {
   }
 
-  void transform(
-    locationt from,
-    locationt to,
-    ai_baset &ai,
-    const namespacet &ns,
-    ai_domain_baset::edge_typet edge_type) final override;
+  void
+  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
+    final override;
 
   void output(
     std::ostream &out,
diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
index 649e24b8a60..1b237c31f1f 100644
--- a/src/analyses/interval_domain.cpp
+++ b/src/analyses/interval_domain.cpp
@@ -59,8 +59,7 @@ void interval_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns,
-  ai_domain_baset::edge_typet /*edge_type*/)
+  const namespacet &ns)
 {
   const goto_programt::instructiont &instruction=*from;
   switch(instruction.type)
@@ -79,12 +78,17 @@ void interval_domaint::transform(
 
   case GOTO:
     {
+      // Comparing iterators is safe as the target must be within the same list
+      // of instructions because this is a GOTO.
       locationt next=from;
       next++;
-      if(next==to)
-        assume(not_exprt(instruction.guard), ns);
-      else
-        assume(instruction.guard, ns);
+      if(from->get_target() != next) // If equal then a skip
+      {
+        if(next == to)
+          assume(not_exprt(instruction.guard), ns);
+        else
+          assume(instruction.guard, ns);
+      }
     }
     break;
 
diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h
index 16dc3cbdd7b..f94236861e6 100644
--- a/src/analyses/interval_domain.h
+++ b/src/analyses/interval_domain.h
@@ -32,12 +32,9 @@ class interval_domaint:public ai_domain_baset
   {
   }
 
-  void transform(
-    locationt from,
-    locationt to,
-    ai_baset &ai,
-    const namespacet &ns,
-    ai_domain_baset::edge_typet edge_type) final override;
+  void
+  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
+    final override;
 
   void output(
     std::ostream &out,
diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp
index d7e3800786b..1e1015eb404 100644
--- a/src/analyses/invariant_set_domain.cpp
+++ b/src/analyses/invariant_set_domain.cpp
@@ -17,13 +17,14 @@ void invariant_set_domaint::transform(
   locationt from_l,
   locationt to_l,
   ai_baset &ai,
-  const namespacet &ns,
-  ai_domain_baset::edge_typet /*edge_type*/)
+  const namespacet &ns)
 {
   switch(from_l->type)
   {
   case GOTO:
     {
+      // Comparing iterators is safe as the target must be within the same list
+      // of instructions because this is a GOTO.
       exprt tmp(from_l->guard);
 
       goto_programt::const_targett next=from_l;
diff --git a/src/analyses/invariant_set_domain.h b/src/analyses/invariant_set_domain.h
index 59e29b4efa6..367e987c709 100644
--- a/src/analyses/invariant_set_domain.h
+++ b/src/analyses/invariant_set_domain.h
@@ -56,8 +56,7 @@ class invariant_set_domaint:public ai_domain_baset
     locationt from_l,
     locationt to_l,
     ai_baset &ai,
-    const namespacet &ns,
-    ai_domain_baset::edge_typet edge_type) final override;
+    const namespacet &ns) final override;
 
   void make_top() final override
   {
diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp
index 2910bf3c629..c509fcac857 100644
--- a/src/analyses/is_threaded.cpp
+++ b/src/analyses/is_threaded.cpp
@@ -48,12 +48,9 @@ class is_threaded_domaint:public ai_domain_baset
            old_is_threaded!=is_threaded;
   }
 
-  void transform(
-    locationt from,
-    locationt to,
-    ai_baset &ai,
-    const namespacet &ns,
-    ai_domain_baset::edge_typet /*edge_type*/) final override
+  void
+  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
+    final override
   {
     // assert(reachable);
 
diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp
index 02cdfa4dd2c..7788835f0db 100644
--- a/src/analyses/reaching_definitions.cpp
+++ b/src/analyses/reaching_definitions.cpp
@@ -59,8 +59,7 @@ void rd_range_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns,
-  ai_domain_baset::edge_typet edge_type)
+  const namespacet &ns)
 {
   reaching_definitions_analysist *rd=
     dynamic_cast<reaching_definitions_analysist*>(&ai);
@@ -79,7 +78,7 @@ void rd_range_domaint::transform(
     transform_start_thread(ns, *rd);
   // do argument-to-parameter assignments
   else if(from->is_function_call())
-    transform_function_call(ns, from, to, *rd, edge_type);
+    transform_function_call(ns, from, to, *rd);
   // cleanup parameters
   else if(from->is_end_function())
     transform_end_function(ns, from, to, *rd);
@@ -170,13 +169,12 @@ void rd_range_domaint::transform_function_call(
   const namespacet &ns,
   locationt from,
   locationt to,
-  reaching_definitions_analysist &rd,
-  ai_domain_baset::edge_typet edge_type)
+  reaching_definitions_analysist &rd)
 {
   const code_function_callt &code=to_code_function_call(from->code);
 
   // only if there is an actual call, i.e., we have a body
-  if(edge_type != ai_domain_baset::edge_typet::FUNCTION_LOCAL)
+  if(from->function != to->function)
   {
     for(valuest::iterator it=values.begin();
         it!=values.end();
diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h
index ce112c1ed66..046dae22863 100644
--- a/src/analyses/reaching_definitions.h
+++ b/src/analyses/reaching_definitions.h
@@ -113,12 +113,9 @@ class rd_range_domaint:public ai_domain_baset
     bv_container=&_bv_container;
   }
 
-  void transform(
-    locationt from,
-    locationt to,
-    ai_baset &ai,
-    const namespacet &ns,
-    ai_domain_baset::edge_typet edge_type) final override;
+  void
+  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
+    final override;
 
   void output(
     std::ostream &out,
@@ -218,8 +215,7 @@ class rd_range_domaint:public ai_domain_baset
     const namespacet &ns,
     locationt from,
     locationt to,
-    reaching_definitions_analysist &rd,
-    ai_domain_baset::edge_typet edge_type);
+    reaching_definitions_analysist &rd);
   void transform_end_function(
     const namespacet &ns,
     locationt from,
diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp
index 5310f0ffcb0..4f92eaebd49 100644
--- a/src/analyses/uninitialized_domain.cpp
+++ b/src/analyses/uninitialized_domain.cpp
@@ -20,8 +20,7 @@ void uninitialized_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns,
-  ai_domain_baset::edge_typet /*edge_type*/)
+  const namespacet &ns)
 {
   if(has_values.is_false())
     return;
diff --git a/src/analyses/uninitialized_domain.h b/src/analyses/uninitialized_domain.h
index afc0b71fed7..2d957d0bbb5 100644
--- a/src/analyses/uninitialized_domain.h
+++ b/src/analyses/uninitialized_domain.h
@@ -29,12 +29,9 @@ class uninitialized_domaint:public ai_domain_baset
   typedef std::set<irep_idt> uninitializedt;
   uninitializedt uninitialized;
 
-  void transform(
-    locationt from,
-    locationt to,
-    ai_baset &ai,
-    const namespacet &ns,
-    ai_domain_baset::edge_typet edge_type) final override;
+  void
+  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
+    final override;
 
   void output(
     std::ostream &out,
diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp
index 004ae391a60..c8ea9dae2d2 100644
--- a/unit/analyses/ai/ai_simplify_lhs.cpp
+++ b/unit/analyses/ai/ai_simplify_lhs.cpp
@@ -25,12 +25,7 @@
 class constant_simplification_mockt:public ai_domain_baset
 {
 public:
-  void transform(
-    locationt,
-    locationt,
-    ai_baset &,
-    const namespacet &,
-    ai_domain_baset::edge_typet) override
+  void transform(locationt, locationt, ai_baset &, const namespacet &) override
   {}
   void make_bottom() override
   {}