@@ -731,11 +731,9 @@ module LocalFlow {
     or
     node2 = node1.(LocalFunctionCreationNode).getAnAccess(true)
     or
-    node1 =
-      unique(FlowSummaryNode n1 |
-        FlowSummaryImpl::Private::Steps::summaryLocalStep(n1.getSummaryNode(),
-          node2.(FlowSummaryNode).getSummaryNode(), true, _)
-      )
+    FlowSummaryImpl::Private::Steps::summaryLocalMustFlowStep(node1
+          .(FlowSummaryNode)
+          .getSummaryNode(), node2.(FlowSummaryNode).getSummaryNode())
   }
 }
 
 
@@ -160,11 +160,8 @@ predicate localMustFlowStep(Node node1, Node node2) {
   or
   node2.asExpr().(AssignExpr).getSource() = node1.asExpr()
   or
-  node1 =
-    unique(FlowSummaryNode n1 |
-      FlowSummaryImpl::Private::Steps::summaryLocalStep(n1.getSummaryNode(),
-        node2.(FlowSummaryNode).getSummaryNode(), true, _)
-    )
+  FlowSummaryImpl::Private::Steps::summaryLocalMustFlowStep(node1.(FlowSummaryNode).getSummaryNode(),
+    node2.(FlowSummaryNode).getSummaryNode())
 }
 
 import Cached
 
@@ -175,11 +175,9 @@ module LocalFlow {
     or
     node1 = node2.(ImplicitBlockArgumentNode).getParameterNode(true)
     or
-    node1 =
-      unique(FlowSummaryNode n1 |
-        FlowSummaryImpl::Private::Steps::summaryLocalStep(n1.getSummaryNode(),
-          node2.(FlowSummaryNode).getSummaryNode(), true, _)
-      )
+    FlowSummaryImpl::Private::Steps::summaryLocalMustFlowStep(node1
+          .(FlowSummaryNode)
+          .getSummaryNode(), node2.(FlowSummaryNode).getSummaryNode())
   }
 }
 
 
@@ -1030,11 +1030,9 @@ module RustDataFlow implements InputSig<Location> {
   predicate localMustFlowStep(Node node1, Node node2) {
     SsaFlow::localMustFlowStep(_, node1, node2)
     or
-    node1 =
-      unique(Node::FlowSummaryNode n1 |
-        FlowSummaryImpl::Private::Steps::summaryLocalStep(n1.getSummaryNode(),
-          node2.(Node::FlowSummaryNode).getSummaryNode(), true, _)
-      )
+    FlowSummaryImpl::Private::Steps::summaryLocalMustFlowStep(node1
+          .(Node::FlowSummaryNode)
+          .getSummaryNode(), node2.(Node::FlowSummaryNode).getSummaryNode())
   }
 
   class LambdaCallKind = Void;
 
@@ -1207,6 +1207,11 @@ module Make<
         )
       }
 
+      /** Holds if the value of `succ` is uniquely determined by the value of `pred`. */
+      predicate summaryLocalMustFlowStep(SummaryNode pred, SummaryNode succ) {
+        pred = unique(SummaryNode n1 | summaryLocalStep(n1, succ, true, _))
+      }
+
       /**
        * Holds if there is a read step of content `c` from `pred` to `succ`, which
        * is synthesized from a flow summary.
Original file line number	Diff line number	Diff line change
`@@ -731,11 +731,9 @@ module LocalFlow {`
`731`	`731`	`or`
`732`	`732`	`node2 = node1.(LocalFunctionCreationNode).getAnAccess(true)`
`733`	`733`	`or`
`734`		`- node1 =`
`735`		`- unique(FlowSummaryNode n1 \|`
`736`		`- FlowSummaryImpl::Private::Steps::summaryLocalStep(n1.getSummaryNode(),`
`737`		`- node2.(FlowSummaryNode).getSummaryNode(), true, _)`
`738`		`- )`
	`734`	`+ FlowSummaryImpl::Private::Steps::summaryLocalMustFlowStep(node1`
	`735`	`+ .(FlowSummaryNode)`
	`736`	`+ .getSummaryNode(), node2.(FlowSummaryNode).getSummaryNode())`
`739`	`737`	`}`
`740`	`738`	`}`
`741`	`739`
Original file line number	Diff line number	Diff line change
`@@ -175,11 +175,9 @@ module LocalFlow {`
`175`	`175`	`or`
`176`	`176`	`node1 = node2.(ImplicitBlockArgumentNode).getParameterNode(true)`
`177`	`177`	`or`
`178`		`- node1 =`
`179`		`- unique(FlowSummaryNode n1 \|`
`180`		`- FlowSummaryImpl::Private::Steps::summaryLocalStep(n1.getSummaryNode(),`
`181`		`- node2.(FlowSummaryNode).getSummaryNode(), true, _)`
`182`		`- )`
	`178`	`+ FlowSummaryImpl::Private::Steps::summaryLocalMustFlowStep(node1`
	`179`	`+ .(FlowSummaryNode)`
	`180`	`+ .getSummaryNode(), node2.(FlowSummaryNode).getSummaryNode())`
`183`	`181`	`}`
`184`	`182`	`}`
`185`	`183`
Original file line number	Diff line number	Diff line change
`@@ -1207,6 +1207,11 @@ module Make<`
`1207`	`1207`	`)`
`1208`	`1208`	`}`
`1209`	`1209`
	`1210`	+ /** Holds if the value of `succ` is uniquely determined by the value of `pred`. */
	`1211`	`+ predicate summaryLocalMustFlowStep(SummaryNode pred, SummaryNode succ) {`
	`1212`	`+ pred = unique(SummaryNode n1 \| summaryLocalStep(n1, succ, true, _))`
	`1213`	`+ }`
	`1214`	`+`
`1210`	`1215`	`/**`
`1211`	`1216`	* Holds if there is a read step of content `c` from `pred` to `succ`, which
`1212`	`1217`	`* is synthesized from a flow summary.`