diff --git a/regression/cbmc-java/instanceof8/InstanceOf8.class b/regression/cbmc-java/instanceof8/InstanceOf8.class
new file mode 100644
index 00000000000..24568fd857f
Binary files /dev/null and b/regression/cbmc-java/instanceof8/InstanceOf8.class differ
diff --git a/regression/cbmc-java/instanceof8/InstanceOf8.java b/regression/cbmc-java/instanceof8/InstanceOf8.java
new file mode 100644
index 00000000000..1d5abbf33f0
--- /dev/null
+++ b/regression/cbmc-java/instanceof8/InstanceOf8.java
@@ -0,0 +1,14 @@
+public class InstanceOf8 {
+  public static boolean test(Integer i) {
+    if (i instanceof Integer) {
+      return true;
+    } else {
+      return false;
+    }
+  }
+  public static void main(String[] args)
+  {
+    assert(!test(null));
+    assert(test(new Integer(1)));
+  }
+}
diff --git a/regression/cbmc-java/instanceof8/test.desc b/regression/cbmc-java/instanceof8/test.desc
new file mode 100644
index 00000000000..21d65c684aa
--- /dev/null
+++ b/regression/cbmc-java/instanceof8/test.desc
@@ -0,0 +1,7 @@
+CORE
+InstanceOf8.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
diff --git a/src/goto-programs/remove_instanceof.cpp b/src/goto-programs/remove_instanceof.cpp
index b893c38b0ff..0e0999cf0d0 100644
--- a/src/goto-programs/remove_instanceof.cpp
+++ b/src/goto-programs/remove_instanceof.cpp
@@ -113,7 +113,12 @@ std::size_t remove_instanceoft::lower_instanceof(
   newinst->source_location=this_inst->source_location;
   newinst->function=this_inst->function;
 
-  // Replace the instanceof construct with a big-or.
+  // Replace the instanceof construct with a conjunction of non-null and the
+  // disjunction of all possible object types. According to the Java
+  // specification, null instanceof T is false for all possible values of T.
+  // (http://docs.oracle.com/javase/specs/jls/se7/html/jls-15.html#jls-15.20.2)
+  notequal_exprt non_null_expr(
+    check_ptr, null_pointer_exprt(to_pointer_type(check_ptr.type())));
   exprt::operandst or_ops;
   for(const auto &clsname : children)
   {
@@ -121,7 +126,7 @@ std::size_t remove_instanceoft::lower_instanceof(
     equal_exprt test(newsym.symbol_expr(), clsexpr);
     or_ops.push_back(test);
   }
-  expr=disjunction(or_ops);
+  expr = and_exprt(non_null_expr, disjunction(or_ops));
 
   return 1;
 }