@@ -692,6 +692,9 @@ module Make<
692692 * Holds if `e` equals `k` and may be assigned to `v`. The boolean
693693 * `fromBackEdge` indicates whether the flow from `e` to `v` goes through a
694694 * back edge.
695+ *
696+ * This predicate is restricted to cases where all such possible values are
697+ * constants, which means that the `GuardValue`s are singleton values.
695698 */
696699 private predicate possibleValue ( SsaDefinition v , boolean fromBackEdge , Expr e , GuardValue k ) {
697700 not hasPossibleUnknownValue ( v ) and
@@ -711,9 +714,10 @@ module Make<
711714 private predicate uniqueValue ( SsaDefinition v , Expr e , GuardValue k ) {
712715 possibleValue ( v , false , e , k ) and
713716 not possibleValue ( v , true , e , k ) and
714- forex ( Expr other , GuardValue otherval | possibleValue ( v , _, other , otherval ) and other != e |
715- disjointValues ( otherval , k )
716- )
717+ // there's only one expression with the value `k`
718+ 1 = strictcount ( Expr e0 | possibleValue ( v , _, e0 , k ) ) and
719+ // and `v` has at least two possible values
720+ 2 <= strictcount ( GuardValue k0 | possibleValue ( v , _, _, k0 ) )
717721 }
718722
719723 /**
0 commit comments