@@ -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 |
@@ -797,13 +798,16 @@ module Make<
797798 }
798799
799800 private predicate impliesStep2 ( Guard g1 , GuardValue v1 , Guard g2 , GuardValue v2 ) {
800- impliesStep1 ( g1 , v1 , g2 , v2 )
801- or
802- exists ( Expr nonnull |
803- exprHasValue ( nonnull , v2 ) and
804- equalityTestSymmetric ( g1 , g2 , nonnull , v1 .asBooleanValue ( ) ) and
805- v2 .isNonNullValue ( )
806- )
801+ (
802+ impliesStep1 ( g1 , v1 , g2 , v2 )
803+ or
804+ exists ( Expr nonnull |
805+ exprHasValue ( nonnull , v2 ) and
806+ equalityTestSymmetric ( g1 , g2 , nonnull , v1 .asBooleanValue ( ) ) and
807+ v2 .isNonNullValue ( )
808+ )
809+ ) and
810+ not exprHasValue ( g2 , v2 ) // disregard trivial guard
807811 }
808812
809813 bindingset [ g1, v1]
0 commit comments