diff --git a/jbmc/regression/jbmc/must-not-throw-annotation/Test.class b/jbmc/regression/jbmc/must-not-throw-annotation/Test.class
new file mode 100644
index 00000000000..cd2a1c01b96
Binary files /dev/null and b/jbmc/regression/jbmc/must-not-throw-annotation/Test.class differ
diff --git a/jbmc/regression/jbmc/must-not-throw-annotation/Test.java b/jbmc/regression/jbmc/must-not-throw-annotation/Test.java
new file mode 100644
index 00000000000..653efbc5d51
--- /dev/null
+++ b/jbmc/regression/jbmc/must-not-throw-annotation/Test.java
@@ -0,0 +1,17 @@
+public class Test {
+
+  @org.cprover.MustNotThrow
+  public static void mustNotThrow() {
+    throw new RuntimeException("Oh dear");
+  }
+
+  public static void main() {
+    try {
+      mustNotThrow();
+    }
+    catch(Throwable e) {
+      assert false;
+    }
+  }
+
+}
diff --git a/jbmc/regression/jbmc/must-not-throw-annotation/org/cprover/MustNotThrow.class b/jbmc/regression/jbmc/must-not-throw-annotation/org/cprover/MustNotThrow.class
new file mode 100644
index 00000000000..ca862caecb9
Binary files /dev/null and b/jbmc/regression/jbmc/must-not-throw-annotation/org/cprover/MustNotThrow.class differ
diff --git a/jbmc/regression/jbmc/must-not-throw-annotation/org/cprover/MustNotThrow.java b/jbmc/regression/jbmc/must-not-throw-annotation/org/cprover/MustNotThrow.java
new file mode 100644
index 00000000000..ab5edbe35f9
--- /dev/null
+++ b/jbmc/regression/jbmc/must-not-throw-annotation/org/cprover/MustNotThrow.java
@@ -0,0 +1,3 @@
+package org.cprover;
+
+public @interface MustNotThrow { }
diff --git a/jbmc/regression/jbmc/must-not-throw-annotation/test.desc b/jbmc/regression/jbmc/must-not-throw-annotation/test.desc
new file mode 100644
index 00000000000..a39e4029a74
--- /dev/null
+++ b/jbmc/regression/jbmc/must-not-throw-annotation/test.desc
@@ -0,0 +1,8 @@
+CORE
+Test.class
+--function Test.main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
index a6f2996a215..67809f059a7 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -406,6 +406,13 @@ void java_bytecode_convert_method_lazy(
   // Not used in jbmc at present, but other codebases that use jbmc as a library
   // use this information.
   method_symbol.type.set(ID_C_abstract, m.is_abstract);
+
+  if(java_bytecode_parse_treet::find_annotation(
+       m.annotations, "java::org.cprover.MustNotThrow"))
+  {
+    method_symbol.type.set(ID_C_must_not_throw, true);
+  }
+
   symbol_table.add(method_symbol);
 }
 
diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp
index 25ee5b2985c..fb398919736 100644
--- a/jbmc/src/java_bytecode/remove_exceptions.cpp
+++ b/jbmc/src/java_bytecode/remove_exceptions.cpp
@@ -432,19 +432,29 @@ bool remove_exceptionst::instrument_function_call(
 
   if(function_may_throw(callee_id))
   {
-    add_exception_dispatch_sequence(
-      goto_program, instr_it, stack_catch, locals);
-
-    // add a null check (so that instanceof can be applied)
-    equal_exprt eq_null(
+    equal_exprt no_exception_currently_in_flight(
       get_inflight_exception_global(),
       null_pointer_exprt(pointer_type(empty_typet())));
 
-    goto_programt::targett t_null=goto_program.insert_after(instr_it);
-    t_null->make_goto(next_it);
-    t_null->source_location=instr_it->source_location;
-    t_null->function=instr_it->function;
-    t_null->guard=eq_null;
+    if(symbol_table.lookup_ref(callee_id).type.get_bool(ID_C_must_not_throw))
+    {
+      // Function is annotated must-not-throw, but we can't prove that here.
+      // Insert an ASSUME(@inflight_exception == null):
+      goto_programt::targett assume_null = goto_program.insert_after(instr_it);
+      assume_null->make_assumption(no_exception_currently_in_flight);
+    }
+    else
+    {
+      add_exception_dispatch_sequence(
+        goto_program, instr_it, stack_catch, locals);
+
+      // add a null check (so that instanceof can be applied)
+      goto_programt::targett t_null=goto_program.insert_after(instr_it);
+      t_null->make_goto(next_it);
+      t_null->source_location=instr_it->source_location;
+      t_null->function=instr_it->function;
+      t_null->guard=no_exception_currently_in_flight;
+    }
 
     return true;
   }
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index bf10417a60b..99e1374dec5 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -670,6 +670,7 @@ IREP_ID_ONE(bits_per_byte)
 IREP_ID_TWO(C_abstract, #abstract)
 IREP_ID_ONE(synthetic)
 IREP_ID_ONE(interface)
+IREP_ID_TWO(C_must_not_throw, #must_not_throw)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.h in their source tree and