diff --git a/.travis.yml b/.travis.yml
index 8b1e9c98a0f..305cd75273f 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -65,7 +65,9 @@ jobs:
       before_install:
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
       # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
-      env: COMPILER="ccache g++-5"
+      env:
+        - COMPILER="ccache g++-5"
+        - EXTRA_CXXFLAGS="-D_GLIBCXX_DEBUG"
 
     # OS X using g++
     - stage: Test different OS/CXX/Flags
diff --git a/regression/cbmc-cover/built-ins7/test.desc b/regression/cbmc-cover/built-ins7/test.desc
index cea40c3340e..bcffa040ad5 100644
--- a/regression/cbmc-cover/built-ins7/test.desc
+++ b/regression/cbmc-cover/built-ins7/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc --unwind 5
 ^EXIT=0$
@@ -7,3 +7,6 @@ main.c
 --
 ^warning: ignoring
 ^\[.*<builtin-library-
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
diff --git a/regression/cbmc-cover/mcdc1/test.desc b/regression/cbmc-cover/mcdc1/test.desc
index 6fe0cd3a5f0..57f43d6c757 100644
--- a/regression/cbmc-cover/mcdc1/test.desc
+++ b/regression/cbmc-cover/mcdc1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -12,3 +12,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
diff --git a/regression/cbmc-cover/mcdc10/test.desc b/regression/cbmc-cover/mcdc10/test.desc
index 87c44864772..fa3c56f7fe9 100644
--- a/regression/cbmc-cover/mcdc10/test.desc
+++ b/regression/cbmc-cover/mcdc10/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,3 +10,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
diff --git a/regression/cbmc-cover/mcdc11/test.desc b/regression/cbmc-cover/mcdc11/test.desc
index 2027e1577be..610510eb049 100644
--- a/regression/cbmc-cover/mcdc11/test.desc
+++ b/regression/cbmc-cover/mcdc11/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -12,3 +12,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
diff --git a/regression/cbmc-cover/mcdc12/test.desc b/regression/cbmc-cover/mcdc12/test.desc
index 03a731e6d27..ae5f712ca95 100644
--- a/regression/cbmc-cover/mcdc12/test.desc
+++ b/regression/cbmc-cover/mcdc12/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -15,3 +15,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
diff --git a/regression/cbmc-cover/mcdc13/test.desc b/regression/cbmc-cover/mcdc13/test.desc
index e47d7569f65..1771bf12de1 100644
--- a/regression/cbmc-cover/mcdc13/test.desc
+++ b/regression/cbmc-cover/mcdc13/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,3 +10,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
diff --git a/regression/cbmc-cover/mcdc14/test.desc b/regression/cbmc-cover/mcdc14/test.desc
index 09cf68d35d2..ebe50bf91f3 100644
--- a/regression/cbmc-cover/mcdc14/test.desc
+++ b/regression/cbmc-cover/mcdc14/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -8,3 +8,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
diff --git a/regression/cbmc-cover/mcdc2/test.desc b/regression/cbmc-cover/mcdc2/test.desc
index cc4a53abf4d..c5e2b92a2dc 100644
--- a/regression/cbmc-cover/mcdc2/test.desc
+++ b/regression/cbmc-cover/mcdc2/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,3 +10,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
diff --git a/regression/cbmc-cover/mcdc3/test.desc b/regression/cbmc-cover/mcdc3/test.desc
index 396c7cd5e0d..576db986f1d 100644
--- a/regression/cbmc-cover/mcdc3/test.desc
+++ b/regression/cbmc-cover/mcdc3/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -9,3 +9,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
diff --git a/regression/cbmc-cover/mcdc4/test.desc b/regression/cbmc-cover/mcdc4/test.desc
index 1c469418a26..ca6fc4a69b0 100644
--- a/regression/cbmc-cover/mcdc4/test.desc
+++ b/regression/cbmc-cover/mcdc4/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -11,3 +11,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
diff --git a/regression/cbmc-cover/mcdc5/test.desc b/regression/cbmc-cover/mcdc5/test.desc
index 2ffe2ed4744..8d409e19d4e 100644
--- a/regression/cbmc-cover/mcdc5/test.desc
+++ b/regression/cbmc-cover/mcdc5/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -11,3 +11,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
diff --git a/regression/cbmc-cover/mcdc6/test.desc b/regression/cbmc-cover/mcdc6/test.desc
index 267488742c2..c3267861d12 100644
--- a/regression/cbmc-cover/mcdc6/test.desc
+++ b/regression/cbmc-cover/mcdc6/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -8,3 +8,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
diff --git a/regression/cbmc-cover/mcdc7/test.desc b/regression/cbmc-cover/mcdc7/test.desc
index c288cbab0ce..9a866c50206 100644
--- a/regression/cbmc-cover/mcdc7/test.desc
+++ b/regression/cbmc-cover/mcdc7/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,3 +10,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
diff --git a/regression/cbmc-cover/mcdc8/test.desc b/regression/cbmc-cover/mcdc8/test.desc
index 43a1b2ca741..7d5ede41f40 100644
--- a/regression/cbmc-cover/mcdc8/test.desc
+++ b/regression/cbmc-cover/mcdc8/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,3 +10,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
diff --git a/regression/cbmc-cover/mcdc9/test.desc b/regression/cbmc-cover/mcdc9/test.desc
index 199f3f14885..f75ea6bfddd 100644
--- a/regression/cbmc-cover/mcdc9/test.desc
+++ b/regression/cbmc-cover/mcdc9/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -11,3 +11,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details
diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
index dedb2da9a3c..d76391c6446 100644
--- a/src/analyses/ai.cpp
+++ b/src/analyses/ai.cpp
@@ -365,7 +365,8 @@ bool ai_baset::visit(
       // initialize state, if necessary
       get_state(to_l);
 
-      new_values.transform(l, to_l, *this, ns);
+      new_values.transform(
+        l, to_l, *this, ns, ai_domain_baset::edge_typet::FUNCTION_LOCAL);
 
       if(merge(new_values, l, to_l))
         have_new_values=true;
@@ -398,7 +399,8 @@ 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);
+    tmp_state->transform(
+      l_call, l_return, *this, ns, ai_domain_baset::edge_typet::FUNCTION_LOCAL);
 
     return merge(*tmp_state, l_call, l_return);
   }
@@ -415,7 +417,8 @@ 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);
+    tmp_state->transform(
+      l_call, l_begin, *this, ns, ai_domain_baset::edge_typet::CALL);
 
     bool new_data=false;
 
@@ -442,7 +445,8 @@ 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);
+    tmp_state->transform(
+      l_end, l_return, *this, ns, ai_domain_baset::edge_typet::RETURN);
 
     // Propagate those
     return merge(*tmp_state, l_end, l_return);
diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index a09e43f699f..99d1b130345 100644
--- a/src/analyses/ai.h
+++ b/src/analyses/ai.h
@@ -31,6 +31,13 @@ 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()
@@ -53,7 +60,8 @@ class ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns)=0;
+    const namespacet &ns,
+    edge_typet edge_type) = 0;
 
   virtual void output(
     std::ostream &out,
@@ -401,7 +409,9 @@ class ait:public ai_baset
   }
 
 protected:
-  typedef std::unordered_map<locationt, domainT, const_target_hash> state_mapt;
+  typedef std::
+    unordered_map<locationt, domainT, const_target_hash, pointee_address_equalt>
+      state_mapt;
   state_mapt state_map;
 
   // this one creates states, if need be
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index e95417f4934..c4174dc8f91 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -45,7 +45,8 @@ void constant_propagator_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns)
+  const namespacet &ns,
+  ai_domain_baset::edge_typet edge_type)
 {
 #ifdef DEBUG
   std::cout << "Transform from/to:\n";
@@ -129,7 +130,7 @@ void constant_propagator_domaint::transform(
       const symbol_exprt &symbol_expr=to_symbol_expr(function);
       const irep_idt id=symbol_expr.get_identifier();
 
-      if(to==next)
+      if(edge_type == ai_domain_baset::edge_typet::FUNCTION_LOCAL)
       {
         if(id==CPROVER_PREFIX "set_must" ||
            id==CPROVER_PREFIX "get_must" ||
diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h
index 0fc4796e8b7..1431783f918 100644
--- a/src/analyses/constant_propagator.h
+++ b/src/analyses/constant_propagator.h
@@ -25,7 +25,8 @@ class constant_propagator_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai_base,
-    const namespacet &ns) final override;
+    const namespacet &ns,
+    ai_domain_baset::edge_typet edge_type) 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 16c3fad0c4f..0b45099302b 100644
--- a/src/analyses/custom_bitvector_analysis.cpp
+++ b/src/analyses/custom_bitvector_analysis.cpp
@@ -269,7 +269,8 @@ void custom_bitvector_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns)
+  const namespacet &ns,
+  ai_domain_baset::edge_typet edge_type)
 {
   // upcast of ai
   custom_bitvector_analysist &cba=
@@ -395,11 +396,8 @@ void custom_bitvector_domaint::transform(
         }
         else
         {
-          goto_programt::const_targett next=from;
-          ++next;
-
           // only if there is an actual call, i.e., we have a body
-          if(next!=to)
+          if(edge_type != ai_domain_baset::edge_typet::FUNCTION_LOCAL)
           {
             const code_typet &code_type=
               to_code_type(ns.lookup(identifier).type);
diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h
index 4896d768cb7..e64a83e585c 100644
--- a/src/analyses/custom_bitvector_analysis.h
+++ b/src/analyses/custom_bitvector_analysis.h
@@ -27,7 +27,8 @@ class custom_bitvector_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final override;
+    const namespacet &ns,
+    ai_domain_baset::edge_typet edge_type) final override;
 
   void output(
     std::ostream &out,
diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp
index 5f1bae158bc..6d691528ca8 100644
--- a/src/analyses/dependence_graph.cpp
+++ b/src/analyses/dependence_graph.cpp
@@ -187,7 +187,8 @@ void dep_graph_domaint::transform(
   goto_programt::const_targett from,
   goto_programt::const_targett to,
   ai_baset &ai,
-  const namespacet &ns)
+  const namespacet &ns,
+  ai_domain_baset::edge_typet edge_type)
 {
   dependence_grapht *dep_graph=dynamic_cast<dependence_grapht*>(&ai);
   assert(dep_graph!=nullptr);
@@ -195,10 +196,9 @@ void dep_graph_domaint::transform(
   // propagate control dependencies across function calls
   if(from->is_function_call())
   {
-    goto_programt::const_targett next=from;
-    ++next;
+    const goto_programt::const_targett next = std::next(from);
 
-    if(next==to)
+    if(edge_type == ai_domain_baset::edge_typet::FUNCTION_LOCAL)
     {
       control_dependencies(from, to, *dep_graph);
     }
diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h
index 30b97108776..97f7548e0f7 100644
--- a/src/analyses/dependence_graph.h
+++ b/src/analyses/dependence_graph.h
@@ -83,7 +83,8 @@ class dep_graph_domaint:public ai_domain_baset
     goto_programt::const_targett from,
     goto_programt::const_targett to,
     ai_baset &ai,
-    const namespacet &ns) final override;
+    const namespacet &ns,
+    ai_domain_baset::edge_typet edge_type) final override;
 
   void output(
     std::ostream &out,
diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp
index 507df39f770..5b4585d421b 100644
--- a/src/analyses/escape_analysis.cpp
+++ b/src/analyses/escape_analysis.cpp
@@ -165,7 +165,8 @@ void escape_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns)
+  const namespacet &ns,
+  ai_domain_baset::edge_typet /*edge_type*/)
 {
   if(has_values.is_false())
     return;
diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h
index 52de2b5dfc8..0020859bf8f 100644
--- a/src/analyses/escape_analysis.h
+++ b/src/analyses/escape_analysis.h
@@ -32,7 +32,8 @@ class escape_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final override;
+    const namespacet &ns,
+    ai_domain_baset::edge_typet edge_type) final override;
 
   void output(
     std::ostream &out,
diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp
index 82c1f5a72dc..32f4f32589b 100644
--- a/src/analyses/global_may_alias.cpp
+++ b/src/analyses/global_may_alias.cpp
@@ -79,7 +79,8 @@ void global_may_alias_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns)
+  const namespacet &ns,
+  ai_domain_baset::edge_typet /*edge_type*/)
 {
   if(has_values.is_false())
     return;
diff --git a/src/analyses/global_may_alias.h b/src/analyses/global_may_alias.h
index a5e1b0cd49a..5ab40edbe57 100644
--- a/src/analyses/global_may_alias.h
+++ b/src/analyses/global_may_alias.h
@@ -32,7 +32,8 @@ class global_may_alias_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final override;
+    const namespacet &ns,
+    ai_domain_baset::edge_typet edge_type) final override;
 
   void output(
     std::ostream &out,
diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
index 5f1b9a314b5..649e24b8a60 100644
--- a/src/analyses/interval_domain.cpp
+++ b/src/analyses/interval_domain.cpp
@@ -59,7 +59,8 @@ void interval_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns)
+  const namespacet &ns,
+  ai_domain_baset::edge_typet /*edge_type*/)
 {
   const goto_programt::instructiont &instruction=*from;
   switch(instruction.type)
diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h
index 7702990d53d..16dc3cbdd7b 100644
--- a/src/analyses/interval_domain.h
+++ b/src/analyses/interval_domain.h
@@ -36,7 +36,8 @@ class interval_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final override;
+    const namespacet &ns,
+    ai_domain_baset::edge_typet edge_type) final override;
 
   void output(
     std::ostream &out,
diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp
index 3132591eb42..d7e3800786b 100644
--- a/src/analyses/invariant_set_domain.cpp
+++ b/src/analyses/invariant_set_domain.cpp
@@ -17,7 +17,8 @@ void invariant_set_domaint::transform(
   locationt from_l,
   locationt to_l,
   ai_baset &ai,
-  const namespacet &ns)
+  const namespacet &ns,
+  ai_domain_baset::edge_typet /*edge_type*/)
 {
   switch(from_l->type)
   {
diff --git a/src/analyses/invariant_set_domain.h b/src/analyses/invariant_set_domain.h
index 367e987c709..59e29b4efa6 100644
--- a/src/analyses/invariant_set_domain.h
+++ b/src/analyses/invariant_set_domain.h
@@ -56,7 +56,8 @@ class invariant_set_domaint:public ai_domain_baset
     locationt from_l,
     locationt to_l,
     ai_baset &ai,
-    const namespacet &ns) final override;
+    const namespacet &ns,
+    ai_domain_baset::edge_typet edge_type) final override;
 
   void make_top() final override
   {
diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp
index 54a3fa2d70d..2910bf3c629 100644
--- a/src/analyses/is_threaded.cpp
+++ b/src/analyses/is_threaded.cpp
@@ -52,7 +52,8 @@ class is_threaded_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final override
+    const namespacet &ns,
+    ai_domain_baset::edge_typet /*edge_type*/) final override
   {
     // assert(reachable);
 
diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp
index c3242849511..02cdfa4dd2c 100644
--- a/src/analyses/reaching_definitions.cpp
+++ b/src/analyses/reaching_definitions.cpp
@@ -59,7 +59,8 @@ void rd_range_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns)
+  const namespacet &ns,
+  ai_domain_baset::edge_typet edge_type)
 {
   reaching_definitions_analysist *rd=
     dynamic_cast<reaching_definitions_analysist*>(&ai);
@@ -78,7 +79,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);
+    transform_function_call(ns, from, to, *rd, edge_type);
   // cleanup parameters
   else if(from->is_end_function())
     transform_end_function(ns, from, to, *rd);
@@ -169,15 +170,13 @@ void rd_range_domaint::transform_function_call(
   const namespacet &ns,
   locationt from,
   locationt to,
-  reaching_definitions_analysist &rd)
+  reaching_definitions_analysist &rd,
+  ai_domain_baset::edge_typet edge_type)
 {
   const code_function_callt &code=to_code_function_call(from->code);
 
-  goto_programt::const_targett next=from;
-  ++next;
-
   // only if there is an actual call, i.e., we have a body
-  if(next!=to)
+  if(edge_type != ai_domain_baset::edge_typet::FUNCTION_LOCAL)
   {
     for(valuest::iterator it=values.begin();
         it!=values.end();
diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h
index e218eb19bca..ce112c1ed66 100644
--- a/src/analyses/reaching_definitions.h
+++ b/src/analyses/reaching_definitions.h
@@ -117,7 +117,8 @@ class rd_range_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final override;
+    const namespacet &ns,
+    ai_domain_baset::edge_typet edge_type) final override;
 
   void output(
     std::ostream &out,
@@ -217,7 +218,8 @@ class rd_range_domaint:public ai_domain_baset
     const namespacet &ns,
     locationt from,
     locationt to,
-    reaching_definitions_analysist &rd);
+    reaching_definitions_analysist &rd,
+    ai_domain_baset::edge_typet edge_type);
   void transform_end_function(
     const namespacet &ns,
     locationt from,
diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp
index 4f92eaebd49..5310f0ffcb0 100644
--- a/src/analyses/uninitialized_domain.cpp
+++ b/src/analyses/uninitialized_domain.cpp
@@ -20,7 +20,8 @@ void uninitialized_domaint::transform(
   locationt from,
   locationt to,
   ai_baset &ai,
-  const namespacet &ns)
+  const namespacet &ns,
+  ai_domain_baset::edge_typet /*edge_type*/)
 {
   if(has_values.is_false())
     return;
diff --git a/src/analyses/uninitialized_domain.h b/src/analyses/uninitialized_domain.h
index 45a9d085c99..afc0b71fed7 100644
--- a/src/analyses/uninitialized_domain.h
+++ b/src/analyses/uninitialized_domain.h
@@ -33,7 +33,8 @@ class uninitialized_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final override;
+    const namespacet &ns,
+    ai_domain_baset::edge_typet edge_type) final override;
 
   void output(
     std::ostream &out,
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index 4f2804e1521..da5a1ce073c 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -591,9 +591,9 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
     if(dest->operands().empty())
     {
       warning().source_location=value.find_source_location();
-      warning() << "initialisation of " << full_type.id()
-                << " requires initializer list, found "
-                << value.id() << " instead" << eom;
+      warning() << "initialisation of " << dest_type.id()
+                << " requires initializer list, found " << value.id()
+                << " instead" << eom;
 
       // in case of a variable-length array consume all remaining
       // initializer elements
diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp
index bb5b9d5a912..3757c8cead1 100644
--- a/src/cpp/cpp_typecheck_compound_type.cpp
+++ b/src/cpp/cpp_typecheck_compound_type.cpp
@@ -1271,7 +1271,7 @@ void cpp_typecheckt::typecheck_member_function(
       method_qualifier);
   }
 
-  if(value.id()=="cpp_not_typechecked")
+  if(value.id() == "cpp_not_typechecked" && value.has_operands())
     move_member_initializers(initializers, type, value.op0());
   else
     move_member_initializers(initializers, type, value);
diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp
index d76afe03b71..a478bc66d77 100644
--- a/src/goto-instrument/cover.cpp
+++ b/src/goto-instrument/cover.cpp
@@ -1553,6 +1553,7 @@ void instrument_cover_goals(
         remove_repetition(controlling);
         // for now, we restrict to the case of a single ''decision'';
         // however, this is not true, e.g., ''? :'' operator.
+        INVARIANT(!decisions.empty(), "There must be at least one decision");
         minimize_mcdc_controlling(controlling, *decisions.begin());
 
         for(const auto &p : controlling)
diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h
index 264cf77c77c..fd48166b0b7 100644
--- a/src/goto-programs/goto_program_template.h
+++ b/src/goto-programs/goto_program_template.h
@@ -807,7 +807,21 @@ struct const_target_hash_templatet
 {
   std::size_t operator()(
     const typename goto_program_templatet<codeT, guardT>::const_targett t) const
-  { return t->location_number; }
+  {
+    using hash_typet = decltype(&(*t));
+    return std::hash<hash_typet>{}(&(*t));
+  }
+};
+
+/// Functor to check whether iterators from different collections point at the
+/// same object.
+struct pointee_address_equalt
+{
+  template <class A, class B>
+  bool operator()(const A &a, const B &b) const
+  {
+    return &(*a) == &(*b);
+  }
 };
 
 #endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_TEMPLATE_H
diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index 9c2c8d2f51c..e316b00ccba 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -18,6 +18,8 @@ Author: Daniel Kroening
 #include <util/prefix.h>
 #include <util/ssa_expr.h>
 
+#include <goto-programs/goto_program_template.h>
+
 void graphml_witnesst::remove_l0_l1(exprt &expr)
 {
   if(expr.id()==ID_symbol)
@@ -241,10 +243,10 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
       continue;
     }
 
-    goto_tracet::stepst::const_iterator next=it;
-    for(++next;
-        next!=goto_trace.steps.end() &&
-        (step_to_node[next->step_nr]==sink || it->pc==next->pc);
+    auto next = std::next(it);
+    for(; next != goto_trace.steps.end() &&
+          (step_to_node[next->step_nr] == sink ||
+           pointee_address_equalt{}(it->pc, next->pc)); // NOLINT
         ++next)
     {
       // advance
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index c25bc90d32d..0b48caff4c3 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -1808,7 +1808,7 @@ static void initial_index_set(
 
   while(!to_process.empty())
   {
-    const exprt &cur = to_process.back();
+    const exprt cur = to_process.back();
     to_process.pop_back();
     if(cur.id() == ID_index && is_char_type(cur.type()))
     {
diff --git a/src/util/expr_iterator.h b/src/util/expr_iterator.h
index be228bcfba4..1c43c953d69 100644
--- a/src/util/expr_iterator.h
+++ b/src/util/expr_iterator.h
@@ -53,7 +53,10 @@ struct depth_iterator_expr_statet final
 inline bool operator==(
   const depth_iterator_expr_statet &left,
   const depth_iterator_expr_statet &right)
-{ return left.it==right.it && left.expr.get()==right.expr.get(); }
+{
+  return distance(left.it, left.end) == distance(right.it, right.end) &&
+         left.expr.get() == right.expr.get();
+}
 
 /// Depth first search iterator base - iterates over supplied expression
 /// and all its operands recursively.
@@ -99,8 +102,12 @@ class depth_iterator_baset
   depth_iterator_t &next_sibling_or_parent()
   {
     PRECONDITION(!m_stack.empty());
-    m_stack.back().it=m_stack.back().end;
-    ++(*this);
+    m_stack.pop_back();
+    if(!m_stack.empty())
+    {
+      ++m_stack.back().it;
+      return ++(*this);
+    }
     return this->downcast();
   }
 
diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp
index c8ea9dae2d2..004ae391a60 100644
--- a/unit/analyses/ai/ai_simplify_lhs.cpp
+++ b/unit/analyses/ai/ai_simplify_lhs.cpp
@@ -25,7 +25,12 @@
 class constant_simplification_mockt:public ai_domain_baset
 {
 public:
-  void transform(locationt, locationt, ai_baset &, const namespacet &) override
+  void transform(
+    locationt,
+    locationt,
+    ai_baset &,
+    const namespacet &,
+    ai_domain_baset::edge_typet) override
   {}
   void make_bottom() override
   {}