diff --git a/regression/cbmc-java/virtual8/A.class b/regression/cbmc-java/virtual8/A.class
new file mode 100644
index 00000000000..680ceb8db5c
Binary files /dev/null and b/regression/cbmc-java/virtual8/A.class differ
diff --git a/regression/cbmc-java/virtual8/B.class b/regression/cbmc-java/virtual8/B.class
new file mode 100644
index 00000000000..06e08d314d8
Binary files /dev/null and b/regression/cbmc-java/virtual8/B.class differ
diff --git a/regression/cbmc-java/virtual8/C.class b/regression/cbmc-java/virtual8/C.class
new file mode 100644
index 00000000000..6391b1ca05c
Binary files /dev/null and b/regression/cbmc-java/virtual8/C.class differ
diff --git a/regression/cbmc-java/virtual8/D.class b/regression/cbmc-java/virtual8/D.class
new file mode 100644
index 00000000000..9cbaf50b562
Binary files /dev/null and b/regression/cbmc-java/virtual8/D.class differ
diff --git a/regression/cbmc-java/virtual8/E.class b/regression/cbmc-java/virtual8/E.class
new file mode 100644
index 00000000000..fcc8898043c
Binary files /dev/null and b/regression/cbmc-java/virtual8/E.class differ
diff --git a/regression/cbmc-java/virtual8/Test.class b/regression/cbmc-java/virtual8/Test.class
new file mode 100644
index 00000000000..f90d0ac64b8
Binary files /dev/null and b/regression/cbmc-java/virtual8/Test.class differ
diff --git a/regression/cbmc-java/virtual8/Test.java b/regression/cbmc-java/virtual8/Test.java
new file mode 100644
index 00000000000..7d5e5b08396
--- /dev/null
+++ b/regression/cbmc-java/virtual8/Test.java
@@ -0,0 +1,29 @@
+public class Test {
+  public static void runF(A x) {
+    x.f();
+  }
+
+  public static void main() {
+    A y = new D();
+    runF(y);
+  }
+}
+
+class A {
+  void f() { }
+}
+
+
+class B extends A {
+  void f() { }
+}
+
+class C extends A {
+  void f() { }
+}
+
+class D extends C {
+}
+
+class E extends B {
+}
diff --git a/regression/cbmc-java/virtual8/test.desc b/regression/cbmc-java/virtual8/test.desc
new file mode 100644
index 00000000000..774005ac03d
--- /dev/null
+++ b/regression/cbmc-java/virtual8/test.desc
@@ -0,0 +1,11 @@
+CORE
+Test.class
+--program-only
+^EXIT=0$
+^SIGNAL=0$
+C\.f
+--
+A\.f
+B\.f
+D\.f
+E\.f
diff --git a/regression/cbmc-java/virtual9/A.class b/regression/cbmc-java/virtual9/A.class
new file mode 100644
index 00000000000..145301d5c90
Binary files /dev/null and b/regression/cbmc-java/virtual9/A.class differ
diff --git a/regression/cbmc-java/virtual9/B.class b/regression/cbmc-java/virtual9/B.class
new file mode 100644
index 00000000000..0b628d311bb
Binary files /dev/null and b/regression/cbmc-java/virtual9/B.class differ
diff --git a/regression/cbmc-java/virtual9/C.class b/regression/cbmc-java/virtual9/C.class
new file mode 100644
index 00000000000..abbca958c2d
Binary files /dev/null and b/regression/cbmc-java/virtual9/C.class differ
diff --git a/regression/cbmc-java/virtual9/D.class b/regression/cbmc-java/virtual9/D.class
new file mode 100644
index 00000000000..31b40172c7a
Binary files /dev/null and b/regression/cbmc-java/virtual9/D.class differ
diff --git a/regression/cbmc-java/virtual9/E.class b/regression/cbmc-java/virtual9/E.class
new file mode 100644
index 00000000000..90b2361dc03
Binary files /dev/null and b/regression/cbmc-java/virtual9/E.class differ
diff --git a/regression/cbmc-java/virtual9/Test.class b/regression/cbmc-java/virtual9/Test.class
new file mode 100644
index 00000000000..eec3a1b0d3e
Binary files /dev/null and b/regression/cbmc-java/virtual9/Test.class differ
diff --git a/regression/cbmc-java/virtual9/Test.java b/regression/cbmc-java/virtual9/Test.java
new file mode 100644
index 00000000000..024d080275b
--- /dev/null
+++ b/regression/cbmc-java/virtual9/Test.java
@@ -0,0 +1,33 @@
+public class Test {
+  public static void runF(A x) {
+    x.f();
+  }
+
+  public static void main(String[] args) {
+    A y = null;
+    if(args.length==3)
+      y = new C();
+    else
+      y = new E();
+    runF(y);
+  }
+}
+
+class A {
+  void f() { }
+}
+
+
+class B extends A {
+  void f() { }
+}
+
+class C extends A {
+  void f() { }
+}
+
+class D extends C {
+}
+
+class E extends B {
+}
diff --git a/regression/cbmc-java/virtual9/test.desc b/regression/cbmc-java/virtual9/test.desc
new file mode 100644
index 00000000000..5ec4ac65fd9
--- /dev/null
+++ b/regression/cbmc-java/virtual9/test.desc
@@ -0,0 +1,13 @@
+KNOWNBUG
+Test.class
+--program-only
+^EXIT=0$
+^SIGNAL=0$
+B\.f
+C\.f
+--
+A\.f
+D\.f
+E\.f
+--
+could be pruned by a value set analysis
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index 995447c1c7e..4d065f6d49b 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -1215,11 +1215,6 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
      (expr.id()==ID_equal || expr.id()==ID_notequal))
     return simplify_inequality_pointer_object(expr);
 
-  // first see if we compare to a constant
-
-  bool op0_is_const=tmp0.is_constant();
-  bool op1_is_const=tmp1.is_constant();
-
   ns.follow_symbol(tmp0.type());
   ns.follow_symbol(tmp1.type());
 
@@ -1229,35 +1224,26 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
   if(tmp1.type().id()==ID_c_enum_tag)
     tmp1.type()=ns.follow_tag(to_c_enum_tag_type(tmp1.type()));
 
+  const auto tmp0_const = expr_try_dynamic_cast<constant_exprt>(tmp0);
+  const auto tmp1_const = expr_try_dynamic_cast<constant_exprt>(tmp1);
+
   // are _both_ constant?
-  if(op0_is_const && op1_is_const)
+  if(tmp0_const && tmp1_const)
   {
-    if(tmp0.type().id()==ID_bool)
+    if(expr.id() == ID_equal || expr.id() == ID_notequal)
     {
-      bool v0=tmp0.is_true();
-      bool v1=tmp1.is_true();
 
-      if(expr.id()==ID_equal)
-      {
-        expr.make_bool(v0==v1);
-        return false;
-      }
-      else if(expr.id()==ID_notequal)
-      {
-        expr.make_bool(v0!=v1);
-        return false;
-      }
+      bool equal = (tmp0_const->get_value() == tmp1_const->get_value());
+      expr.make_bool(expr.id() == ID_equal ? equal : !equal);
+      return false;
     }
-    else if(tmp0.type().id()==ID_fixedbv)
+
+    if(tmp0.type().id() == ID_fixedbv)
     {
       fixedbvt f0(to_constant_expr(tmp0));
       fixedbvt f1(to_constant_expr(tmp1));
 
-      if(expr.id()==ID_notequal)
-        expr.make_bool(f0!=f1);
-      else if(expr.id()==ID_equal)
-        expr.make_bool(f0==f1);
-      else if(expr.id()==ID_ge)
+      if(expr.id() == ID_ge)
         expr.make_bool(f0>=f1);
       else if(expr.id()==ID_le)
         expr.make_bool(f0<=f1);
@@ -1275,11 +1261,7 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
       ieee_floatt f0(to_constant_expr(tmp0));
       ieee_floatt f1(to_constant_expr(tmp1));
 
-      if(expr.id()==ID_notequal)
-        expr.make_bool(f0!=f1);
-      else if(expr.id()==ID_equal)
-        expr.make_bool(f0==f1);
-      else if(expr.id()==ID_ge)
+      if(expr.id() == ID_ge)
         expr.make_bool(f0>=f1);
       else if(expr.id()==ID_le)
         expr.make_bool(f0<=f1);
@@ -1302,11 +1284,7 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
       if(to_rational(tmp1, r1))
         return true;
 
-      if(expr.id()==ID_notequal)
-        expr.make_bool(r0!=r1);
-      else if(expr.id()==ID_equal)
-        expr.make_bool(r0==r1);
-      else if(expr.id()==ID_ge)
+      if(expr.id() == ID_ge)
         expr.make_bool(r0>=r1);
       else if(expr.id()==ID_le)
         expr.make_bool(r0<=r1);
@@ -1329,11 +1307,7 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
       if(to_integer(tmp1, v1))
         return true;
 
-      if(expr.id()==ID_notequal)
-        expr.make_bool(v0!=v1);
-      else if(expr.id()==ID_equal)
-        expr.make_bool(v0==v1);
-      else if(expr.id()==ID_ge)
+      if(expr.id() == ID_ge)
         expr.make_bool(v0>=v1);
       else if(expr.id()==ID_le)
         expr.make_bool(v0<=v1);
@@ -1347,7 +1321,7 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
       return false;
     }
   }
-  else if(op0_is_const)
+  else if(tmp0_const)
   {
     // we want the constant on the RHS
 
@@ -1366,7 +1340,7 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
     simplify_inequality_constant(expr);
     return false;
   }
-  else if(op1_is_const)
+  else if(tmp1_const)
   {
     // one is constant
     return simplify_inequality_constant(expr);