diff --git a/regression/cbmc-java/virtual7/test.desc b/regression/cbmc-java/virtual7/test.desc
index 2e196d82e8c..b35404ac657 100644
--- a/regression/cbmc-java/virtual7/test.desc
+++ b/regression/cbmc-java/virtual7/test.desc
@@ -3,9 +3,9 @@ test.class
 --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$
-IF "java::E".*THEN GOTO [67]
-IF "java::B".*THEN GOTO [67]
-IF "java::D".*THEN GOTO [67]
-IF "java::C".*THEN GOTO [67]
+IF "java::E".*THEN GOTO [12]
+IF "java::B".*THEN GOTO [12]
+IF "java::D".*THEN GOTO [12]
+IF "java::C".*THEN GOTO [12]
 --
 IF "java::A".*THEN GOTO
diff --git a/src/analyses/Makefile b/src/analyses/Makefile
index 690b119e83c..77c7d7f92d0 100644
--- a/src/analyses/Makefile
+++ b/src/analyses/Makefile
@@ -24,6 +24,7 @@ SRC = ai.cpp \
       reaching_definitions.cpp \
       replace_symbol_ext.cpp \
       static_analysis.cpp \
+      uncaught_exceptions_analysis.cpp \
       uninitialized_domain.cpp \
       # Empty last line
 
diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp
new file mode 100644
index 00000000000..814fcaf3730
--- /dev/null
+++ b/src/analyses/uncaught_exceptions_analysis.cpp
@@ -0,0 +1,335 @@
+/*******************************************************************\
+
+Module: Over-approximating uncaught exceptions analysis
+
+Author: Cristina David
+
+\*******************************************************************/
+
+#ifdef DEBUG
+#include <iostream>
+#endif
+#include "uncaught_exceptions_analysis.h"
+
+/*******************************************************************\
+
+Function: get_exception_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Returns the compile type of an exception
+
+\*******************************************************************/
+
+irep_idt uncaught_exceptions_domaint::get_exception_type(const typet &type)
+{
+  assert(type.id()==ID_pointer);
+
+  if(type.subtype().id()==ID_symbol)
+  {
+    return to_symbol_type(type.subtype()).get_identifier();
+  }
+  return ID_empty;
+}
+
+/*******************************************************************\
+
+Function: get_exception_symbol
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Returns the symbol corresponding to an exception
+
+\*******************************************************************/
+
+exprt uncaught_exceptions_domaint::get_exception_symbol(const exprt &expr)
+{
+  if(expr.id()!=ID_symbol && expr.has_operands())
+    return get_exception_symbol(expr.op0());
+
+  return expr;
+}
+
+/*******************************************************************\
+
+Function: uncaught_exceptions_domaint::join
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: The join operator for the uncaught exceptions domain
+
+\*******************************************************************/
+
+void uncaught_exceptions_domaint::join(
+  const irep_idt &element)
+{
+  thrown.insert(element);
+}
+
+void uncaught_exceptions_domaint::join(
+  const std::set<irep_idt> &elements)
+{
+  thrown.insert(elements.begin(), elements.end());
+}
+
+void uncaught_exceptions_domaint::join(
+  const std::vector<irep_idt> &elements)
+{
+  thrown.insert(elements.begin(), elements.end());
+}
+
+
+/*******************************************************************\
+
+Function: uncaught_exceptions_domaint::transform
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: The transformer for the uncaught exceptions domain
+
+\*******************************************************************/
+
+void uncaught_exceptions_domaint::transform(
+  const goto_programt::const_targett from,
+  uncaught_exceptions_analysist &uea,
+  const namespacet &ns)
+{
+  const goto_programt::instructiont &instruction=*from;
+
+  switch(instruction.type)
+  {
+  case THROW:
+  {
+    const exprt &exc_symbol=get_exception_symbol(instruction.code);
+    // retrieve the static type of the thrown exception
+    const irep_idt &type_id=get_exception_type(exc_symbol.type());
+    bool assertion_error=
+      id2string(type_id).find("java.lang.AssertionError")!=std::string::npos;
+    if(!assertion_error)
+    {
+      join(type_id);
+      // we must consider all the subtypes given that
+      // the runtime type is a subtype of the static type
+      std::vector<irep_idt> subtypes=
+        class_hierarchy.get_children_trans(type_id);
+      join(subtypes);
+    }
+    break;
+  }
+  case CATCH:
+  {
+    if(!instruction.code.has_operands())
+    {
+      if(!instruction.targets.empty()) // push
+      {
+        std::set<irep_idt> caught;
+        stack_caught.push_back(caught);
+        std::set<irep_idt> &last_caught=stack_caught.back();
+        const irept::subt &exception_list=
+          instruction.code.find(ID_exception_list).get_sub();
+
+        for(const auto &exc : exception_list)
+        {
+          last_caught.insert(exc.id());
+          std::vector<irep_idt> subtypes=
+            class_hierarchy.get_children_trans(exc.id());
+          last_caught.insert(subtypes.begin(), subtypes.end());
+        }
+      }
+      else // pop
+      {
+        if(!stack_caught.empty())
+        {
+          const std::set<irep_idt> &caught=stack_caught.back();
+          join(caught);
+          // remove the caught exceptions
+          for(const auto &exc_id : caught)
+            thrown.erase(exc_id);
+          stack_caught.pop_back();
+        }
+      }
+    }
+    break;
+  }
+  case FUNCTION_CALL:
+  {
+    const exprt &function_expr=
+      to_code_function_call(instruction.code).function();
+    assert(function_expr.id()==ID_symbol);
+    const irep_idt &function_name=
+      to_symbol_expr(function_expr).get_identifier();
+    // use the current information about the callee
+    join(uea.exceptions_map[function_name]);
+    break;
+  }
+  default:
+  {}
+  }
+}
+
+/*******************************************************************\
+
+Function: uncaught_exceptions_domaint::get_elements
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Returns the value of the private member thrown
+
+\*******************************************************************/
+
+const std::set<irep_idt> &uncaught_exceptions_domaint::get_elements() const
+{
+  return thrown;
+}
+
+/*******************************************************************\
+
+Function: uncaught_exceptions_domaint::operator()
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Constructs the class hierarchy
+
+\*******************************************************************/
+
+void uncaught_exceptions_domaint::operator()(
+  const namespacet &ns)
+{
+  class_hierarchy(ns.get_symbol_table());
+}
+
+/*******************************************************************\
+
+Function: uncaught_exceptions_analysist::collect_uncaught_exceptions
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Runs the uncaught exceptions analysis, which 
+          populates the exceptions map
+
+\*******************************************************************/
+
+void uncaught_exceptions_analysist::collect_uncaught_exceptions(
+  const goto_functionst &goto_functions,
+  const namespacet &ns)
+{
+  bool change=true;
+
+  while(change)
+  {
+    change=false;
+    // add all the functions to the worklist
+    forall_goto_functions(current_function, goto_functions)
+    {
+      domain.make_top();
+      const goto_programt &goto_program=current_function->second.body;
+
+      if(goto_program.empty())
+        continue;
+
+      forall_goto_program_instructions(instr_it, goto_program)
+      {
+        domain.transform(instr_it, *this, ns);
+      }
+      // did our estimation for the current function improve?
+      const std::set<irep_idt> &elements=domain.get_elements();
+      if(exceptions_map[current_function->first].size()<elements.size())
+      {
+        change=true;
+        exceptions_map[current_function->first]=elements;
+      }
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: uncaught_exceptions_analysist::output
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Prints the exceptions map that maps each method to the 
+          set of exceptions that may escape it
+
+\*******************************************************************/
+
+void uncaught_exceptions_analysist::output(
+  const goto_functionst &goto_functions)
+{
+#ifdef DEBUG
+  forall_goto_functions(it, goto_functions)
+  {
+    if(exceptions_map[it->first].size()>0)
+    {
+      std::cout << "Uncaught exceptions in function " <<
+        it->first << ": " << std::endl;
+      assert(exceptions_map.find(it->first)!=exceptions_map.end());
+      for(auto exc_id : exceptions_map[it->first])
+        std::cout << id2string(exc_id) << " ";
+      std::cout << std::endl;
+    }
+  }
+#endif
+}
+
+/*******************************************************************\
+
+Function: uncaught_exceptions_analysist::operator()
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Applies the uncaught exceptions analysis and 
+          outputs the result
+
+\*******************************************************************/
+
+void uncaught_exceptions_analysist::operator()(
+  const goto_functionst &goto_functions,
+  const namespacet &ns,
+  exceptions_mapt &exceptions)
+{
+  domain(ns);
+  collect_uncaught_exceptions(goto_functions, ns);
+  exceptions=exceptions_map;
+  output(goto_functions);
+}
+
+/*******************************************************************\
+
+Function: uncaught_exceptions
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Applies the uncaught exceptions analysis and 
+          outputs the result
+
+\*******************************************************************/
+
+void uncaught_exceptions(
+  const goto_functionst &goto_functions,
+  const namespacet &ns,
+  std::map<irep_idt, std::set<irep_idt>> &exceptions_map)
+{
+  uncaught_exceptions_analysist exceptions;
+  exceptions(goto_functions, ns, exceptions_map);
+}
diff --git a/src/analyses/uncaught_exceptions_analysis.h b/src/analyses/uncaught_exceptions_analysis.h
new file mode 100644
index 00000000000..50ed75b202c
--- /dev/null
+++ b/src/analyses/uncaught_exceptions_analysis.h
@@ -0,0 +1,98 @@
+/*******************************************************************\
+
+Module: Over-approximative uncaught exceptions analysis
+
+Author: Cristina David
+
+\*******************************************************************/
+
+#ifndef CPROVER_ANALYSES_UNCAUGHT_EXCEPTIONS_ANALYSIS_H
+#define CPROVER_ANALYSES_UNCAUGHT_EXCEPTIONS_ANALYSIS_H
+
+#include <algorithm>
+#include <map>
+#include <set>
+#include <goto-programs/goto_functions.h>
+#include <goto-programs/class_hierarchy.h>
+
+/*******************************************************************\
+
+ Class: uncaught_exceptions_domaint
+
+ Purpose: defines the domain used by the uncaught 
+          exceptions analysis
+
+\*******************************************************************/
+
+class uncaught_exceptions_analysist;
+
+class uncaught_exceptions_domaint
+{
+ public:
+  void transform(const goto_programt::const_targett,
+                 uncaught_exceptions_analysist &,
+                 const namespacet &);
+
+  void join(const irep_idt &);
+  void join(const std::set<irep_idt> &);
+  void join(const std::vector<irep_idt> &);
+
+  void make_top()
+  {
+    thrown.clear();
+    stack_caught.clear();
+  }
+
+  static irep_idt get_exception_type(const typet &type);
+
+  static exprt get_exception_symbol(const exprt &exor);
+
+  const std::set<irep_idt>  &get_elements() const;
+
+  void operator()(const namespacet &ns);
+
+ private:
+  typedef std::vector<std::set<irep_idt>> stack_caughtt;
+  stack_caughtt stack_caught;
+  std::set<irep_idt> thrown;
+  class_hierarchyt class_hierarchy;
+};
+
+/*******************************************************************\
+
+ Class: uncaught_exceptions_analysist
+
+ Purpose: computes in exceptions_map an overapproximation of the 
+          exceptions thrown by each method
+
+\*******************************************************************/
+
+class uncaught_exceptions_analysist
+{
+public:
+  typedef std::map<irep_idt, std::set<irep_idt>> exceptions_mapt;
+
+  void collect_uncaught_exceptions(
+    const goto_functionst &,
+    const namespacet &);
+
+  void output(const goto_functionst &);
+
+  void operator()(
+    const goto_functionst &,
+    const namespacet &,
+    exceptions_mapt &);
+
+  friend class uncaught_exceptions_domaint;
+
+ private:
+  uncaught_exceptions_domaint domain;
+  exceptions_mapt exceptions_map;
+};
+
+void uncaught_exceptions(
+  const goto_functionst &,
+  const namespacet &,
+  std::map<irep_idt, std::set<irep_idt>> &);
+
+#endif
diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp
index 5726831804f..de2ab742c07 100644
--- a/src/goto-programs/remove_exceptions.cpp
+++ b/src/goto-programs/remove_exceptions.cpp
@@ -19,6 +19,7 @@ Date:   December 2016
 #include <util/symbol_table.h>
 
 #include "remove_exceptions.h"
+#include <analyses/uncaught_exceptions_analysis.h>
 
 class remove_exceptionst
 {
@@ -27,8 +28,11 @@ class remove_exceptionst
   typedef std::vector<catch_handlerst> stack_catcht;
 
 public:
-  explicit remove_exceptionst(symbol_tablet &_symbol_table):
-    symbol_table(_symbol_table)
+  explicit remove_exceptionst(
+    symbol_tablet &_symbol_table,
+    std::map<irep_idt, std::set<irep_idt>> &_exceptions_map):
+    symbol_table(_symbol_table),
+    exceptions_map(_exceptions_map)
   {
   }
 
@@ -37,6 +41,7 @@ class remove_exceptionst
 
 protected:
   symbol_tablet &symbol_table;
+  std::map<irep_idt, std::set<irep_idt>> &exceptions_map;
 
   void add_exceptional_returns(
     const goto_functionst::function_mapt::iterator &);
@@ -110,47 +115,67 @@ void remove_exceptionst::add_exceptional_returns(
     return;
   }
 
-  // We generate an exceptional return value for any function that has
-  // a throw or a function call. This can be improved by only considering
-  // function calls that may escape exceptions. However, this will
-  // require multiple passes.
-  bool add_exceptional_var=false;
+  // We generate an exceptional return value for any function that
+  // contains a throw or a function call that may escape exceptions.
   forall_goto_program_instructions(instr_it, goto_program)
-    if(instr_it->is_throw() || instr_it->is_function_call())
+  {
+    bool has_uncaught_exceptions=false;
+    if(instr_it->is_function_call())
     {
-      add_exceptional_var=true;
-      break;
+      const exprt &function_expr=
+        to_code_function_call(instr_it->code).function();
+      assert(function_expr.id()==ID_symbol);
+      const irep_idt &function_name=
+        to_symbol_expr(function_expr).get_identifier();
+      has_uncaught_exceptions=!exceptions_map[function_name].empty();
     }
 
-  if(add_exceptional_var)
-  {
-    // look up the function symbol
-    symbol_tablet::symbolst::iterator s_it=
-      symbol_table.symbols.find(function_id);
-
-    assert(s_it!=symbol_table.symbols.end());
-
-    auxiliary_symbolt new_symbol;
-    new_symbol.is_static_lifetime=true;
-    new_symbol.module=function_symbol.module;
-    new_symbol.base_name=id2string(function_symbol.base_name)+EXC_SUFFIX;
-    new_symbol.name=id2string(function_symbol.name)+EXC_SUFFIX;
-    new_symbol.mode=function_symbol.mode;
-    new_symbol.type=typet(ID_pointer, empty_typet());
-    symbol_table.add(new_symbol);
-
-    // initialize the exceptional return with NULL
-    symbol_exprt lhs_expr_null=new_symbol.symbol_expr();
-    null_pointer_exprt rhs_expr_null((pointer_typet(empty_typet())));
-    goto_programt::targett t_null=
-      goto_program.insert_before(goto_program.instructions.begin());
-    t_null->make_assignment();
-    t_null->source_location=
-      goto_program.instructions.begin()->source_location;
-    t_null->code=code_assignt(
-      lhs_expr_null,
-      rhs_expr_null);
-    t_null->function=function_id;
+    bool assertion_error=false;
+    if(instr_it->is_throw())
+    {
+      const exprt &exc =
+        uncaught_exceptions_domaint::get_exception_symbol(instr_it->code);
+      assertion_error =
+        id2string(uncaught_exceptions_domaint::get_exception_type(exc.type())).
+        find("java.lang.AssertionError")!=std::string::npos;
+    }
+
+    // if we find a throw different from AssertionError or a function call
+    // that may escape exceptions, then we add an exceptional return
+    // variable
+    if((instr_it->is_throw() && !assertion_error)
+       || has_uncaught_exceptions)
+    {
+      // look up the function symbol
+      symbol_tablet::symbolst::iterator s_it=
+        symbol_table.symbols.find(function_id);
+
+      assert(s_it!=symbol_table.symbols.end());
+
+      auxiliary_symbolt new_symbol;
+      new_symbol.is_static_lifetime=true;
+      new_symbol.module=function_symbol.module;
+      new_symbol.base_name=id2string(function_symbol.base_name)+EXC_SUFFIX;
+      new_symbol.name=id2string(function_symbol.name)+EXC_SUFFIX;
+      new_symbol.mode=function_symbol.mode;
+      new_symbol.type=typet(ID_pointer, empty_typet());
+      symbol_table.add(new_symbol);
+
+      // initialize the exceptional return with NULL
+      symbol_exprt lhs_expr_null=new_symbol.symbol_expr();
+      null_pointer_exprt rhs_expr_null((pointer_typet(empty_typet())));
+      goto_programt::targett t_null=
+        goto_program.insert_before(goto_program.instructions.begin());
+      t_null->make_assignment();
+      t_null->source_location=
+        goto_program.instructions.begin()->source_location;
+      t_null->code=code_assignt(
+        lhs_expr_null,
+        rhs_expr_null);
+      t_null->function=function_id;
+
+      break;
+    }
   }
 }
 
@@ -264,6 +289,18 @@ void remove_exceptionst::instrument_throw(
 {
   assert(instr_it->type==THROW);
 
+  const exprt &exc_expr=
+    uncaught_exceptions_domaint::get_exception_symbol(instr_it->code);
+  bool assertion_error=id2string(
+    uncaught_exceptions_domaint::get_exception_type(exc_expr.type())).
+    find("java.lang.AssertionError")!=std::string::npos;
+
+  // we don't count AssertionError (we couldn't catch it anyway
+  // and this may reduce the instrumentation considerably if the programmer
+  // used assertions)
+  if(assertion_error)
+    return;
+
   goto_programt &goto_program=func_it->second.body;
   const irep_idt &function_id=func_it->first;
 
@@ -322,11 +359,6 @@ void remove_exceptionst::instrument_throw(
     t_dead->function=instr_it->function;
   }
 
-  // replace "throw x;" by "f#exception_value=x;"
-  exprt exc_expr=instr_it->code;
-  while(exc_expr.id()!=ID_symbol && exc_expr.has_operands())
-    exc_expr=exc_expr.op0();
-
   // add the assignment with the appropriate cast
   code_assignt assignment(typecast_exprt(exc_thrown, exc_expr.type()),
                           exc_expr);
@@ -368,7 +400,8 @@ void remove_exceptionst::instrument_function_call(
   const irep_idt &callee_id=
     to_symbol_expr(function_call.function()).get_identifier();
 
-  if(symbol_table.has_symbol(id2string(callee_id)+EXC_SUFFIX))
+  if(symbol_table.has_symbol(id2string(callee_id)+EXC_SUFFIX) &&
+     symbol_table.has_symbol(id2string(function_id)+EXC_SUFFIX))
   {
     // we may have an escaping exception
     const symbolt &callee_exc_symbol=
@@ -575,7 +608,10 @@ void remove_exceptions(
   symbol_tablet &symbol_table,
   goto_functionst &goto_functions)
 {
-  remove_exceptionst remove_exceptions(symbol_table);
+  const namespacet ns(symbol_table);
+  std::map<irep_idt, std::set<irep_idt>> exceptions_map;
+  uncaught_exceptions(goto_functions, ns, exceptions_map);
+  remove_exceptionst remove_exceptions(symbol_table, exceptions_map);
   remove_exceptions(goto_functions);
 }
 
@@ -593,6 +629,9 @@ Purpose: removes throws/CATCH-POP/CATCH-PUSH
 
 void remove_exceptions(goto_modelt &goto_model)
 {
-  remove_exceptionst remove_exceptions(goto_model.symbol_table);
+  std::map<irep_idt, std::set<irep_idt>> exceptions_map;
+  remove_exceptionst remove_exceptions(
+    goto_model.symbol_table,
+    exceptions_map);
   remove_exceptions(goto_model.goto_functions);
 }