diff --git a/regression/goto-analyzer/sensitivity-function-call-recursive/main.c b/regression/goto-analyzer/sensitivity-function-call-recursive/main.c
new file mode 100644
index 00000000000..b9e6daf3347
--- /dev/null
+++ b/regression/goto-analyzer/sensitivity-function-call-recursive/main.c
@@ -0,0 +1,56 @@
+#include <assert.h>
+
+int bar(int other)
+{
+  if(other > 0)
+  {
+    int value = bar(other - 1);
+    return value + 1;
+  }
+  else
+  {
+    return 0;
+  }
+}
+
+int bar_clean(int other)
+{
+  if(other > 0)
+  {
+    int value = bar_clean(other - 1);
+    return value + 1;
+  }
+  else
+  {
+    return 0;
+  }
+}
+
+int fun(int changing, int constant)
+{
+  if(changing > 0)
+  {
+    int value = fun(changing - 1, constant);
+    return value;
+  }
+  else
+  {
+    return constant;
+  }
+}
+
+int main(int argc, char *argv[])
+{
+  int x=3;
+  int y=bar(x+1);
+  assert(y==4); // Unknown in the constants domain
+
+  int y2 = bar(0);
+  assert(y2==0); // Unknown since we are not sensitive to call domain
+
+  int z = bar_clean(0);
+  assert(z==0); // Unknown as the function has parameter as top
+
+  int w = fun(5, 18);
+  assert(w==18);
+}
diff --git a/regression/goto-analyzer/sensitivity-function-call-recursive/test.desc b/regression/goto-analyzer/sensitivity-function-call-recursive/test.desc
new file mode 100644
index 00000000000..88534789621
--- /dev/null
+++ b/regression/goto-analyzer/sensitivity-function-call-recursive/test.desc
@@ -0,0 +1,11 @@
+KNOWNBUG
+main.c
+--variable --pointers --arrays --structs --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] .* assertion y==4: Unknown$
+^\[main\.assertion\.2\] .* assertion y2==0: Unknown$
+^\[main\.assertion\.3\] .* assertion z==0: Success$
+^\[main\.assertion\.4\] .* assertion w==18: Success$
+--
+^warning: ignoring
diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
index 9591d0b2725..c70206a41ad 100644
--- a/src/analyses/ai.cpp
+++ b/src/analyses/ai.cpp
@@ -37,7 +37,7 @@ xmlt ai_domain_baset::output_xml(
 {
   std::ostringstream out;
   output(out, ai, ns);
-  xmlt xml("domain");
+  xmlt xml("abstract_state");
   xml.data=out.str();
   return xml;
 }
@@ -170,7 +170,7 @@ jsont ai_baset::output_json(
       json_numbert(std::to_string(i_it->location_number));
     location["sourceLocation"]=
       json_stringt(i_it->source_location.as_string());
-    location["domain"]=find_state(i_it).output_json(*this, ns);
+    location["abstractState"]=find_state(i_it).output_json(*this, ns);
 
     // Ideally we need output_instruction_json
     std::ostringstream out;
@@ -431,7 +431,12 @@ bool ai_baset::do_function_call(
     assert(l_end->is_end_function());
 
     // do edge from end of function to instruction after call
-    std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_end)));
+    const statet &end_state=get_state(l_end);
+
+    if(end_state.is_bottom())
+      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);
 
     // Propagate those
@@ -454,14 +459,6 @@ bool ai_baset::do_function_call_rec(
   {
     const irep_idt &identifier=function.get(ID_identifier);
 
-    if(recursion_set.find(identifier)!=recursion_set.end())
-    {
-      // recursion detected!
-      return new_data;
-    }
-    else
-      recursion_set.insert(identifier);
-
     goto_functionst::function_mapt::const_iterator it=
       goto_functions.function_map.find(identifier);
 
@@ -474,8 +471,6 @@ bool ai_baset::do_function_call_rec(
       it,
       arguments,
       ns);
-
-    recursion_set.erase(identifier);
   }
   else if(function.id()==ID_if)
   {
diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index a04c60547d0..1cecf984953 100644
--- a/src/analyses/ai.h
+++ b/src/analyses/ai.h
@@ -80,6 +80,10 @@ class ai_domain_baset
   // a reasonable entry-point state
   virtual void make_entry()=0;
 
+  virtual bool is_bottom() const=0;
+
+  virtual bool is_top() const=0;
+
   // also add
   //
   //   bool merge(const T &b, locationt from, locationt to);
@@ -158,6 +162,17 @@ class ai_baset
     fixedpoint(goto_function.body, goto_functions, ns);
   }
 
+  /// Returns the abstract state before the given instruction
+  virtual const ai_domain_baset & abstract_state_before(
+    goto_programt::const_targett t) const = 0;
+
+  /// Returns the abstract state after the given instruction
+  virtual const ai_domain_baset & abstract_state_after(
+    goto_programt::const_targett t) const
+  {
+    return abstract_state_before(std::next(t));
+  }
+
   virtual void clear()
   {
   }
@@ -307,9 +322,6 @@ class ai_baset
     const goto_functionst &goto_functions,
     const namespacet &ns);
 
-  typedef std::set<irep_idt> recursion_sett;
-  recursion_sett recursion_set;
-
   // function calls
   bool do_function_call_rec(
     locationt l_call, locationt l_return,
@@ -369,6 +381,12 @@ class ait:public ai_baset
     return it->second;
   }
 
+  const ai_domain_baset & abstract_state_before(
+    goto_programt::const_targett t) const override
+  {
+    return (*this)[t];
+  }
+
   void clear() override
   {
     state_map.clear();
diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h
index 695aea8782f..0fc4796e8b7 100644
--- a/src/analyses/constant_propagator.h
+++ b/src/analyses/constant_propagator.h
@@ -25,7 +25,7 @@ class constant_propagator_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai_base,
-    const namespacet &ns) override;
+    const namespacet &ns) final override;
 
   virtual void output(
     std::ostream &out,
@@ -39,23 +39,33 @@ class constant_propagator_domaint:public ai_domain_baset
 
   virtual bool ai_simplify(
     exprt &condition,
-    const namespacet &ns) const override;
+    const namespacet &ns) const final override;
 
-  virtual void make_bottom() override
+  virtual void make_bottom() final override
   {
     values.set_to_bottom();
   }
 
-  virtual void make_top() override
+  virtual void make_top() final override
   {
     values.set_to_top();
   }
 
-  virtual void make_entry() override
+  virtual void make_entry() final override
   {
     make_top();
   }
 
+  virtual bool is_bottom() const final override
+  {
+    return values.is_bot();
+  }
+
+  virtual bool is_top() const final override
+  {
+    return values.is_top();
+  }
+
   struct valuest
   {
   public:
@@ -70,27 +80,37 @@ class constant_propagator_domaint:public ai_domain_baset
 
     // set whole state
 
-    inline void set_to_bottom()
+    void set_to_bottom()
     {
       replace_const.clear();
       is_bottom=true;
     }
 
-    inline void set_to_top()
+    void set_to_top()
     {
       replace_const.clear();
       is_bottom=false;
     }
 
+    bool is_bot() const
+    {
+      return is_bottom && replace_const.empty();
+    }
+
+    bool is_top() const
+    {
+      return !is_bottom && replace_const.empty();
+    }
+
     // set single identifier
 
-    inline void set_to(const irep_idt &lhs, const exprt &rhs)
+    void set_to(const irep_idt &lhs, const exprt &rhs)
     {
       replace_const.expr_map[lhs]=rhs;
       is_bottom=false;
     }
 
-    inline void set_to(const symbol_exprt &lhs, const exprt &rhs)
+    void set_to(const symbol_exprt &lhs, const exprt &rhs)
     {
       set_to(lhs.get_identifier(), rhs);
     }
diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h
index f0c298f84d6..55d5d444af8 100644
--- a/src/analyses/custom_bitvector_analysis.h
+++ b/src/analyses/custom_bitvector_analysis.h
@@ -27,32 +27,48 @@ class custom_bitvector_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final;
+    const namespacet &ns) const final override;
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     may_bits.clear();
     must_bits.clear();
     has_values=tvt(false);
   }
 
-  void make_top() final
+  void make_top() final override
   {
     may_bits.clear();
     must_bits.clear();
     has_values=tvt(true);
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_bottom() const final override
+  {
+    DATA_INVARIANT(!has_values.is_false() ||
+                   (may_bits.empty() && must_bits.empty()),
+                   "If the domain is bottom, it must have no bits set");
+    return has_values.is_false();
+  }
+
+  bool is_top() const final override
+  {
+    DATA_INVARIANT(!has_values.is_true() ||
+                   (may_bits.empty() && must_bits.empty()),
+                   "If the domain is top, it must have no bits set");
+    return has_values.is_true();
+  }
+
   bool merge(
     const custom_bitvector_domaint &b,
     locationt from,
diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h
index 4cd7be4c589..2508174b443 100644
--- a/src/analyses/dependence_graph.h
+++ b/src/analyses/dependence_graph.h
@@ -83,12 +83,12 @@ 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;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final;
+    const namespacet &ns) const final override;
 
   jsont output_json(
     const ai_baset &ai,
@@ -96,27 +96,53 @@ class dep_graph_domaint:public ai_domain_baset
 
   void make_top() final override
   {
-    assert(node_id!=std::numeric_limits<node_indext>::max());
+    DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
+                   "node_id must not be valid");
 
     has_values=tvt(true);
     control_deps.clear();
     data_deps.clear();
   }
 
-  void make_bottom() final
+  void make_bottom() final override
   {
-    assert(node_id!=std::numeric_limits<node_indext>::max());
+    DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
+                   "node_id must be valid");
 
     has_values=tvt(false);
     control_deps.clear();
     data_deps.clear();
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_top() const final override
+  {
+    DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
+                   "node_id must be valid");
+
+    DATA_INVARIANT(!has_values.is_true() ||
+                   (control_deps.empty() && data_deps.empty()),
+                   "If the domain is top, it must have no dependencies");
+
+    return has_values.is_true();
+  }
+
+  bool is_bottom() const final override
+  {
+    DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
+                   "node_id must be valid");
+
+    DATA_INVARIANT(!has_values.is_false() ||
+                   (control_deps.empty() && data_deps.empty()),
+                   "If the domain is bottom, it must have no dependencies");
+
+    return has_values.is_false();
+  }
+
   void set_node_id(node_indext id)
   {
     node_id=id;
diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h
index 7a4c606e1d4..52de2b5dfc8 100644
--- a/src/analyses/escape_analysis.h
+++ b/src/analyses/escape_analysis.h
@@ -32,33 +32,49 @@ class escape_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final;
+    const namespacet &ns) const final override;
 
   bool merge(
     const escape_domaint &b,
     locationt from,
     locationt to);
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     cleanup_map.clear();
     aliases.clear();
     has_values=tvt(false);
   }
 
-  void make_top() final
+  void make_top() final override
   {
     cleanup_map.clear();
     aliases.clear();
     has_values=tvt(true);
   }
 
-  void make_entry() final
+  bool is_bottom() const override final
+  {
+    DATA_INVARIANT(!has_values.is_false() ||
+                   (cleanup_map.empty() && (aliases.size()==0)),
+                   "If the domain is bottom, all maps must be empty");
+    return has_values.is_false();
+  }
+
+  bool is_top() const override final
+  {
+    DATA_INVARIANT(!has_values.is_true() ||
+                   (cleanup_map.empty() && (aliases.size()==0)),
+                   "If the domain is top, all maps must be empty");
+    return has_values.is_true();
+  }
+
+  void make_entry() override final
   {
     make_top();
   }
diff --git a/src/analyses/global_may_alias.h b/src/analyses/global_may_alias.h
index d946b371c05..a5e1b0cd49a 100644
--- a/src/analyses/global_may_alias.h
+++ b/src/analyses/global_may_alias.h
@@ -32,35 +32,49 @@ class global_may_alias_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final;
+    const namespacet &ns) const final override;
 
   bool merge(
     const global_may_alias_domaint &b,
     locationt from,
     locationt to);
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     aliases.clear();
     has_values=tvt(false);
   }
 
-  void make_top() final
+  void make_top() final override
   {
     aliases.clear();
     has_values=tvt(true);
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_bottom() const final override
+  {
+    DATA_INVARIANT(!has_values.is_false() || (aliases.size()==0),
+                   "If the domain is bottom, there must be no aliases");
+    return has_values.is_false();
+  }
+
+  bool is_top() const final override
+  {
+    DATA_INVARIANT(!has_values.is_true() || (aliases.size()==0),
+                   "If the domain is top, there must be no aliases");
+    return has_values.is_true();
+  }
+
   typedef union_find<irep_idt> aliasest;
   aliasest aliases;
 
diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h
index d078324679f..7702990d53d 100644
--- a/src/analyses/interval_domain.h
+++ b/src/analyses/interval_domain.h
@@ -36,12 +36,12 @@ class interval_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final;
+    const namespacet &ns) const override;
 
 protected:
   bool join(const interval_domaint &b);
@@ -56,7 +56,7 @@ class interval_domaint:public ai_domain_baset
   }
 
   // no states
-  void make_bottom() final
+  void make_bottom() final override
   {
     int_map.clear();
     float_map.clear();
@@ -64,18 +64,34 @@ class interval_domaint:public ai_domain_baset
   }
 
   // all states
-  void make_top() final
+  void make_top() final override
   {
     int_map.clear();
     float_map.clear();
     bottom=false;
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_bottom() const override final
+  {
+    #if 0
+    // This invariant should hold but is not correctly enforced at the moment.
+    DATA_INVARIANT(!bottom || (int_map.empty() && float_map.empty()),
+                   "If the domain is bottom the value maps must be empty");
+    #endif
+
+    return bottom;
+  }
+
+  bool is_top() const override final
+  {
+    return !bottom && int_map.empty() && float_map.empty();
+  }
+
   exprt make_expression(const symbol_exprt &) const;
 
   void assume(const exprt &, const namespacet &);
@@ -90,11 +106,6 @@ class interval_domaint:public ai_domain_baset
     return src.id()==ID_floatbv;
   }
 
-  bool is_bottom() const
-  {
-    return bottom;
-  }
-
   virtual bool ai_simplify(
     exprt &condition,
     const namespacet &ns) const override;
diff --git a/src/analyses/invariant_set_domain.h b/src/analyses/invariant_set_domain.h
index 4d38b6b2657..367e987c709 100644
--- a/src/analyses/invariant_set_domain.h
+++ b/src/analyses/invariant_set_domain.h
@@ -44,7 +44,7 @@ class invariant_set_domaint:public ai_domain_baset
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final
+    const namespacet &ns) const final override
   {
     if(has_values.is_known())
       out << has_values.to_string() << '\n';
@@ -56,25 +56,35 @@ class invariant_set_domaint:public ai_domain_baset
     locationt from_l,
     locationt to_l,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
-  void make_top() final
+  void make_top() final override
   {
     invariant_set.make_true();
     has_values=tvt(true);
   }
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     invariant_set.make_false();
     has_values=tvt(false);
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     invariant_set.make_true();
     has_values=tvt(true);
   }
+
+  bool is_top() const override final
+  {
+    return has_values.is_true();
+  }
+
+  bool is_bottom() const override final
+  {
+    return has_values.is_false();
+  }
 };
 
 #endif // CPROVER_ANALYSES_INVARIANT_SET_DOMAIN_H
diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp
index 1ac32d2341c..54a3fa2d70d 100644
--- a/src/analyses/is_threaded.cpp
+++ b/src/analyses/is_threaded.cpp
@@ -52,7 +52,7 @@ class is_threaded_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final
+    const namespacet &ns) final override
   {
     // assert(reachable);
 
@@ -63,23 +63,36 @@ class is_threaded_domaint:public ai_domain_baset
       is_threaded=true;
   }
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     reachable=false;
     is_threaded=false;
   }
 
-  void make_top() final
+  void make_top() final override
   {
     reachable=true;
     is_threaded=true;
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     reachable=true;
     is_threaded=false;
   }
+
+  bool is_bottom() const override final
+  {
+    DATA_INVARIANT(reachable || !is_threaded,
+                   "A location cannot be threaded if it is not reachable.");
+
+    return !reachable;
+  }
+
+  bool is_top() const override final
+  {
+    return reachable && is_threaded;
+  }
 };
 
 void is_threadedt::compute(const goto_functionst &goto_functions)
diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h
index c62bd5e4b51..e218eb19bca 100644
--- a/src/analyses/reaching_definitions.h
+++ b/src/analyses/reaching_definitions.h
@@ -117,17 +117,17 @@ class rd_range_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final
+    const namespacet &ns) const final override
   {
     output(out);
   }
 
-  void make_top() final
+  void make_top() final override
   {
     values.clear();
     if(bv_container)
@@ -135,7 +135,7 @@ class rd_range_domaint:public ai_domain_baset
     has_values=tvt(true);
   }
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     values.clear();
     if(bv_container)
@@ -143,11 +143,25 @@ class rd_range_domaint:public ai_domain_baset
     has_values=tvt(false);
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_top() const override final
+  {
+    DATA_INVARIANT(!has_values.is_true() || values.empty(),
+                   "If domain is top, the value map must be empty");
+    return has_values.is_true();
+  }
+
+  bool is_bottom() const override final
+  {
+    DATA_INVARIANT(!has_values.is_false() || values.empty(),
+                   "If domain is bottom, the value map must be empty");
+    return has_values.is_false();
+  }
+
   // returns true iff there is something new
   bool merge(
     const rd_range_domaint &other,
@@ -246,9 +260,9 @@ class reaching_definitions_analysist:
   virtual ~reaching_definitions_analysist();
 
   virtual void initialize(
-    const goto_functionst &goto_functions);
+    const goto_functionst &goto_functions) override;
 
-  virtual statet &get_state(goto_programt::const_targett l)
+  virtual statet &get_state(goto_programt::const_targett l) override
   {
     statet &s=concurrency_aware_ait<rd_range_domaint>::get_state(l);
 
diff --git a/src/analyses/uninitialized_domain.h b/src/analyses/uninitialized_domain.h
index 11dcaa02170..45a9d085c99 100644
--- a/src/analyses/uninitialized_domain.h
+++ b/src/analyses/uninitialized_domain.h
@@ -33,30 +33,44 @@ class uninitialized_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
     const namespacet &ns) const final;
 
-  void make_top() final
+  void make_top() final override
   {
     uninitialized.clear();
     has_values=tvt(true);
   }
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     uninitialized.clear();
     has_values=tvt(false);
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_top() const override final
+  {
+    DATA_INVARIANT(!has_values.is_true() || uninitialized.empty(),
+                   "If domain is top, the uninitialized set must be empty");
+    return has_values.is_true();
+  }
+
+  bool is_bottom() const override final
+  {
+    DATA_INVARIANT(!has_values.is_false() || uninitialized.empty(),
+                   "If domain is bottom, the uninitialized set must be empty");
+    return has_values.is_false();
+  }
+
   // returns true iff there is something new
   bool merge(
     const uninitialized_domaint &other,
diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp
index d345468fd99..c8ea9dae2d2 100644
--- a/unit/analyses/ai/ai_simplify_lhs.cpp
+++ b/unit/analyses/ai/ai_simplify_lhs.cpp
@@ -33,6 +33,16 @@ class constant_simplification_mockt:public ai_domain_baset
   {}
   void make_entry() override
   {}
+  bool is_bottom() const override
+  {
+    UNREACHABLE;
+    return true;
+  }
+  bool is_top() const override
+  {
+    UNREACHABLE;
+    return true;
+  }
 
   bool ai_simplify(exprt &condition, const namespacet &ns) const override;
 };