@@ -505,7 +505,8 @@ module Make<
505505 or
506506 exists ( NonNullExpr nonnull |
507507 equalityTestSymmetric ( g1 , g2 , nonnull , v1 .asBooleanValue ( ) ) and
508- v2 .isNonNullValue ( )
508+ v2 .isNonNullValue ( ) and
509+ not g2 instanceof NonNullExpr // disregard trivial guard
509510 )
510511 or
511512 exists ( Case c1 , Expr switchExpr |
@@ -801,13 +802,16 @@ module Make<
801802 }
802803
803804 private predicate impliesStep2 ( Guard g1 , GuardValue v1 , Guard g2 , GuardValue v2 ) {
804- impliesStep1 ( g1 , v1 , g2 , v2 )
805- or
806- exists ( Expr nonnull |
807- exprHasValue ( nonnull , v2 ) and
808- equalityTestSymmetric ( g1 , g2 , nonnull , v1 .asBooleanValue ( ) ) and
809- v2 .isNonNullValue ( )
810- )
805+ (
806+ impliesStep1 ( g1 , v1 , g2 , v2 )
807+ or
808+ exists ( Expr nonnull |
809+ exprHasValue ( nonnull , v2 ) and
810+ equalityTestSymmetric ( g1 , g2 , nonnull , v1 .asBooleanValue ( ) ) and
811+ v2 .isNonNullValue ( )
812+ )
813+ ) and
814+ not exprHasValue ( g2 , v2 ) // disregard trivial guard
811815 }
812816
813817 bindingset [ g1, v1]
0 commit comments