diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 7d7edb8891f..c5228bb270f 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -318,6 +318,9 @@ class goto_symext
     const statet::goto_statet &goto_state,
     statet &dest);
 
+  bool may_assume_unreachable_if_uninitialised(const symbolt &object_symbol)
+    const;
+
   void phi_function(
     const statet::goto_statet &goto_state,
     statet &);
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index e25add14741..3f1218aefa7 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -344,6 +344,14 @@ void goto_symext::merge_value_sets(
   dest.value_set.make_union(src.value_set);
 }
 
+bool goto_symext::may_assume_unreachable_if_uninitialised(
+  const symbolt &object_symbol) const
+{
+  return
+    language_mode == ID_java &&
+    ns.follow(object_symbol.type).id() == ID_struct;
+}
+
 void goto_symext::phi_function(
   const statet::goto_statet &goto_state,
   statet &dest_state)
@@ -424,11 +432,23 @@ void goto_symext::phi_function(
     }
 
     exprt rhs;
+    bool object_unreachable_if_uninitialised =
+      may_assume_unreachable_if_uninitialised(symbol);
 
     if(dest_state.guard.is_false())
       rhs=goto_state_rhs;
     else if(goto_state.guard.is_false())
       rhs=dest_state_rhs;
+    else if(object_unreachable_if_uninitialised &&
+            goto_state.level2_current_count(l1_identifier) == 0)
+    {
+      rhs = dest_state_rhs;
+    }
+    else if(object_unreachable_if_uninitialised &&
+            dest_state.level2.current_count(l1_identifier) == 0)
+    {
+      rhs = goto_state_rhs;
+    }
     else
     {
       rhs=if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs);