--- a/graal/com.oracle.graal.phases.common/src/com/oracle/graal/phases/common/cfs/EquationalReasoner.java	Sun May 04 01:28:07 2014 +0200
+++ b/graal/com.oracle.graal.phases.common/src/com/oracle/graal/phases/common/cfs/EquationalReasoner.java	Sun May 04 14:44:09 2014 +0200
@@ -441,6 +441,8 @@
                 return baseCaseIsNullNode((IsNullNode) condition);
             } else if (condition instanceof ObjectEqualsNode) {
                 return baseCaseObjectEqualsNode((ObjectEqualsNode) condition);
+            } else if (condition instanceof ShortCircuitOrNode) {
+                return baseCaseShortCircuitOrNode((ShortCircuitOrNode) condition);
             }
         }
         return condition;
@@ -515,6 +517,38 @@
     }
 
     /**
+     * The following is tried:
+     *
+     * <ol>
+     * <li>
+     * A {@link com.oracle.graal.phases.common.cfs.Witness} that is at check-cast level level
+     * doesn't entail {@link com.oracle.graal.nodes.calc.IsNullNode} (on its own) nor
+     * {@link com.oracle.graal.nodes.java.InstanceOfNode} (also on its own) but of course it entails
+     * <code>(IsNull || IsInstanceOf)</code>. Good thing
+     * {@link com.oracle.graal.phases.common.cfs.CastCheckExtractor} detects that very pattern.</li>
+     * <li>
+     * Otherwise return the unmodified argument (later on,
+     * {@link #deverbosifyFloatingNode(com.oracle.graal.nodes.calc.FloatingNode)} will attempt to
+     * simplify the {@link com.oracle.graal.nodes.ShortCircuitOrNode}).</li>
+     * </ol>
+     *
+     * @return a {@link com.oracle.graal.nodes.LogicConstantNode}, in case a reduction was made;
+     *         otherwise the unmodified argument.
+     */
+    private LogicNode baseCaseShortCircuitOrNode(ShortCircuitOrNode orNode) {
+        CastCheckExtractor cast = CastCheckExtractor.extract(orNode);
+        if (cast != null) {
+            if (state.knownToConform(cast.subject, cast.type)) {
+                return trueConstant;
+            } else if (state.knownNotToConform(cast.subject, cast.type)) {
+                return falseConstant;
+            }
+            return orNode;
+        }
+        return orNode;
+    }
+
+    /**
      * It's always ok to use "<code>downcast(object)</code>" instead of " <code>object</code>"
      * because this method re-wraps the argument in a {@link com.oracle.graal.nodes.PiNode} only if
      * the new stamp is strictly more refined than the original.

--- a/graal/com.oracle.graal.phases.common/src/com/oracle/graal/phases/common/cfs/State.java	Sun May 04 01:28:07 2014 +0200
+++ b/graal/com.oracle.graal.phases.common/src/com/oracle/graal/phases/common/cfs/State.java	Sun May 04 14:44:09 2014 +0200
@@ -422,7 +422,8 @@
         assert FlowUtil.hasLegalObjectStamp(object);
         assert !to.isPrimitive();
         final ValueNode scrutinee = GraphUtil.unproxify(object);
-        if (isNull(scrutinee)) {
+        if (!isNonNull(scrutinee)) {
+            // unless `null` can be ruled out, a positive answer isn't safe
             return false;
         }
         ResolvedJavaType stampType = StampTool.typeOrNull(object);