diff --git a/config/identical-files.json b/config/identical-files.json
index 9be5c0d0dd2..aabd081ed79 100644
--- a/config/identical-files.json
+++ b/config/identical-files.json
@@ -345,6 +345,10 @@
     "csharp/ql/src/experimental/ir/implementation/raw/gvn/internal/ValueNumberingImports.qll",
     "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/gvn/internal/ValueNumberingImports.qll"
   ],
+  "C# ControlFlowReachability": [
+    "csharp/ql/src/semmle/code/csharp/dataflow/internal/ControlFlowReachability.qll",
+    "csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ControlFlowReachability.qll"
+  ],
   "Inline Test Expectations": [
     "cpp/ql/test/TestUtilities/InlineExpectationsTest.qll",
     "python/ql/test/TestUtilities/InlineExpectationsTest.qll"
diff --git a/csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll b/csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll
index 5ba6486fd7a..b3b36d3d769 100644
--- a/csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll
+++ b/csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll
@@ -310,6 +310,22 @@ module ControlFlow {
       Split getASplit() { result = splits.getASplit() }
     }
 
+    /** A control-flow node for an expression. */
+    class ExprNode extends ElementNode {
+      Expr e;
+
+      ExprNode() { e = unique(Expr e_ | e_ = this.getElement() | e_) }
+
+      /** Gets the expression that this control-flow node belongs to. */
+      Expr getExpr() { result = e }
+
+      /** Gets the value of this expression node, if any. */
+      string getValue() { result = e.getValue() }
+
+      /** Gets the type of this expression node. */
+      Type getType() { result = e.getType() }
+    }
+
     class Split = SplitImpl;
 
     class FinallySplit = FinallySplitting::FinallySplitImpl;
diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/ModulusAnalysis.qll b/csharp/ql/src/semmle/code/csharp/dataflow/ModulusAnalysis.qll
index 2b3c3402415..2964353ce69 100644
--- a/csharp/ql/src/semmle/code/csharp/dataflow/ModulusAnalysis.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/ModulusAnalysis.qll
@@ -111,18 +111,6 @@ private predicate evenlyDivisibleExpr(Expr e, int factor) {
   )
 }
 
-/**
- * Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
- * in an arbitrary 1-based numbering of the input edges to `phi`.
- */
-private predicate rankedPhiInput(
-  SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r
-) {
-  edge.phiInput(phi, inp) and
-  edge =
-    rank[r](SsaReadPositionPhiInputEdge e | e.phiInput(phi, _) | e order by getId(e.getOrigBlock()))
-}
-
 /**
  * Holds if `rix` is the number of input edges to `phi`.
  */
diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/SignAnalysis.qll b/csharp/ql/src/semmle/code/csharp/dataflow/SignAnalysis.qll
index 3742f87de25..6f6f38bd199 100644
--- a/csharp/ql/src/semmle/code/csharp/dataflow/SignAnalysis.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/SignAnalysis.qll
@@ -6,4 +6,41 @@
  * three-valued domain `{negative, zero, positive}`.
  */
 
-import semmle.code.csharp.dataflow.internal.rangeanalysis.SignAnalysisCommon
+import csharp
+private import semmle.code.csharp.dataflow.internal.rangeanalysis.SignAnalysisCommon as Common
+
+/** Holds if `e` can be positive and cannot be negative. */
+predicate positiveExpr(Expr e) {
+  forex(ControlFlow::Node cfn | cfn = e.getAControlFlowNode() |
+    positive(cfn) or strictlyPositive(cfn)
+  )
+}
+
+/** Holds if `e` can be negative and cannot be positive. */
+predicate negativeExpr(Expr e) {
+  forex(ControlFlow::Node cfn | cfn = e.getAControlFlowNode() |
+    negative(cfn) or strictlyNegative(cfn)
+  )
+}
+
+/** Holds if `e` is strictly positive. */
+predicate strictlyPositiveExpr(Expr e) {
+  forex(ControlFlow::Node cfn | cfn = e.getAControlFlowNode() | strictlyPositive(cfn))
+}
+
+/** Holds if `e` is strictly negative. */
+predicate strictlyNegativeExpr(Expr e) {
+  forex(ControlFlow::Node cfn | cfn = e.getAControlFlowNode() | strictlyNegative(cfn))
+}
+
+/** Holds if `e` can be positive and cannot be negative. */
+predicate positive(ControlFlow::Nodes::ExprNode e) { Common::positive(e) }
+
+/** Holds if `e` can be negative and cannot be positive. */
+predicate negative(ControlFlow::Nodes::ExprNode e) { Common::negative(e) }
+
+/** Holds if `e` is strictly positive. */
+predicate strictlyPositive(ControlFlow::Nodes::ExprNode e) { Common::strictlyPositive(e) }
+
+/** Holds if `e` is strictly negative. */
+predicate strictlyNegative(ControlFlow::Nodes::ExprNode e) { Common::strictlyNegative(e) }
diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/ControlFlowReachability.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/ControlFlowReachability.qll
index 9c2cbabcd61..b8eaa2310d8 100644
--- a/csharp/ql/src/semmle/code/csharp/dataflow/internal/ControlFlowReachability.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/ControlFlowReachability.qll
@@ -1,6 +1,4 @@
 import csharp
-private import DataFlowPrivate
-private import DataFlowPublic
 
 private class ControlFlowScope extends ControlFlowElement {
   private boolean exactScope;
@@ -89,21 +87,21 @@ abstract class ControlFlowReachabilityConfiguration extends string {
 
   pragma[nomagic]
   private predicate reachesBasicBlockExprBase(
-    Expr e1, Expr e2, ControlFlowElement scope, boolean exactScope, boolean isSuccessor,
-    ControlFlow::Nodes::ElementNode cfn1, int i, ControlFlow::BasicBlock bb
+    Expr e1, Expr e2, boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn1, int i,
+    ControlFlow::BasicBlock bb
   ) {
-    this.candidate(e1, e2, scope, exactScope, isSuccessor) and
+    this.candidate(e1, e2, _, _, isSuccessor) and
     cfn1 = e1.getAControlFlowNode() and
     bb.getNode(i) = cfn1
   }
 
   pragma[nomagic]
   private predicate reachesBasicBlockExprRec(
-    Expr e1, Expr e2, ControlFlowElement scope, boolean exactScope, boolean isSuccessor,
-    ControlFlow::Nodes::ElementNode cfn1, ControlFlow::BasicBlock bb
+    Expr e1, Expr e2, boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn1,
+    ControlFlow::BasicBlock bb
   ) {
     exists(ControlFlow::BasicBlock mid |
-      this.reachesBasicBlockExpr(e1, e2, scope, exactScope, isSuccessor, cfn1, mid)
+      this.reachesBasicBlockExpr(e1, e2, isSuccessor, cfn1, mid)
     |
       isSuccessor = true and
       bb = mid.getASuccessor()
@@ -115,36 +113,35 @@ abstract class ControlFlowReachabilityConfiguration extends string {
 
   pragma[nomagic]
   private predicate reachesBasicBlockExpr(
-    Expr e1, Expr e2, ControlFlowElement scope, boolean exactScope, boolean isSuccessor,
-    ControlFlow::Nodes::ElementNode cfn1, ControlFlow::BasicBlock bb
+    Expr e1, Expr e2, boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn1,
+    ControlFlow::BasicBlock bb
   ) {
-    this.reachesBasicBlockExprBase(e1, e2, scope, exactScope, isSuccessor, cfn1, _, bb)
+    this.reachesBasicBlockExprBase(e1, e2, isSuccessor, cfn1, _, bb)
     or
-    this.candidate(e1, e2, scope, exactScope, isSuccessor) and
-    exists(ControlFlowElement scope0, boolean exactScope0 |
-      this.reachesBasicBlockExprRec(e1, e2, scope0, exactScope0, isSuccessor, cfn1, bb)
-    |
-      bb = getABasicBlockInScope(scope0, exactScope0)
+    exists(ControlFlowElement scope, boolean exactScope |
+      this.candidate(e1, e2, scope, exactScope, isSuccessor) and
+      this.reachesBasicBlockExprRec(e1, e2, isSuccessor, cfn1, bb) and
+      bb = getABasicBlockInScope(scope, exactScope)
     )
   }
 
   pragma[nomagic]
   private predicate reachesBasicBlockDefinitionBase(
-    Expr e, AssignableDefinition def, ControlFlowElement scope, boolean exactScope,
-    boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn, int i, ControlFlow::BasicBlock bb
+    Expr e, AssignableDefinition def, boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn,
+    int i, ControlFlow::BasicBlock bb
   ) {
-    this.candidateDef(e, def, scope, exactScope, isSuccessor) and
+    this.candidateDef(e, def, _, _, isSuccessor) and
     cfn = e.getAControlFlowNode() and
     bb.getNode(i) = cfn
   }
 
   pragma[nomagic]
   private predicate reachesBasicBlockDefinitionRec(
-    Expr e, AssignableDefinition def, ControlFlowElement scope, boolean exactScope,
-    boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn, ControlFlow::BasicBlock bb
+    Expr e, AssignableDefinition def, boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn,
+    ControlFlow::BasicBlock bb
   ) {
     exists(ControlFlow::BasicBlock mid |
-      this.reachesBasicBlockDefinition(e, def, scope, exactScope, isSuccessor, cfn, mid)
+      this.reachesBasicBlockDefinition(e, def, isSuccessor, cfn, mid)
     |
       isSuccessor = true and
       bb = mid.getASuccessor()
@@ -156,16 +153,15 @@ abstract class ControlFlowReachabilityConfiguration extends string {
 
   pragma[nomagic]
   private predicate reachesBasicBlockDefinition(
-    Expr e, AssignableDefinition def, ControlFlowElement scope, boolean exactScope,
-    boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn, ControlFlow::BasicBlock bb
+    Expr e, AssignableDefinition def, boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn,
+    ControlFlow::BasicBlock bb
   ) {
-    this.reachesBasicBlockDefinitionBase(e, def, scope, exactScope, isSuccessor, cfn, _, bb)
+    this.reachesBasicBlockDefinitionBase(e, def, isSuccessor, cfn, _, bb)
     or
-    this.candidateDef(e, def, scope, exactScope, isSuccessor) and
-    exists(ControlFlowElement scope0, boolean exactScope0 |
-      this.reachesBasicBlockDefinitionRec(e, def, scope0, exactScope0, isSuccessor, cfn, bb)
-    |
-      bb = getABasicBlockInScope(scope0, exactScope0)
+    exists(ControlFlowElement scope, boolean exactScope |
+      this.candidateDef(e, def, scope, exactScope, isSuccessor) and
+      this.reachesBasicBlockDefinitionRec(e, def, isSuccessor, cfn, bb) and
+      bb = getABasicBlockInScope(scope, exactScope)
     )
   }
 
@@ -176,7 +172,7 @@ abstract class ControlFlowReachabilityConfiguration extends string {
   pragma[nomagic]
   predicate hasExprPath(Expr e1, ControlFlow::Node cfn1, Expr e2, ControlFlow::Node cfn2) {
     exists(ControlFlow::BasicBlock bb, boolean isSuccessor, int i, int j |
-      this.reachesBasicBlockExprBase(e1, e2, _, _, isSuccessor, cfn1, i, bb) and
+      this.reachesBasicBlockExprBase(e1, e2, isSuccessor, cfn1, i, bb) and
       cfn2 = bb.getNode(j) and
       cfn2 = e2.getAControlFlowNode()
     |
@@ -186,7 +182,7 @@ abstract class ControlFlowReachabilityConfiguration extends string {
     )
     or
     exists(ControlFlow::BasicBlock bb |
-      this.reachesBasicBlockExprRec(e1, e2, _, _, _, cfn1, bb) and
+      this.reachesBasicBlockExprRec(e1, e2, _, cfn1, bb) and
       cfn2 = bb.getANode() and
       cfn2 = e2.getAControlFlowNode()
     )
@@ -201,7 +197,7 @@ abstract class ControlFlowReachabilityConfiguration extends string {
     Expr e, ControlFlow::Node cfn, AssignableDefinition def, ControlFlow::Node cfnDef
   ) {
     exists(ControlFlow::BasicBlock bb, boolean isSuccessor, int i, int j |
-      this.reachesBasicBlockDefinitionBase(e, def, _, _, isSuccessor, cfn, i, bb) and
+      this.reachesBasicBlockDefinitionBase(e, def, isSuccessor, cfn, i, bb) and
       cfnDef = bb.getNode(j) and
       def.getAControlFlowNode() = cfnDef
     |
@@ -211,35 +207,9 @@ abstract class ControlFlowReachabilityConfiguration extends string {
     )
     or
     exists(ControlFlow::BasicBlock bb |
-      this.reachesBasicBlockDefinitionRec(e, def, _, _, _, cfn, bb) and
+      this.reachesBasicBlockDefinitionRec(e, def, _, cfn, bb) and
       def.getAControlFlowNode() = cfnDef and
       cfnDef = bb.getANode()
     )
   }
-
-  /**
-   * Holds if there is a control-flow path from `n1` to `n2`. `n2` is either an
-   * expression node or an SSA definition node.
-   */
-  pragma[nomagic]
-  predicate hasNodePath(ExprNode n1, Node n2) {
-    exists(Expr e1, ControlFlow::Node cfn1, Expr e2, ControlFlow::Node cfn2 |
-      this.hasExprPath(e1, cfn1, e2, cfn2)
-    |
-      cfn1 = n1.getControlFlowNode() and
-      cfn2 = n2.(ExprNode).getControlFlowNode()
-    )
-    or
-    exists(
-      Expr e, ControlFlow::Node cfn, AssignableDefinition def, ControlFlow::Node cfnDef,
-      Ssa::ExplicitDefinition ssaDef
-    |
-      this.hasDefPath(e, cfn, def, cfnDef)
-    |
-      cfn = n1.getControlFlowNode() and
-      ssaDef.getADefinition() = def and
-      ssaDef.getControlFlowNode() = cfnDef and
-      n2.(SsaDefinitionNode).getDefinition() = ssaDef
-    )
-  }
 }
diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowPrivate.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowPrivate.qll
index bae73a6609d..1acfe13d53e 100644
--- a/csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowPrivate.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowPrivate.qll
@@ -122,6 +122,32 @@ private module ThisFlow {
   }
 }
 
+/**
+ * Holds if there is a control-flow path from `n1` to `n2`. `n2` is either an
+ * expression node or an SSA definition node.
+ */
+pragma[nomagic]
+predicate hasNodePath(ControlFlowReachabilityConfiguration conf, ExprNode n1, Node n2) {
+  exists(Expr e1, ControlFlow::Node cfn1, Expr e2, ControlFlow::Node cfn2 |
+    conf.hasExprPath(e1, cfn1, e2, cfn2)
+  |
+    cfn1 = n1.getControlFlowNode() and
+    cfn2 = n2.(ExprNode).getControlFlowNode()
+  )
+  or
+  exists(
+    Expr e, ControlFlow::Node cfn, AssignableDefinition def, ControlFlow::Node cfnDef,
+    Ssa::ExplicitDefinition ssaDef
+  |
+    conf.hasDefPath(e, cfn, def, cfnDef)
+  |
+    cfn = n1.getControlFlowNode() and
+    ssaDef.getADefinition() = def and
+    ssaDef.getControlFlowNode() = cfnDef and
+    n2.(SsaDefinitionNode).getDefinition() = ssaDef
+  )
+}
+
 /** Provides predicates related to local data flow. */
 module LocalFlow {
   private class LocalExprStepConfiguration extends ControlFlowReachabilityConfiguration {
@@ -307,7 +333,7 @@ module LocalFlow {
       not usesInstanceField(def)
     )
     or
-    any(LocalExprStepConfiguration x).hasNodePath(nodeFrom, nodeTo)
+    hasNodePath(any(LocalExprStepConfiguration x), nodeFrom, nodeTo)
     or
     ThisFlow::adjacentThisRefs(nodeFrom, nodeTo)
     or
@@ -669,7 +695,7 @@ private module Cached {
   cached
   predicate storeStepImpl(Node node1, Content c, Node node2) {
     exists(StoreStepConfiguration x, ExprNode node, boolean postUpdate |
-      x.hasNodePath(node1, node) and
+      hasNodePath(x, node1, node) and
       if postUpdate = true then node = node2.(PostUpdateNode).getPreUpdateNode() else node = node2
     |
       fieldOrPropertyStore(_, c, node1.asExpr(), node.getExpr(), postUpdate)
@@ -704,10 +730,10 @@ private module Cached {
   cached
   predicate readStepImpl(Node node1, Content c, Node node2) {
     exists(ReadStepConfiguration x |
-      x.hasNodePath(node1, node2) and
+      hasNodePath(x, node1, node2) and
       fieldOrPropertyRead(node1.asExpr(), c, node2.asExpr())
       or
-      x.hasNodePath(node1, node2) and
+      hasNodePath(x, node1, node2) and
       arrayRead(node1.asExpr(), node2.asExpr()) and
       c instanceof ElementContent
       or
@@ -719,7 +745,7 @@ private module Cached {
         c instanceof ElementContent
       )
       or
-      x.hasNodePath(node1, node2) and
+      hasNodePath(x, node1, node2) and
       node2.asExpr().(AwaitExpr).getExpr() = node1.asExpr() and
       c = getResultContent()
     )
diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/TaintTrackingPrivate.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/TaintTrackingPrivate.qll
index 68284e965fa..1a1fdf5355e 100755
--- a/csharp/ql/src/semmle/code/csharp/dataflow/internal/TaintTrackingPrivate.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/TaintTrackingPrivate.qll
@@ -105,7 +105,7 @@ private class LocalTaintExprStepConfiguration extends ControlFlowReachabilityCon
 
 private predicate localTaintStepCommon(DataFlow::Node nodeFrom, DataFlow::Node nodeTo) {
   Stages::DataFlowStage::forceCachingInSameStage() and
-  any(LocalTaintExprStepConfiguration x).hasNodePath(nodeFrom, nodeTo)
+  hasNodePath(any(LocalTaintExprStepConfiguration x), nodeFrom, nodeTo)
   or
   localTaintStepCil(nodeFrom, nodeTo)
 }
diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/BoundSpecific.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/BoundSpecific.qll
index edf437e919c..3515f2f96c8 100644
--- a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/BoundSpecific.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/BoundSpecific.qll
@@ -5,17 +5,16 @@
 private import csharp as CS
 private import semmle.code.csharp.dataflow.SSA::Ssa as Ssa
 private import semmle.code.csharp.dataflow.internal.rangeanalysis.ConstantUtils as CU
+private import semmle.code.csharp.dataflow.internal.rangeanalysis.RangeUtils as RU
+private import semmle.code.csharp.dataflow.internal.rangeanalysis.SsaUtils as SU
 
-class SsaVariable extends Ssa::Definition {
-  /** Gets a read of the source variable underlying this SSA definition. */
-  Expr getAUse() { result = getARead() }
-}
+class SsaVariable = SU::SsaVariable;
 
-class Expr = CS::Expr;
+class Expr = CS::ControlFlow::Nodes::ExprNode;
 
 class IntegralType = CS::IntegralType;
 
 class ConstantIntegerExpr = CU::ConstantIntegerExpr;
 
 /** Holds if `e` is a bound expression and it is not an SSA variable read. */
-predicate interestingExprBound(Expr e) { CU::systemArrayLengthAccess(e.(CS::PropertyRead)) }
+predicate interestingExprBound(Expr e) { CU::systemArrayLengthAccess(e.getExpr()) }
diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ConstantUtils.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ConstantUtils.qll
index 08b64321a38..c067e29d320 100644
--- a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ConstantUtils.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ConstantUtils.qll
@@ -4,18 +4,10 @@
 
 private import csharp
 private import Ssa
+private import SsaUtils
+private import RangeUtils
 
-/**
- * Holds if property `p` matches `property` in `baseClass` or any overrides.
- */
-predicate propertyOverrides(Property p, string baseClass, string property) {
-  exists(Property p2 |
-    p2.getSourceDeclaration().getDeclaringType().hasQualifiedName(baseClass) and
-    p2.hasName(property)
-  |
-    p.overridesOrImplementsOrEquals(p2)
-  )
-}
+private class ExprNode = ControlFlow::Nodes::ExprNode;
 
 /**
  * Holds if `pa` is an access to the `Length` property of an array.
@@ -30,40 +22,42 @@ predicate systemArrayLengthAccess(PropertyAccess pa) {
  * - a read of a compile time constant with integer value `val`, or
  * - a read of the `Length` of an array with `val` lengths.
  */
-private predicate constantIntegerExpr(Expr e, int val) {
+private predicate constantIntegerExpr(ExprNode e, int val) {
   e.getValue().toInt() = val
   or
-  exists(ExplicitDefinition v, Expr src |
-    e = v.getARead() and
-    src = v.getADefinition().getSource() and
+  exists(ExprNode src |
+    e = getAnExplicitDefinitionRead(src) and
     constantIntegerExpr(src, val)
   )
   or
   isArrayLengthAccess(e, val)
 }
 
-private int getArrayLength(ArrayCreation arrCreation, int index) {
-  constantIntegerExpr(arrCreation.getLengthArgument(index), result)
+private int getArrayLength(ExprNode e, int index) {
+  exists(ArrayCreation arrCreation, ExprNode length |
+    hasChild(arrCreation, arrCreation.getLengthArgument(index), e, length) and
+    constantIntegerExpr(length, result)
+  )
 }
 
-private int getArrayLengthRec(ArrayCreation arrCreation, int index) {
+private int getArrayLengthRec(ExprNode arrCreation, int index) {
   index = 0 and result = getArrayLength(arrCreation, 0)
   or
   index > 0 and
   result = getArrayLength(arrCreation, index) * getArrayLengthRec(arrCreation, index - 1)
 }
 
-private predicate isArrayLengthAccess(PropertyAccess pa, int length) {
-  systemArrayLengthAccess(pa) and
-  exists(ExplicitDefinition arr, ArrayCreation arrCreation |
-    getArrayLengthRec(arrCreation, arrCreation.getNumberOfLengthArguments() - 1) = length and
-    arrCreation = arr.getADefinition().getSource() and
-    pa.getQualifier() = arr.getARead()
+private predicate isArrayLengthAccess(ExprNode e, int length) {
+  exists(PropertyAccess pa, ExprNode arrCreation |
+    systemArrayLengthAccess(pa) and
+    getArrayLengthRec(arrCreation,
+      arrCreation.getExpr().(ArrayCreation).getNumberOfLengthArguments() - 1) = length and
+    hasChild(pa, pa.getQualifier(), e, getAnExplicitDefinitionRead(arrCreation))
   )
 }
 
 /** An expression that always has the same integer value. */
-class ConstantIntegerExpr extends Expr {
+class ConstantIntegerExpr extends ExprNode {
   ConstantIntegerExpr() { constantIntegerExpr(this, _) }
 
   /** Gets the integer value of this expression. */
diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ControlFlowReachability.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ControlFlowReachability.qll
new file mode 100644
index 00000000000..b8eaa2310d8
--- /dev/null
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ControlFlowReachability.qll
@@ -0,0 +1,215 @@
+import csharp
+
+private class ControlFlowScope extends ControlFlowElement {
+  private boolean exactScope;
+
+  ControlFlowScope() {
+    exists(ControlFlowReachabilityConfiguration c |
+      c.candidate(_, _, this, exactScope, _) or
+      c.candidateDef(_, _, this, exactScope, _)
+    )
+  }
+
+  predicate isExact() { exactScope = true }
+
+  predicate isNonExact() { exactScope = false }
+}
+
+private ControlFlowElement getANonExactScopeChild(ControlFlowScope scope) {
+  scope.isNonExact() and
+  result = scope
+  or
+  result = getANonExactScopeChild(scope).getAChild()
+}
+
+pragma[noinline]
+private ControlFlow::BasicBlock getABasicBlockInScope(ControlFlowScope scope, boolean exactScope) {
+  result.getANode().getElement() = getANonExactScopeChild(scope) and
+  exactScope = false
+  or
+  scope.isExact() and
+  result.getANode().getElement() = scope and
+  exactScope = true
+}
+
+/**
+ * A helper class for determining control-flow reachability for pairs of
+ * elements.
+ *
+ * This is useful when defining for example expression-based data-flow steps in
+ * the presence of control-flow splitting, where a data-flow step should make
+ * sure to stay in the same split.
+ *
+ * For example, in
+ *
+ * ```csharp
+ * if (b)
+ *     ....
+ * var x = "foo";
+ * if (b)
+ *     ....
+ * ```
+ *
+ * there should only be steps from `[b = true] "foo"` to `[b = true] SSA def(x)`
+ * and `[b = false] "foo"` to `[b = false] SSA def(x)`, and for example not from
+ * `[b = true] "foo"` to `[b = false] SSA def(x)`
+ */
+abstract class ControlFlowReachabilityConfiguration extends string {
+  bindingset[this]
+  ControlFlowReachabilityConfiguration() { any() }
+
+  /**
+   * Holds if `e1` and `e2` are expressions for which we want to find a
+   * control-flow path that follows control flow successors (resp.
+   * predecessors, as specified by `isSuccesor`) inside the syntactic scope
+   * `scope`. The Boolean `exactScope` indicates whether a transitive child
+   * of `scope` is allowed (`exactScope = false`).
+   */
+  predicate candidate(
+    Expr e1, Expr e2, ControlFlowElement scope, boolean exactScope, boolean isSuccessor
+  ) {
+    none()
+  }
+
+  /**
+   * Holds if `e` and `def` are elements for which we want to find a
+   * control-flow path that follows control flow successors (resp.
+   * predecessors, as specified by `isSuccesor`) inside the syntactic scope
+   * `scope`. The Boolean `exactScope` indicates whether a transitive child
+   * of `scope` is allowed (`exactScope = false`).
+   */
+  predicate candidateDef(
+    Expr e, AssignableDefinition def, ControlFlowElement scope, boolean exactScope,
+    boolean isSuccessor
+  ) {
+    none()
+  }
+
+  pragma[nomagic]
+  private predicate reachesBasicBlockExprBase(
+    Expr e1, Expr e2, boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn1, int i,
+    ControlFlow::BasicBlock bb
+  ) {
+    this.candidate(e1, e2, _, _, isSuccessor) and
+    cfn1 = e1.getAControlFlowNode() and
+    bb.getNode(i) = cfn1
+  }
+
+  pragma[nomagic]
+  private predicate reachesBasicBlockExprRec(
+    Expr e1, Expr e2, boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn1,
+    ControlFlow::BasicBlock bb
+  ) {
+    exists(ControlFlow::BasicBlock mid |
+      this.reachesBasicBlockExpr(e1, e2, isSuccessor, cfn1, mid)
+    |
+      isSuccessor = true and
+      bb = mid.getASuccessor()
+      or
+      isSuccessor = false and
+      bb = mid.getAPredecessor()
+    )
+  }
+
+  pragma[nomagic]
+  private predicate reachesBasicBlockExpr(
+    Expr e1, Expr e2, boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn1,
+    ControlFlow::BasicBlock bb
+  ) {
+    this.reachesBasicBlockExprBase(e1, e2, isSuccessor, cfn1, _, bb)
+    or
+    exists(ControlFlowElement scope, boolean exactScope |
+      this.candidate(e1, e2, scope, exactScope, isSuccessor) and
+      this.reachesBasicBlockExprRec(e1, e2, isSuccessor, cfn1, bb) and
+      bb = getABasicBlockInScope(scope, exactScope)
+    )
+  }
+
+  pragma[nomagic]
+  private predicate reachesBasicBlockDefinitionBase(
+    Expr e, AssignableDefinition def, boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn,
+    int i, ControlFlow::BasicBlock bb
+  ) {
+    this.candidateDef(e, def, _, _, isSuccessor) and
+    cfn = e.getAControlFlowNode() and
+    bb.getNode(i) = cfn
+  }
+
+  pragma[nomagic]
+  private predicate reachesBasicBlockDefinitionRec(
+    Expr e, AssignableDefinition def, boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn,
+    ControlFlow::BasicBlock bb
+  ) {
+    exists(ControlFlow::BasicBlock mid |
+      this.reachesBasicBlockDefinition(e, def, isSuccessor, cfn, mid)
+    |
+      isSuccessor = true and
+      bb = mid.getASuccessor()
+      or
+      isSuccessor = false and
+      bb = mid.getAPredecessor()
+    )
+  }
+
+  pragma[nomagic]
+  private predicate reachesBasicBlockDefinition(
+    Expr e, AssignableDefinition def, boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn,
+    ControlFlow::BasicBlock bb
+  ) {
+    this.reachesBasicBlockDefinitionBase(e, def, isSuccessor, cfn, _, bb)
+    or
+    exists(ControlFlowElement scope, boolean exactScope |
+      this.candidateDef(e, def, scope, exactScope, isSuccessor) and
+      this.reachesBasicBlockDefinitionRec(e, def, isSuccessor, cfn, bb) and
+      bb = getABasicBlockInScope(scope, exactScope)
+    )
+  }
+
+  /**
+   * Holds if there is a control-flow path from `cfn1` to `cfn2`, where `cfn1` is a
+   * control-flow node for `e1` and `cfn2` is a control-flow node for `e2`.
+   */
+  pragma[nomagic]
+  predicate hasExprPath(Expr e1, ControlFlow::Node cfn1, Expr e2, ControlFlow::Node cfn2) {
+    exists(ControlFlow::BasicBlock bb, boolean isSuccessor, int i, int j |
+      this.reachesBasicBlockExprBase(e1, e2, isSuccessor, cfn1, i, bb) and
+      cfn2 = bb.getNode(j) and
+      cfn2 = e2.getAControlFlowNode()
+    |
+      isSuccessor = true and j >= i
+      or
+      isSuccessor = false and i >= j
+    )
+    or
+    exists(ControlFlow::BasicBlock bb |
+      this.reachesBasicBlockExprRec(e1, e2, _, cfn1, bb) and
+      cfn2 = bb.getANode() and
+      cfn2 = e2.getAControlFlowNode()
+    )
+  }
+
+  /**
+   * Holds if there is a control-flow path from `cfn` to `cfnDef`, where `cfn` is a
+   * control-flow node for `e` and `cfnDef` is a control-flow node for `def`.
+   */
+  pragma[nomagic]
+  predicate hasDefPath(
+    Expr e, ControlFlow::Node cfn, AssignableDefinition def, ControlFlow::Node cfnDef
+  ) {
+    exists(ControlFlow::BasicBlock bb, boolean isSuccessor, int i, int j |
+      this.reachesBasicBlockDefinitionBase(e, def, isSuccessor, cfn, i, bb) and
+      cfnDef = bb.getNode(j) and
+      def.getAControlFlowNode() = cfnDef
+    |
+      isSuccessor = true and j >= i
+      or
+      isSuccessor = false and i >= j
+    )
+    or
+    exists(ControlFlow::BasicBlock bb |
+      this.reachesBasicBlockDefinitionRec(e, def, _, cfn, bb) and
+      def.getAControlFlowNode() = cfnDef and
+      cfnDef = bb.getANode()
+    )
+  }
+}
diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
index 2cdbfbf65f4..380bbe59485 100644
--- a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
@@ -1,98 +1,39 @@
 module Private {
   private import csharp as CS
   private import ConstantUtils as CU
-  private import semmle.code.csharp.controlflow.Guards as G
   private import semmle.code.csharp.dataflow.internal.rangeanalysis.RangeUtils as RU
   private import SsaUtils as SU
-  private import SignAnalysisSpecific::Private as SA
+  private import SsaReadPositionCommon
 
   class BasicBlock = CS::Ssa::BasicBlock;
 
-  class SsaVariable extends CS::Ssa::Definition {
-    CS::AssignableRead getAUse() { result = this.getARead() }
-  }
+  class SsaVariable = SU::SsaVariable;
 
   class SsaPhiNode = CS::Ssa::PhiNode;
 
-  class Expr = CS::Expr;
+  class Expr = CS::ControlFlow::Nodes::ExprNode;
 
-  class Guard = G::Guard;
+  class Guard = RU::Guard;
 
   class ConstantIntegerExpr = CU::ConstantIntegerExpr;
 
-  class ConditionalExpr extends CS::ConditionalExpr {
-    /** Gets the "then" expression of this conditional expression. */
-    Expr getTrueExpr() { result = this.getThen() }
+  class ConditionalExpr = RU::ExprNode::ConditionalExpr;
 
-    /** Gets the "else" expression of this conditional expression. */
-    Expr getFalseExpr() { result = this.getElse() }
-  }
+  class AddExpr = RU::ExprNode::AddExpr;
 
-  /** Represent an addition expression. */
-  class AddExpr extends CS::AddExpr {
-    /** Gets the LHS operand of this add expression. */
-    Expr getLhs() { result = this.getLeftOperand() }
+  class SubExpr = RU::ExprNode::SubExpr;
 
-    /** Gets the RHS operand of this add expression. */
-    Expr getRhs() { result = this.getRightOperand() }
-  }
+  class RemExpr = RU::ExprNode::RemExpr;
 
-  /** Represent a subtraction expression. */
-  class SubExpr extends CS::SubExpr {
-    /** Gets the LHS operand of this subtraction expression. */
-    Expr getLhs() { result = this.getLeftOperand() }
+  class BitwiseAndExpr = RU::ExprNode::BitwiseAndExpr;
 
-    /** Gets the RHS operand of this subtraction expression. */
-    Expr getRhs() { result = this.getRightOperand() }
-  }
+  class MulExpr = RU::ExprNode::MulExpr;
 
-  class RemExpr = CS::RemExpr;
+  class LShiftExpr = RU::ExprNode::LShiftExpr;
 
-  /** Represent a bitwise and or an assign-and expression. */
-  class BitwiseAndExpr extends CS::Expr {
-    BitwiseAndExpr() { this instanceof CS::BitwiseAndExpr or this instanceof CS::AssignAndExpr }
+  predicate guardDirectlyControlsSsaRead = RU::guardControlsSsaRead/3;
 
-    /** Gets an operand of this bitwise and operation. */
-    Expr getAnOperand() {
-      result = this.(CS::BitwiseAndExpr).getAnOperand() or
-      result = this.(CS::AssignAndExpr).getRValue() or
-      result = this.(CS::AssignAndExpr).getLValue()
-    }
-
-    /** Holds if this expression has operands `e1` and `e2`. */
-    predicate hasOperands(Expr e1, Expr e2) {
-      this.getAnOperand() = e1 and
-      this.getAnOperand() = e2 and
-      e1 != e2
-    }
-  }
-
-  /** Represent a multiplication or an assign-mul expression. */
-  class MulExpr extends CS::Expr {
-    MulExpr() { this instanceof CS::MulExpr or this instanceof CS::AssignMulExpr }
-
-    /** Gets an operand of this multiplication. */
-    Expr getAnOperand() {
-      result = this.(CS::MulExpr).getAnOperand() or
-      result = this.(CS::AssignMulExpr).getRValue() or
-      result = this.(CS::AssignMulExpr).getLValue()
-    }
-  }
-
-  /** Represent a left shift or an assign-lshift expression. */
-  class LShiftExpr extends CS::Expr {
-    LShiftExpr() { this instanceof CS::LShiftExpr or this instanceof CS::AssignLShiftExpr }
-
-    /** Gets the RHS operand of this shift. */
-    Expr getRhs() {
-      result = this.(CS::LShiftExpr).getRightOperand() or
-      result = this.(CS::AssignLShiftExpr).getRValue()
-    }
-  }
-
-  predicate guardDirectlyControlsSsaRead = SA::guardControlsSsaRead/3;
-
-  predicate guardControlsSsaRead = SA::guardControlsSsaRead/3;
+  predicate guardControlsSsaRead = RU::guardControlsSsaRead/3;
 
   predicate valueFlowStep = RU::valueFlowStep/3;
 
@@ -100,11 +41,44 @@ module Private {
 
   predicate ssaUpdateStep = RU::ssaUpdateStep/3;
 
-  Expr getABasicBlockExpr(BasicBlock bb) { result = bb.getANode().getElement() }
+  Expr getABasicBlockExpr(BasicBlock bb) { result = bb.getANode() }
 
-  private predicate id(CS::ControlFlowElement x, CS::ControlFlowElement y) { x = y }
+  private class CallableOrCFE extends CS::Element {
+    CallableOrCFE() { this instanceof CS::Callable or this instanceof CS::ControlFlowElement }
+  }
 
-  private predicate idOf(CS::ControlFlowElement x, int y) = equivalenceRelation(id/2)(x, y)
+  private predicate id(CallableOrCFE x, CallableOrCFE y) { x = y }
 
-  int getId(BasicBlock bb) { idOf(bb.getFirstNode().getElement(), result) }
+  private predicate idOf(CallableOrCFE x, int y) = equivalenceRelation(id/2)(x, y)
+
+  private class PhiInputEdgeBlock extends BasicBlock {
+    PhiInputEdgeBlock() { this = any(SsaReadPositionPhiInputEdge edge).getOrigBlock() }
+  }
+
+  int getId(PhiInputEdgeBlock bb) {
+    idOf(bb.getFirstNode().getElement(), result)
+    or
+    idOf(bb.(CS::ControlFlow::BasicBlocks::EntryBlock).getCallable(), result)
+  }
+
+  private string getSplitString(PhiInputEdgeBlock bb) {
+    result = bb.getFirstNode().(CS::ControlFlow::Nodes::ElementNode).getSplitsString()
+    or
+    not exists(bb.getFirstNode().(CS::ControlFlow::Nodes::ElementNode).getSplitsString()) and
+    result = ""
+  }
+
+  /**
+   * Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
+   * in an arbitrary 1-based numbering of the input edges to `phi`.
+   */
+  predicate rankedPhiInput(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r) {
+    edge.phiInput(phi, inp) and
+    edge =
+      rank[r](SsaReadPositionPhiInputEdge e |
+        e.phiInput(phi, _)
+      |
+        e order by getId(e.getOrigBlock()), getSplitString(e.getOrigBlock())
+      )
+  }
 }
diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/RangeUtils.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/RangeUtils.qll
index 4abfb2d1779..6096df5e2e4 100644
--- a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/RangeUtils.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/RangeUtils.qll
@@ -1,98 +1,406 @@
 /**
  * Provides predicates for range and modulus analysis.
  */
+private module Impl {
+  private import csharp
+  private import Ssa
+  private import SsaUtils
+  private import ConstantUtils
+  private import SsaReadPositionCommon
+  private import semmle.code.csharp.controlflow.Guards as G
+  private import ControlFlowReachability
 
-private import csharp
-private import Ssa
-private import SsaUtils
-private import ConstantUtils
-private import SsaReadPositionCommon
-private import semmle.code.csharp.controlflow.Guards as G
+  private class BooleanValue = G::AbstractValues::BooleanValue;
 
-private class BooleanValue = G::AbstractValues::BooleanValue;
+  private class ExprNode = ControlFlow::Nodes::ExprNode;
 
-/**
- * Holds if `v` is an `ExplicitDefinition` that equals `e + delta`.
- */
-predicate ssaUpdateStep(ExplicitDefinition v, Expr e, int delta) {
-  v.getADefinition().getExpr().(Assignment).getRValue() = e and delta = 0
-  or
-  v.getADefinition().getExpr().(PostIncrExpr).getOperand() = e and delta = 1
-  or
-  v.getADefinition().getExpr().(PreIncrExpr).getOperand() = e and delta = 1
-  or
-  v.getADefinition().getExpr().(PostDecrExpr).getOperand() = e and delta = -1
-  or
-  v.getADefinition().getExpr().(PreDecrExpr).getOperand() = e and delta = -1
-}
+  private class ExprChildReachability extends ControlFlowReachabilityConfiguration {
+    ExprChildReachability() { this = "ExprChildReachability" }
 
-private G::Guard eqFlowCondAbs(Definition def, Expr e, int delta, boolean isEq, G::AbstractValue v) {
-  exists(boolean eqpolarity |
-    result.isEquality(ssaRead(def, delta), e, eqpolarity) and
-    eqpolarity.booleanXor(v.(BooleanValue).getValue()).booleanNot() = isEq
-  )
-  or
-  exists(G::AbstractValue v0 |
-    G::Internal::impliesSteps(result, v, eqFlowCondAbs(def, e, delta, isEq, v0), v0)
-  )
-}
+    override predicate candidate(
+      Expr e1, Expr e2, ControlFlowElement scope, boolean exactScope, boolean isSuccessor
+    ) {
+      e2 = e1.getAChild() and
+      scope = e1 and
+      exactScope = false and
+      isSuccessor in [false, true]
+    }
+  }
 
-/**
- * Gets a condition that tests whether `def` equals `e + delta`.
- *
- * If the condition evaluates to `testIsTrue`:
- * - `isEq = true`  : `def == e + delta`
- * - `isEq = false` : `def != e + delta`
- */
-G::Guard eqFlowCond(Definition def, Expr e, int delta, boolean isEq, boolean testIsTrue) {
-  exists(BooleanValue v |
-    result = eqFlowCondAbs(def, e, delta, isEq, v) and
-    testIsTrue = v.getValue()
-  )
-}
+  /** Holds if `parent` having child `child` implies `parentNode` having child `childNode`. */
+  predicate hasChild(Expr parent, Expr child, ExprNode parentNode, ExprNode childNode) {
+    any(ExprChildReachability x).hasExprPath(parent, parentNode, child, childNode)
+  }
 
-/**
- * Holds if `e1 + delta` equals `e2`.
- */
-predicate valueFlowStep(Expr e2, Expr e1, int delta) {
-  valueFlowStep(e2.(AssignOperation).getExpandedAssignment(), e1, delta)
-  or
-  e2.(AssignExpr).getRValue() = e1 and delta = 0
-  or
-  e2.(UnaryPlusExpr).getOperand() = e1 and delta = 0
-  or
-  e2.(PostIncrExpr).getOperand() = e1 and delta = 0
-  or
-  e2.(PostDecrExpr).getOperand() = e1 and delta = 0
-  or
-  e2.(PreIncrExpr).getOperand() = e1 and delta = 1
-  or
-  e2.(PreDecrExpr).getOperand() = e1 and delta = -1
-  or
-  exists(ConstantIntegerExpr x |
-    e2.(AddExpr).getAnOperand() = e1 and
-    e2.(AddExpr).getAnOperand() = x and
-    not e1 = x
-  |
-    x.getIntValue() = delta
-  )
-  or
-  exists(ConstantIntegerExpr x |
-    exists(SubExpr sub |
-      e2 = sub and
-      sub.getLeftOperand() = e1 and
-      sub.getRightOperand() = x
+  /** Holds if SSA definition `def` equals `e + delta`. */
+  predicate ssaUpdateStep(ExplicitDefinition def, ExprNode e, int delta) {
+    exists(ControlFlow::Node cfn | cfn = def.getControlFlowNode() |
+      e = cfn.(ExprNode::Assignment).getRValue() and delta = 0
+      or
+      e = cfn.(ExprNode::PostIncrExpr).getOperand() and delta = 1
+      or
+      e = cfn.(ExprNode::PreIncrExpr).getOperand() and delta = 1
+      or
+      e = cfn.(ExprNode::PostDecrExpr).getOperand() and delta = -1
+      or
+      e = cfn.(ExprNode::PreDecrExpr).getOperand() and delta = -1
     )
-  |
-    x.getIntValue() = -delta
-  )
+  }
+
+  /** Holds if `e1 + delta` equals `e2`. */
+  predicate valueFlowStep(ExprNode e2, ExprNode e1, int delta) {
+    e2.(ExprNode::AssignExpr).getRValue() = e1 and delta = 0
+    or
+    e2.(ExprNode::UnaryPlusExpr).getOperand() = e1 and delta = 0
+    or
+    e2.(ExprNode::PostIncrExpr).getOperand() = e1 and delta = 0
+    or
+    e2.(ExprNode::PostDecrExpr).getOperand() = e1 and delta = 0
+    or
+    e2.(ExprNode::PreIncrExpr).getOperand() = e1 and delta = 1
+    or
+    e2.(ExprNode::PreDecrExpr).getOperand() = e1 and delta = -1
+    or
+    exists(ConstantIntegerExpr x |
+      e2.(ExprNode::AddExpr).getAnOperand() = e1 and
+      e2.(ExprNode::AddExpr).getAnOperand() = x and
+      e1 != x and
+      x.getIntValue() = delta
+    )
+    or
+    exists(ConstantIntegerExpr x |
+      e2.(ExprNode::SubExpr).getLeftOperand() = e1 and
+      e2.(ExprNode::SubExpr).getRightOperand() = x and
+      x.getIntValue() = -delta
+    )
+  }
+
+  /** An expression whose value may control the execution of another element. */
+  class Guard extends Expr {
+    Guard() { this instanceof G::Guard }
+
+    /**
+     * Holds if basic block `bb` is guarded by this guard having value `v`.
+     */
+    predicate controlsBasicBlock(BasicBlock bb, G::AbstractValue v) {
+      this.(G::Guard).controlsBasicBlock(bb, v)
+    }
+
+    /**
+     * Holds if this guard is an equality test between `e1` and `e2`. If the test is
+     * negated, that is `!=`, then `polarity` is false, otherwise `polarity` is
+     * true.
+     */
+    predicate isEquality(ExprNode e1, ExprNode e2, boolean polarity) {
+      exists(Expr e1_, Expr e2_ |
+        e1 = unique(ExprNode cfn | hasChild(this, e1_, _, cfn) | cfn) and
+        e2 = unique(ExprNode cfn | hasChild(this, e2_, _, cfn) | cfn) and
+        this.(G::Guard).isEquality(e1_, e2_, polarity)
+      )
+    }
+  }
+
+  private Guard eqFlowCondAbs(
+    Definition def, ExprNode e, int delta, boolean isEq, G::AbstractValue v
+  ) {
+    exists(boolean eqpolarity |
+      result.isEquality(ssaRead(def, delta), e, eqpolarity) and
+      eqpolarity.booleanXor(v.(BooleanValue).getValue()).booleanNot() = isEq
+    )
+    or
+    exists(G::AbstractValue v0 |
+      G::Internal::impliesSteps(result, v, eqFlowCondAbs(def, e, delta, isEq, v0), v0)
+    )
+  }
+
+  /**
+   * Gets a condition that tests whether `def` equals `e + delta`.
+   *
+   * If the condition evaluates to `testIsTrue`:
+   * - `isEq = true`  : `def == e + delta`
+   * - `isEq = false` : `def != e + delta`
+   */
+  Guard eqFlowCond(Definition def, ExprNode e, int delta, boolean isEq, boolean testIsTrue) {
+    exists(BooleanValue v |
+      result = eqFlowCondAbs(def, e, delta, isEq, v) and
+      testIsTrue = v.getValue()
+    )
+  }
+
+  /**
+   * Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
+   */
+  predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
+    exists(BooleanValue b | b.getValue() = testIsTrue |
+      guard.controlsBasicBlock(controlled.(SsaReadPositionBlock).getBlock(), b)
+    )
+  }
+
+  /**
+   * Holds if property `p` matches `property` in `baseClass` or any overrides.
+   */
+  predicate propertyOverrides(Property p, string baseClass, string property) {
+    exists(Property p2 |
+      p2.getSourceDeclaration().getDeclaringType().hasQualifiedName(baseClass) and
+      p2.hasName(property)
+    |
+      p.overridesOrImplementsOrEquals(p2)
+    )
+  }
 }
 
+import Impl
+
 /**
- * Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
+ * Provides classes for mapping CFG nodes to AST nodes, in a way that respects
+ * control-flow splitting. For example, in
+ *
+ * ```csharp
+ * int M(bool b)
+ * {
+ *     var i = b ? 1 : -1;
+ *     i = i - 1;
+ *     if (b)
+ *         return 0;
+ *     return i;
+ * }
+ * ```
+ * the subtraction `i - 1` exists in two copies in the CFG. The class `SubExpr`
+ * contains each copy, with split-respecting `getLeft/RightOperand()` predicates.
  */
-predicate guardControlsSsaRead(G::Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
-  exists(BooleanValue b | b.getValue() = testIsTrue |
-    guard.controlsBasicBlock(controlled.(SsaReadPositionBlock).getBlock(), b)
-  )
+module ExprNode {
+  private import csharp as CS
+
+  private class ExprNode = CS::ControlFlow::Nodes::ExprNode;
+
+  private import Sign
+
+  /** An assignable access. */
+  class AssignableAccess extends ExprNode {
+    override CS::AssignableAccess e;
+  }
+
+  /** A field access. */
+  class FieldAccess extends ExprNode {
+    override CS::FieldAccess e;
+  }
+
+  /** A character literal. */
+  class CharLiteral extends ExprNode {
+    override CS::CharLiteral e;
+  }
+
+  /** An integer literal. */
+  class IntegerLiteral extends ExprNode {
+    override CS::IntegerLiteral e;
+  }
+
+  /** A long literal. */
+  class LongLiteral extends ExprNode {
+    override CS::LongLiteral e;
+  }
+
+  /** A cast. */
+  class CastExpr extends ExprNode {
+    override CS::CastExpr e;
+
+    /** Gets the source type of this cast. */
+    CS::Type getSourceType() { result = e.getSourceType() }
+  }
+
+  /** A floating point literal. */
+  class RealLiteral extends ExprNode {
+    override CS::RealLiteral e;
+  }
+
+  /** An assignment. */
+  class Assignment extends ExprNode {
+    override CS::Assignment e;
+
+    /** Gets the left operand of this assignment. */
+    ExprNode getLValue() {
+      result = unique(ExprNode res | hasChild(e, e.getLValue(), this, res) | res)
+    }
+
+    /** Gets the right operand of this assignment. */
+    ExprNode getRValue() {
+      result = unique(ExprNode res | hasChild(e, e.getRValue(), this, res) | res)
+    }
+  }
+
+  /** A simple assignment. */
+  class AssignExpr extends Assignment {
+    override CS::AssignExpr e;
+  }
+
+  /** A unary operation. */
+  class UnaryOperation extends ExprNode {
+    override CS::UnaryOperation e;
+
+    /** Returns the operand of this unary operation. */
+    ExprNode getOperand() {
+      result = unique(ExprNode res | hasChild(e, e.getOperand(), this, res) | res)
+    }
+
+    /** Returns the operation representing this unary operation. */
+    TUnarySignOperation getOp() { none() }
+  }
+
+  /** A prefix increment operation. */
+  class PreIncrExpr extends UnaryOperation {
+    override CS::PreIncrExpr e;
+
+    override TIncOp getOp() { any() }
+  }
+
+  /** A postfix increment operation. */
+  class PostIncrExpr extends UnaryOperation {
+    override CS::PostIncrExpr e;
+  }
+
+  /** A prefix decrement operation. */
+  class PreDecrExpr extends UnaryOperation {
+    override CS::PreDecrExpr e;
+
+    override TDecOp getOp() { any() }
+  }
+
+  /** A postfix decrement operation. */
+  class PostDecrExpr extends UnaryOperation {
+    override CS::PostDecrExpr e;
+  }
+
+  /** A unary plus operation. */
+  class UnaryPlusExpr extends UnaryOperation {
+    override CS::UnaryPlusExpr e;
+  }
+
+  /** A unary minus operation. */
+  class UnaryMinusExpr extends UnaryOperation {
+    override CS::UnaryMinusExpr e;
+
+    override TNegOp getOp() { any() }
+  }
+
+  /** A bitwise complement operation. */
+  class ComplementExpr extends UnaryOperation {
+    override CS::ComplementExpr e;
+
+    override TBitNotOp getOp() { any() }
+  }
+
+  /** A binary operation. */
+  class BinaryOperation extends ExprNode {
+    override CS::BinaryOperation e;
+
+    /** Returns the operation representing this binary operation. */
+    TBinarySignOperation getOp() { none() }
+
+    /** Gets the left operand of this binary operation. */
+    ExprNode getLeftOperand() {
+      result = unique(ExprNode res | hasChild(e, e.getLeftOperand(), this, res) | res)
+    }
+
+    /** Gets the right operand of this binary operation. */
+    ExprNode getRightOperand() {
+      result = unique(ExprNode res | hasChild(e, e.getRightOperand(), this, res) | res)
+    }
+
+    /** Gets the left operand of this binary operation. */
+    ExprNode getLhs() { result = this.getLeftOperand() }
+
+    /** Gets the right operand of this binary operation. */
+    ExprNode getRhs() { result = this.getRightOperand() }
+
+    /** Gets an operand of this binary operation. */
+    ExprNode getAnOperand() { hasChild(e, e.getAnOperand(), this, result) }
+
+    /** Holds if this binary operation has operands `e1` and `e2`. */
+    predicate hasOperands(ExprNode e1, ExprNode e2) {
+      this.getAnOperand() = e1 and
+      this.getAnOperand() = e2 and
+      e1 != e2
+    }
+  }
+
+  /** An addition operation. */
+  class AddExpr extends BinaryOperation {
+    override CS::AddExpr e;
+
+    override TAddOp getOp() { any() }
+  }
+
+  /** A subtraction operation. */
+  class SubExpr extends BinaryOperation {
+    override CS::SubExpr e;
+
+    override TSubOp getOp() { any() }
+  }
+
+  /** A multiplication operation. */
+  class MulExpr extends BinaryOperation {
+    override CS::MulExpr e;
+
+    override TMulOp getOp() { any() }
+  }
+
+  /** A division operation. */
+  class DivExpr extends BinaryOperation {
+    override CS::DivExpr e;
+
+    override TDivOp getOp() { any() }
+  }
+
+  /** A remainder operation. */
+  class RemExpr extends BinaryOperation {
+    override CS::RemExpr e;
+
+    override TRemOp getOp() { any() }
+  }
+
+  /** A bitwise-and operation. */
+  class BitwiseAndExpr extends BinaryOperation {
+    override CS::BitwiseAndExpr e;
+
+    override TBitAndOp getOp() { any() }
+  }
+
+  /** A bitwise-or operation. */
+  class BitwiseOrExpr extends BinaryOperation {
+    override CS::BitwiseOrExpr e;
+
+    override TBitOrOp getOp() { any() }
+  }
+
+  /** A bitwise-xor operation. */
+  class BitwiseXorExpr extends BinaryOperation {
+    override CS::BitwiseXorExpr e;
+
+    override TBitXorOp getOp() { any() }
+  }
+
+  /** A left-shift operation. */
+  class LShiftExpr extends BinaryOperation {
+    override CS::LShiftExpr e;
+
+    override TLShiftOp getOp() { any() }
+  }
+
+  /** A right-shift operation. */
+  class RShiftExpr extends BinaryOperation {
+    override CS::RShiftExpr e;
+
+    override TRShiftOp getOp() { any() }
+  }
+
+  /** A conditional expression. */
+  class ConditionalExpr extends ExprNode {
+    override CS::ConditionalExpr e;
+
+    /** Gets the "then" expression of this conditional expression. */
+    ExprNode getTrueExpr() { hasChild(e, e.getThen(), this, result) }
+
+    /** Gets the "else" expression of this conditional expression. */
+    ExprNode getFalseExpr() { hasChild(e, e.getElse(), this, result) }
+  }
 }
diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll
index d00a38bac73..06af17094a5 100644
--- a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll
@@ -51,7 +51,7 @@ private predicate unknownSign(Expr e) {
     or
     exists(CastExpr cast, Type fromtyp |
       cast = e and
-      fromtyp = cast.getExpr().getType() and
+      fromtyp = cast.getSourceType() and
       not fromtyp instanceof NumericOrCharType
     )
     or
diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll
index 782c01d15b7..1dee323fd24 100644
--- a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll
@@ -6,11 +6,10 @@ module Private {
   private import SsaUtils as SU
   private import ConstantUtils as CU
   private import RangeUtils as RU
-  private import semmle.code.csharp.controlflow.Guards as G
   private import Sign
   import Impl
 
-  class Guard = G::Guard;
+  class Guard = RU::Guard;
 
   class ConstantIntegerExpr = CU::ConstantIntegerExpr;
 
@@ -18,97 +17,33 @@ module Private {
 
   class SsaPhiNode = CS::Ssa::PhiNode;
 
-  class VarAccess = CS::AssignableAccess;
+  class VarAccess = RU::ExprNode::AssignableAccess;
 
-  class FieldAccess = CS::FieldAccess;
+  class FieldAccess = RU::ExprNode::FieldAccess;
 
-  class CharacterLiteral = CS::CharLiteral;
+  class CharacterLiteral = RU::ExprNode::CharLiteral;
 
-  class IntegerLiteral = CS::IntegerLiteral;
+  class IntegerLiteral = RU::ExprNode::IntegerLiteral;
 
-  class LongLiteral = CS::LongLiteral;
+  class LongLiteral = RU::ExprNode::LongLiteral;
 
-  class CastExpr = CS::CastExpr;
+  class CastExpr = RU::ExprNode::CastExpr;
 
   class Type = CS::Type;
 
-  class Expr = CS::Expr;
+  class Expr = CS::ControlFlow::Nodes::ExprNode;
 
-  class VariableUpdate = CS::AssignableDefinition;
+  class VariableUpdate = CS::Ssa::ExplicitDefinition;
 
   class Field = CS::Field;
 
-  class RealLiteral = CS::RealLiteral;
+  class RealLiteral = RU::ExprNode::RealLiteral;
 
-  class DivExpr = CS::DivExpr;
+  class DivExpr = RU::ExprNode::DivExpr;
 
-  /** Class to represent unary operation. */
-  class UnaryOperation extends Expr {
-    UnaryOperation() {
-      this instanceof CS::PreIncrExpr or
-      this instanceof CS::PreDecrExpr or
-      this instanceof CS::UnaryMinusExpr or
-      this instanceof CS::ComplementExpr
-    }
+  class UnaryOperation = RU::ExprNode::UnaryOperation;
 
-    /** Returns the operand of this expression. */
-    Expr getOperand() {
-      result = this.(CS::PreIncrExpr).getOperand() or
-      result = this.(CS::PreDecrExpr).getOperand() or
-      result = this.(CS::UnaryMinusExpr).getOperand() or
-      result = this.(CS::ComplementExpr).getOperand()
-    }
-
-    /** Returns the operation representing this expression. */
-    TUnarySignOperation getOp() {
-      this instanceof CS::PreIncrExpr and result = TIncOp()
-      or
-      this instanceof CS::PreDecrExpr and result = TDecOp()
-      or
-      this instanceof CS::UnaryMinusExpr and result = TNegOp()
-      or
-      this instanceof CS::ComplementExpr and result = TBitNotOp()
-    }
-  }
-
-  /** Class to represent binary operation. */
-  class BinaryOperation extends CS::BinaryOperation {
-    BinaryOperation() {
-      this instanceof CS::AddExpr or
-      this instanceof CS::SubExpr or
-      this instanceof CS::MulExpr or
-      this instanceof CS::DivExpr or
-      this instanceof CS::RemExpr or
-      this instanceof CS::BitwiseAndExpr or
-      this instanceof CS::BitwiseOrExpr or
-      this instanceof CS::BitwiseXorExpr or
-      this instanceof CS::LShiftExpr or
-      this instanceof CS::RShiftExpr
-    }
-
-    /** Returns the operation representing this expression. */
-    TBinarySignOperation getOp() {
-      this instanceof CS::AddExpr and result = TAddOp()
-      or
-      this instanceof CS::SubExpr and result = TSubOp()
-      or
-      this instanceof CS::MulExpr and result = TMulOp()
-      or
-      this instanceof CS::DivExpr and result = TDivOp()
-      or
-      this instanceof CS::RemExpr and result = TRemOp()
-      or
-      this instanceof CS::BitwiseAndExpr and result = TBitAndOp()
-      or
-      this instanceof CS::BitwiseOrExpr and result = TBitOrOp()
-      or
-      this instanceof CS::BitwiseXorExpr and result = TBitXorOp()
-      or
-      this instanceof CS::LShiftExpr and result = TLShiftOp()
-      or
-      this instanceof CS::RShiftExpr and result = TRShiftOp()
-    }
-  }
+  class BinaryOperation = RU::ExprNode::BinaryOperation;
 
   predicate ssaRead = SU::ssaRead/2;
 
@@ -118,21 +53,21 @@ module Private {
 private module Impl {
   private import csharp
   private import SsaUtils
+  private import RangeUtils
   private import ConstantUtils
-  private import semmle.code.csharp.controlflow.Guards
   private import Linq.Helpers
   private import Sign
   private import SignAnalysisCommon
   private import SsaReadPositionCommon
   private import semmle.code.csharp.commons.ComparisonTest
 
-  private class BooleanValue = AbstractValues::BooleanValue;
+  private class ExprNode = ControlFlow::Nodes::ExprNode;
 
   /** Gets the character value of expression `e`. */
-  string getCharValue(Expr e) { result = e.getValue() and e.getType() instanceof CharType }
+  string getCharValue(ExprNode e) { result = e.getValue() and e.getType() instanceof CharType }
 
   /** Gets the constant `float` value of non-`ConstantIntegerExpr` expressions. */
-  float getNonIntegerValue(Expr e) {
+  float getNonIntegerValue(ExprNode e) {
     exists(string s |
       s = e.getValue() and
       result = s.toFloat() and
@@ -144,19 +79,19 @@ private module Impl {
    * Holds if `e` is an access to the size of a container (`string`, `Array`,
    * `IEnumerable`, or `ICollection`).
    */
-  predicate containerSizeAccess(Expr e) {
-    exists(Property p | p = e.(PropertyAccess).getTarget() |
+  predicate containerSizeAccess(ExprNode e) {
+    exists(Property p | p = e.getExpr().(PropertyAccess).getTarget() |
       propertyOverrides(p, "System.Collections.Generic.IEnumerable<>", "Count") or
       propertyOverrides(p, "System.Collections.ICollection", "Count") or
       propertyOverrides(p, "System.String", "Length") or
       propertyOverrides(p, "System.Array", "Length")
     )
     or
-    e instanceof CountCall
+    e.getExpr() instanceof CountCall
   }
 
   /** Holds if `e` is by definition strictly positive. */
-  predicate positiveExpression(Expr e) { e instanceof SizeofExpr }
+  predicate positiveExpression(ExprNode e) { e.getExpr() instanceof SizeofExpr }
 
   abstract class NumericOrCharType extends Type { }
 
@@ -185,43 +120,48 @@ private module Impl {
   }
 
   /** Returns the underlying variable update of the explicit SSA variable `v`. */
-  AssignableDefinition getExplicitSsaAssignment(Ssa::ExplicitDefinition v) {
-    result = v.getADefinition()
-  }
+  Ssa::ExplicitDefinition getExplicitSsaAssignment(Ssa::ExplicitDefinition v) { result = v }
 
   /** Returns the assignment of the variable update `def`. */
-  Expr getExprFromSsaAssignment(AssignableDefinition def) { result = def.getSource() }
+  ExprNode getExprFromSsaAssignment(Ssa::ExplicitDefinition def) {
+    exists(AssignableDefinition adef |
+      adef = def.getADefinition() and
+      hasChild(adef.getExpr(), adef.getSource(), def.getControlFlowNode(), result)
+    )
+  }
 
   /** Holds if `def` can have any sign. */
-  predicate explicitSsaDefWithAnySign(AssignableDefinition def) {
-    not exists(def.getSource()) and
+  predicate explicitSsaDefWithAnySign(Ssa::ExplicitDefinition def) {
+    not exists(def.getADefinition().getSource()) and
     not def.getElement() instanceof MutatorOperation
   }
 
   /** Returns the operand of the operation if `def` is a decrement. */
-  Expr getDecrementOperand(AssignableDefinition def) {
-    result = def.getElement().(DecrementOperation).getOperand()
+  ExprNode getDecrementOperand(Ssa::ExplicitDefinition def) {
+    hasChild(def.getElement(), def.getElement().(DecrementOperation).getOperand(),
+      def.getControlFlowNode(), result)
   }
 
   /** Returns the operand of the operation if `def` is an increment. */
-  Expr getIncrementOperand(AssignableDefinition def) {
-    result = def.getElement().(IncrementOperation).getOperand()
+  ExprNode getIncrementOperand(Ssa::ExplicitDefinition def) {
+    hasChild(def.getElement(), def.getElement().(IncrementOperation).getOperand(),
+      def.getControlFlowNode(), result)
   }
 
-  /** Gets the variable underlying the implicit SSA variable `v`. */
-  Declaration getImplicitSsaDeclaration(Ssa::ImplicitDefinition v) {
-    result = v.getSourceVariable().getAssignable()
+  /** Gets the variable underlying the implicit SSA variable `def`. */
+  Declaration getImplicitSsaDeclaration(Ssa::ImplicitDefinition def) {
+    result = def.getSourceVariable().getAssignable()
   }
 
-  /** Holds if the variable underlying the implicit SSA variable `v` is not a field. */
-  predicate nonFieldImplicitSsaDefinition(Ssa::ImplicitDefinition v) {
-    not getImplicitSsaDeclaration(v) instanceof Field
+  /** Holds if the variable underlying the implicit SSA variable `def` is not a field. */
+  predicate nonFieldImplicitSsaDefinition(Ssa::ImplicitDefinition def) {
+    not getImplicitSsaDeclaration(def) instanceof Field
   }
 
   /** Returned an expression that is assigned to `f`. */
-  Expr getAssignedValueToField(Field f) {
-    result = f.getAnAssignedValue() or
-    result = any(AssignOperation a | a.getLValue() = f.getAnAccess())
+  ExprNode getAssignedValueToField(Field f) {
+    result.getExpr() in [f.getAnAssignedValue(),
+          any(AssignOperation a | a.getLValue() = f.getAnAccess())]
   }
 
   /** Holds if `f` can have any sign. */
@@ -244,71 +184,78 @@ private module Impl {
   /**
    * Holds if `e` has type `NumericOrCharType`, but the sign of `e` is unknown.
    */
-  predicate numericExprWithUnknownSign(Expr e) {
+  predicate numericExprWithUnknownSign(ExprNode e) {
     e.getType() instanceof NumericOrCharType and
     not e = getARead(_) and
-    not e instanceof FieldAccess and
-    not e instanceof TypeAccess and
+    not e.getExpr() instanceof FieldAccess and
+    not e.getExpr() instanceof TypeAccess and
     // The expression types that are listed here are the ones handled in `specificSubExprSign`.
     // Keep them in sync.
-    not e instanceof AssignExpr and
-    not e instanceof AssignOperation and
-    not e instanceof UnaryPlusExpr and
-    not e instanceof PostIncrExpr and
-    not e instanceof PostDecrExpr and
-    not e instanceof PreIncrExpr and
-    not e instanceof PreDecrExpr and
-    not e instanceof UnaryMinusExpr and
-    not e instanceof ComplementExpr and
-    not e instanceof AddExpr and
-    not e instanceof SubExpr and
-    not e instanceof MulExpr and
-    not e instanceof DivExpr and
-    not e instanceof RemExpr and
-    not e instanceof BitwiseAndExpr and
-    not e instanceof BitwiseOrExpr and
-    not e instanceof BitwiseXorExpr and
-    not e instanceof LShiftExpr and
-    not e instanceof RShiftExpr and
-    not e instanceof ConditionalExpr and
-    not e instanceof RefExpr and
-    not e instanceof LocalVariableDeclAndInitExpr and
-    not e instanceof SwitchCaseExpr and
-    not e instanceof CastExpr and
-    not e instanceof SwitchExpr and
-    not e instanceof NullCoalescingExpr
+    not e.getExpr() instanceof AssignExpr and
+    not e.getExpr() instanceof AssignOperation and
+    not e.getExpr() instanceof UnaryPlusExpr and
+    not e.getExpr() instanceof PostIncrExpr and
+    not e.getExpr() instanceof PostDecrExpr and
+    not e.getExpr() instanceof PreIncrExpr and
+    not e.getExpr() instanceof PreDecrExpr and
+    not e.getExpr() instanceof UnaryMinusExpr and
+    not e.getExpr() instanceof ComplementExpr and
+    not e.getExpr() instanceof AddExpr and
+    not e.getExpr() instanceof SubExpr and
+    not e.getExpr() instanceof MulExpr and
+    not e.getExpr() instanceof DivExpr and
+    not e.getExpr() instanceof RemExpr and
+    not e.getExpr() instanceof BitwiseAndExpr and
+    not e.getExpr() instanceof BitwiseOrExpr and
+    not e.getExpr() instanceof BitwiseXorExpr and
+    not e.getExpr() instanceof LShiftExpr and
+    not e.getExpr() instanceof RShiftExpr and
+    not e.getExpr() instanceof ConditionalExpr and
+    not e.getExpr() instanceof RefExpr and
+    not e.getExpr() instanceof LocalVariableDeclAndInitExpr and
+    not e.getExpr() instanceof SwitchCaseExpr and
+    not e.getExpr() instanceof CastExpr and
+    not e.getExpr() instanceof SwitchExpr and
+    not e.getExpr() instanceof NullCoalescingExpr
   }
 
   /** Returns a sub expression of `e` for expression types where the sign depends on the child. */
-  Expr getASubExprWithSameSign(Expr e) {
-    result = e.(AssignExpr).getRValue() or
-    result = e.(AssignOperation).getExpandedAssignment() or
-    result = e.(UnaryPlusExpr).getOperand() or
-    result = e.(PostIncrExpr).getOperand() or
-    result = e.(PostDecrExpr).getOperand() or
-    result = e.(ConditionalExpr).getAChild() or
-    result = e.(NullCoalescingExpr).getAChild() or
-    result = e.(SwitchExpr).getACase().getBody() or
-    result = e.(SwitchCaseExpr).getBody() or
-    result = e.(LocalVariableDeclAndInitExpr).getInitializer() or
-    result = e.(RefExpr).getExpr() or
-    result = e.(CastExpr).getExpr()
+  ExprNode getASubExprWithSameSign(ExprNode e) {
+    exists(Expr e_, Expr child | hasChild(e_, child, e, result) |
+      child = e_.(AssignExpr).getRValue() or
+      child = e_.(UnaryPlusExpr).getOperand() or
+      child = e_.(PostIncrExpr).getOperand() or
+      child = e_.(PostDecrExpr).getOperand() or
+      child = e_.(ConditionalExpr).getAChild() or
+      child = e_.(NullCoalescingExpr).getAChild() or
+      child = e_.(SwitchExpr).getACase() or
+      child = e_.(SwitchCaseExpr).getBody() or
+      child = e_.(LocalVariableDeclAndInitExpr).getInitializer() or
+      child = e_.(RefExpr).getExpr() or
+      child = e_.(CastExpr).getExpr()
+    )
   }
 
-  Expr getARead(Ssa::Definition v) { result = v.getARead() }
+  ExprNode getARead(Ssa::Definition v) { exists(v.getAReadAtNode(result)) }
 
-  Field getField(FieldAccess fa) { result = fa.getTarget() }
+  Field getField(ExprNode fa) { result = fa.getExpr().(FieldAccess).getTarget() }
 
-  Expr getAnExpression(SsaReadPositionBlock bb) { result = bb.getBlock().getANode().getElement() }
+  ExprNode getAnExpression(SsaReadPositionBlock bb) { result = bb.getBlock().getANode() }
 
   Guard getComparisonGuard(ComparisonExpr ce) { result = ce.getExpr() }
 
+  private newtype TComparisonExpr =
+    MkComparisonExpr(ComparisonTest ct, ExprNode e) { e = ct.getExpr().getAControlFlowNode() }
+
   /** A relational comparison */
-  class ComparisonExpr extends ComparisonTest {
+  class ComparisonExpr extends MkComparisonExpr {
+    private ComparisonTest ct;
+    private ExprNode e;
     private boolean strict;
 
     ComparisonExpr() {
-      this.getComparisonKind() =
+      this = MkComparisonExpr(ct, e) and
+      ct.getComparisonKind() =
         any(ComparisonKind ck |
           ck.isLessThan() and strict = true
           or
@@ -317,13 +264,22 @@ private module Impl {
         )
     }
 
+    /** Gets the underlying expression. */
+    Expr getExpr() { result = ct.getExpr() }
+
+    /** Gets a textual representation of this comparison test. */
+    string toString() { result = ct.toString() }
+
+    /** Gets the location of this comparison test. */
+    Location getLocation() { result = ct.getLocation() }
+
     /**
      * Gets the operand on the "greater" (or "greater-or-equal") side
      * of this relational expression, that is, the side that is larger
      * if the overall expression evaluates to `true`; for example on
      * `x <= 20` this is the `20`, and on `y > 0` it is `y`.
      */
-    Expr getGreaterOperand() { result = this.getSecondArgument() }
+    ExprNode getGreaterOperand() { hasChild(ct.getExpr(), ct.getSecondArgument(), e, result) }
 
     /**
      * Gets the operand on the "lesser" (or "lesser-or-equal") side
@@ -331,7 +287,7 @@ private module Impl {
      * if the overall expression evaluates to `true`; for example on
      * `x <= 20` this is `x`, and on `y > 0` it is the `0`.
      */
-    Expr getLesserOperand() { result = this.getFirstArgument() }
+    ExprNode getLesserOperand() { hasChild(ct.getExpr(), ct.getFirstArgument(), e, result) }
 
     /** Holds if this comparison is strict, i.e. `<` or `>`. */
     predicate isStrict() { strict = true }
diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaUtils.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaUtils.qll
index 7f1811c1f37..b26082b6250 100644
--- a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaUtils.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaUtils.qll
@@ -4,15 +4,32 @@
 
 private import csharp
 private import Ssa
+private import RangeUtils
 private import ConstantUtils
 
+private class ExprNode = ControlFlow::Nodes::ExprNode;
+
+/** An SSA variable. */
+class SsaVariable extends Definition {
+  /** Gets a read of this SSA variable. */
+  ExprNode getAUse() { exists(this.getAReadAtNode(result)) }
+}
+
+/** Gets a node that reads `src` via an SSA explicit definition. */
+ExprNode getAnExplicitDefinitionRead(ExprNode src) {
+  exists(ExplicitDefinition def |
+    exists(def.getAReadAtNode(result)) and
+    hasChild(def.getElement(), def.getADefinition().getSource(), def.getControlFlowNode(), src)
+  )
+}
+
 /**
  * Gets an expression that equals `v - delta`.
  */
-Expr ssaRead(Definition v, int delta) {
-  result = v.getARead() and delta = 0
+ExprNode ssaRead(Definition v, int delta) {
+  exists(v.getAReadAtNode(result)) and delta = 0
   or
-  exists(AddExpr add, int d1, ConstantIntegerExpr c |
+  exists(ExprNode::AddExpr add, int d1, ConstantIntegerExpr c |
     result = add and
     delta = d1 - c.getIntValue()
   |
@@ -21,22 +38,22 @@ Expr ssaRead(Definition v, int delta) {
     add.getRightOperand() = ssaRead(v, d1) and add.getLeftOperand() = c
   )
   or
-  exists(SubExpr sub, int d1, ConstantIntegerExpr c |
+  exists(ExprNode::SubExpr sub, int d1, ConstantIntegerExpr c |
     result = sub and
     sub.getLeftOperand() = ssaRead(v, d1) and
     sub.getRightOperand() = c and
     delta = d1 + c.getIntValue()
   )
   or
-  v.(ExplicitDefinition).getADefinition().getExpr().(PreIncrExpr) = result and delta = 0
+  v.(ExplicitDefinition).getControlFlowNode().(ExprNode::PreIncrExpr) = result and delta = 0
   or
-  v.(ExplicitDefinition).getADefinition().getExpr().(PreDecrExpr) = result and delta = 0
+  v.(ExplicitDefinition).getControlFlowNode().(ExprNode::PreDecrExpr) = result and delta = 0
   or
-  v.(ExplicitDefinition).getADefinition().getExpr().(PostIncrExpr) = result and delta = 1 // x++ === ++x - 1
+  v.(ExplicitDefinition).getControlFlowNode().(ExprNode::PostIncrExpr) = result and delta = 1 // x++ === ++x - 1
   or
-  v.(ExplicitDefinition).getADefinition().getExpr().(PostDecrExpr) = result and delta = -1 // x-- === --x + 1
+  v.(ExplicitDefinition).getControlFlowNode().(ExprNode::PostDecrExpr) = result and delta = -1 // x-- === --x + 1
   or
-  v.(ExplicitDefinition).getADefinition().getExpr().(Assignment) = result and delta = 0
+  v.(ExplicitDefinition).getControlFlowNode().(ExprNode::Assignment) = result and delta = 0
   or
-  result.(AssignExpr).getRValue() = ssaRead(v, delta)
+  result.(ExprNode::AssignExpr).getRValue() = ssaRead(v, delta)
 }
diff --git a/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.cs b/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.cs
index 8c55e74372b..a10354cbbe9 100644
--- a/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.cs
+++ b/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.cs
@@ -55,7 +55,7 @@ class ModulusAnalysis
         {
             j = i * 8 + 7;
         }
-        System.Console.WriteLine(j); // congruent 3 mod 4 or 7 mod 8
+        System.Console.WriteLine(j); // congruent 3 mod 4 (cond = true) or 7 mod 8 (cond = false)
 
         if (cond)
         {
@@ -78,7 +78,18 @@ class ModulusAnalysis
         }
     }
 
+    void For(int cap)
+    {
+        for (var i = 0; i < cap; i++)
+            System.Console.WriteLine(i);
+
+        for (var j = 0; j < cap; j += 1)
+            System.Console.WriteLine(j);
+
+        for (var k = 0; k < cap; k += 3)
+            System.Console.WriteLine(k); // congruent 0 mod 3
+    }
 
 
-    int[] GetArray(){ return new int[42]; }
+    int[] GetArray() { return new int[42]; }
 }
\ No newline at end of file
diff --git a/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.expected b/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.expected
index c7bacd76943..8c2f3b67680 100644
--- a/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.expected
+++ b/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.expected
@@ -33,82 +33,106 @@
 | ModulusAnalysis.cs:25:42:25:44 | access to local variable mul | 0 | 3 | 42 |
 | ModulusAnalysis.cs:25:42:25:44 | access to local variable mul | SSA def(mul) | 0 | 0 |
 | ModulusAnalysis.cs:29:17:31:23 | ... ? ... : ... | 0 | 3 | 4 |
-| ModulusAnalysis.cs:30:15:30:15 | access to parameter i | SSA param(i) | 0 | 0 |
-| ModulusAnalysis.cs:30:15:30:19 | ... * ... | 0 | 0 | 4 |
-| ModulusAnalysis.cs:30:15:30:23 | ... + ... | 0 | 3 | 4 |
-| ModulusAnalysis.cs:30:19:30:19 | 4 | 0 | 4 | 0 |
-| ModulusAnalysis.cs:30:23:30:23 | 3 | 0 | 3 | 0 |
-| ModulusAnalysis.cs:31:15:31:15 | access to parameter i | SSA param(i) | 0 | 0 |
-| ModulusAnalysis.cs:31:15:31:19 | ... * ... | 0 | 0 | 8 |
-| ModulusAnalysis.cs:31:15:31:23 | ... + ... | 0 | 7 | 8 |
-| ModulusAnalysis.cs:31:19:31:19 | 8 | 0 | 8 | 0 |
-| ModulusAnalysis.cs:31:23:31:23 | 7 | 0 | 7 | 0 |
-| ModulusAnalysis.cs:32:34:32:34 | access to local variable j | 0 | 3 | 4 |
-| ModulusAnalysis.cs:32:34:32:34 | access to local variable j | [cond (line 9): false] SSA def(j) | 0 | 0 |
-| ModulusAnalysis.cs:32:34:32:34 | access to local variable j | [cond (line 9): true] SSA def(j) | 0 | 0 |
-| ModulusAnalysis.cs:34:13:34:13 | access to parameter x | SSA param(x) | 0 | 0 |
-| ModulusAnalysis.cs:34:17:34:18 | access to constant c1 | 0 | 42 | 0 |
-| ModulusAnalysis.cs:34:17:34:18 | access to constant c1 | SSA entry def(ModulusAnalysis.c1) | 0 | 0 |
-| ModulusAnalysis.cs:34:23:34:23 | 3 | 0 | 3 | 0 |
-| ModulusAnalysis.cs:34:28:34:28 | access to parameter y | SSA param(y) | 0 | 0 |
-| ModulusAnalysis.cs:34:32:34:33 | access to constant c1 | 0 | 42 | 0 |
-| ModulusAnalysis.cs:34:32:34:33 | access to constant c1 | SSA entry def(ModulusAnalysis.c1) | 0 | 0 |
-| ModulusAnalysis.cs:34:38:34:38 | 7 | 0 | 7 | 0 |
-| ModulusAnalysis.cs:36:38:36:38 | access to parameter x | 0 | 3 | 42 |
-| ModulusAnalysis.cs:36:38:36:38 | access to parameter x | SSA param(x) | 0 | 0 |
-| ModulusAnalysis.cs:36:38:36:42 | ... + ... | 0 | 10 | 42 |
-| ModulusAnalysis.cs:36:38:36:42 | ... + ... | SSA param(x) | 7 | 42 |
-| ModulusAnalysis.cs:36:38:36:42 | ... + ... | SSA param(y) | 3 | 42 |
-| ModulusAnalysis.cs:36:42:36:42 | access to parameter y | 0 | 7 | 42 |
-| ModulusAnalysis.cs:36:42:36:42 | access to parameter y | SSA param(y) | 0 | 0 |
-| ModulusAnalysis.cs:39:13:39:13 | access to parameter x | SSA param(x) | 0 | 0 |
-| ModulusAnalysis.cs:39:17:39:18 | access to constant c1 | 0 | 42 | 0 |
-| ModulusAnalysis.cs:39:17:39:18 | access to constant c1 | SSA entry def(ModulusAnalysis.c1) | 0 | 0 |
-| ModulusAnalysis.cs:39:23:39:23 | 3 | 0 | 3 | 0 |
-| ModulusAnalysis.cs:39:28:39:28 | access to parameter y | SSA param(y) | 0 | 0 |
-| ModulusAnalysis.cs:39:32:39:33 | access to constant c1 | 0 | 42 | 0 |
-| ModulusAnalysis.cs:39:32:39:33 | access to constant c1 | SSA entry def(ModulusAnalysis.c1) | 0 | 0 |
-| ModulusAnalysis.cs:39:38:39:38 | 7 | 0 | 7 | 0 |
-| ModulusAnalysis.cs:41:38:41:38 | access to parameter x | 0 | 3 | 42 |
-| ModulusAnalysis.cs:41:38:41:38 | access to parameter x | SSA param(x) | 0 | 0 |
-| ModulusAnalysis.cs:41:38:41:42 | ... - ... | 0 | 38 | 42 |
-| ModulusAnalysis.cs:41:38:41:42 | ... - ... | SSA param(x) | 35 | 42 |
-| ModulusAnalysis.cs:41:42:41:42 | access to parameter y | 0 | 7 | 42 |
-| ModulusAnalysis.cs:41:42:41:42 | access to parameter y | SSA param(y) | 0 | 0 |
-| ModulusAnalysis.cs:44:17:44:26 | access to property Length | [cond (line 9): false] SSA untracked def(arr.Length) | 0 | 0 |
-| ModulusAnalysis.cs:44:17:44:26 | access to property Length | [cond (line 9): true] SSA untracked def(arr.Length) | 0 | 0 |
-| ModulusAnalysis.cs:44:17:44:30 | ... * ... | 0 | 0 | 4 |
-| ModulusAnalysis.cs:44:17:44:35 | ... - ... | 0 | 1 | 4 |
-| ModulusAnalysis.cs:44:30:44:30 | 4 | 0 | 4 | 0 |
-| ModulusAnalysis.cs:44:34:44:35 | 11 | 0 | 11 | 0 |
-| ModulusAnalysis.cs:45:34:45:34 | access to local variable l | 0 | 1 | 4 |
-| ModulusAnalysis.cs:45:34:45:34 | access to local variable l | [cond (line 9): false] SSA def(l) | 0 | 0 |
-| ModulusAnalysis.cs:45:34:45:34 | access to local variable l | [cond (line 9): true] SSA def(l) | 0 | 0 |
-| ModulusAnalysis.cs:47:9:47:38 | ... = ... | 0 | 1 | 4 |
-| ModulusAnalysis.cs:47:13:47:29 | access to property Length | access to property Length | 0 | 0 |
-| ModulusAnalysis.cs:47:13:47:33 | ... * ... | 0 | 0 | 4 |
-| ModulusAnalysis.cs:47:13:47:38 | ... - ... | 0 | 1 | 4 |
-| ModulusAnalysis.cs:47:33:47:33 | 4 | 0 | 4 | 0 |
-| ModulusAnalysis.cs:47:37:47:38 | 11 | 0 | 11 | 0 |
-| ModulusAnalysis.cs:48:34:48:34 | access to local variable l | 0 | 1 | 4 |
-| ModulusAnalysis.cs:48:34:48:34 | access to local variable l | [cond (line 9): false] SSA def(l) | 0 | 0 |
-| ModulusAnalysis.cs:48:34:48:34 | access to local variable l | [cond (line 9): true] SSA def(l) | 0 | 0 |
-| ModulusAnalysis.cs:52:13:52:25 | ... = ... | 0 | 3 | 4 |
-| ModulusAnalysis.cs:52:17:52:17 | access to parameter i | SSA param(i) | 0 | 0 |
-| ModulusAnalysis.cs:52:17:52:21 | ... * ... | 0 | 0 | 4 |
-| ModulusAnalysis.cs:52:17:52:25 | ... + ... | 0 | 3 | 4 |
-| ModulusAnalysis.cs:52:21:52:21 | 4 | 0 | 4 | 0 |
-| ModulusAnalysis.cs:52:25:52:25 | 3 | 0 | 3 | 0 |
-| ModulusAnalysis.cs:56:13:56:25 | ... = ... | 0 | 7 | 8 |
-| ModulusAnalysis.cs:56:17:56:17 | access to parameter i | SSA param(i) | 0 | 0 |
-| ModulusAnalysis.cs:56:17:56:21 | ... * ... | 0 | 0 | 8 |
-| ModulusAnalysis.cs:56:17:56:25 | ... + ... | 0 | 7 | 8 |
-| ModulusAnalysis.cs:56:21:56:21 | 8 | 0 | 8 | 0 |
-| ModulusAnalysis.cs:56:25:56:25 | 7 | 0 | 7 | 0 |
-| ModulusAnalysis.cs:58:34:58:34 | access to local variable j | 0 | 3 | 4 |
-| ModulusAnalysis.cs:58:34:58:34 | access to local variable j | 0 | 7 | 8 |
-| ModulusAnalysis.cs:58:34:58:34 | access to local variable j | [cond (line 9): false] SSA def(j) | 0 | 0 |
-| ModulusAnalysis.cs:58:34:58:34 | access to local variable j | [cond (line 9): true] SSA def(j) | 0 | 0 |
+| ModulusAnalysis.cs:30:15:30:15 | [cond (line 9): true] access to parameter i | SSA param(i) | 0 | 0 |
+| ModulusAnalysis.cs:30:15:30:19 | [cond (line 9): true] ... * ... | 0 | 0 | 4 |
+| ModulusAnalysis.cs:30:15:30:23 | [cond (line 9): true] ... + ... | 0 | 3 | 4 |
+| ModulusAnalysis.cs:30:19:30:19 | [cond (line 9): true] 4 | 0 | 4 | 0 |
+| ModulusAnalysis.cs:30:23:30:23 | [cond (line 9): true] 3 | 0 | 3 | 0 |
+| ModulusAnalysis.cs:31:15:31:15 | [cond (line 9): false] access to parameter i | SSA param(i) | 0 | 0 |
+| ModulusAnalysis.cs:31:15:31:19 | [cond (line 9): false] ... * ... | 0 | 0 | 8 |
+| ModulusAnalysis.cs:31:15:31:23 | [cond (line 9): false] ... + ... | 0 | 7 | 8 |
+| ModulusAnalysis.cs:31:19:31:19 | [cond (line 9): false] 8 | 0 | 8 | 0 |
+| ModulusAnalysis.cs:31:23:31:23 | [cond (line 9): false] 7 | 0 | 7 | 0 |
+| ModulusAnalysis.cs:32:34:32:34 | [cond (line 9): false] access to local variable j | 0 | 3 | 4 |
+| ModulusAnalysis.cs:32:34:32:34 | [cond (line 9): false] access to local variable j | [cond (line 9): false] SSA def(j) | 0 | 0 |
+| ModulusAnalysis.cs:32:34:32:34 | [cond (line 9): true] access to local variable j | 0 | 3 | 4 |
+| ModulusAnalysis.cs:32:34:32:34 | [cond (line 9): true] access to local variable j | [cond (line 9): true] SSA def(j) | 0 | 0 |
+| ModulusAnalysis.cs:34:13:34:13 | [cond (line 9): false] access to parameter x | SSA param(x) | 0 | 0 |
+| ModulusAnalysis.cs:34:13:34:13 | [cond (line 9): true] access to parameter x | SSA param(x) | 0 | 0 |
+| ModulusAnalysis.cs:34:17:34:18 | [cond (line 9): false] access to constant c1 | 0 | 42 | 0 |
+| ModulusAnalysis.cs:34:17:34:18 | [cond (line 9): false] access to constant c1 | SSA entry def(ModulusAnalysis.c1) | 0 | 0 |
+| ModulusAnalysis.cs:34:17:34:18 | [cond (line 9): true] access to constant c1 | 0 | 42 | 0 |
+| ModulusAnalysis.cs:34:17:34:18 | [cond (line 9): true] access to constant c1 | SSA entry def(ModulusAnalysis.c1) | 0 | 0 |
+| ModulusAnalysis.cs:34:23:34:23 | [cond (line 9): false] 3 | 0 | 3 | 0 |
+| ModulusAnalysis.cs:34:23:34:23 | [cond (line 9): true] 3 | 0 | 3 | 0 |
+| ModulusAnalysis.cs:34:28:34:28 | [cond (line 9): false] access to parameter y | SSA param(y) | 0 | 0 |
+| ModulusAnalysis.cs:34:28:34:28 | [cond (line 9): true] access to parameter y | SSA param(y) | 0 | 0 |
+| ModulusAnalysis.cs:34:32:34:33 | [cond (line 9): false] access to constant c1 | 0 | 42 | 0 |
+| ModulusAnalysis.cs:34:32:34:33 | [cond (line 9): false] access to constant c1 | SSA entry def(ModulusAnalysis.c1) | 0 | 0 |
+| ModulusAnalysis.cs:34:32:34:33 | [cond (line 9): true] access to constant c1 | 0 | 42 | 0 |
+| ModulusAnalysis.cs:34:32:34:33 | [cond (line 9): true] access to constant c1 | SSA entry def(ModulusAnalysis.c1) | 0 | 0 |
+| ModulusAnalysis.cs:34:38:34:38 | [cond (line 9): false] 7 | 0 | 7 | 0 |
+| ModulusAnalysis.cs:34:38:34:38 | [cond (line 9): true] 7 | 0 | 7 | 0 |
+| ModulusAnalysis.cs:36:38:36:38 | [cond (line 9): false] access to parameter x | SSA param(x) | 0 | 0 |
+| ModulusAnalysis.cs:36:38:36:38 | [cond (line 9): true] access to parameter x | SSA param(x) | 0 | 0 |
+| ModulusAnalysis.cs:36:42:36:42 | [cond (line 9): false] access to parameter y | SSA param(y) | 0 | 0 |
+| ModulusAnalysis.cs:36:42:36:42 | [cond (line 9): true] access to parameter y | SSA param(y) | 0 | 0 |
+| ModulusAnalysis.cs:39:13:39:13 | [cond (line 9): false] access to parameter x | SSA param(x) | 0 | 0 |
+| ModulusAnalysis.cs:39:13:39:13 | [cond (line 9): true] access to parameter x | SSA param(x) | 0 | 0 |
+| ModulusAnalysis.cs:39:17:39:18 | [cond (line 9): false] access to constant c1 | 0 | 42 | 0 |
+| ModulusAnalysis.cs:39:17:39:18 | [cond (line 9): false] access to constant c1 | SSA entry def(ModulusAnalysis.c1) | 0 | 0 |
+| ModulusAnalysis.cs:39:17:39:18 | [cond (line 9): true] access to constant c1 | 0 | 42 | 0 |
+| ModulusAnalysis.cs:39:17:39:18 | [cond (line 9): true] access to constant c1 | SSA entry def(ModulusAnalysis.c1) | 0 | 0 |
+| ModulusAnalysis.cs:39:23:39:23 | [cond (line 9): false] 3 | 0 | 3 | 0 |
+| ModulusAnalysis.cs:39:23:39:23 | [cond (line 9): true] 3 | 0 | 3 | 0 |
+| ModulusAnalysis.cs:39:28:39:28 | [cond (line 9): false] access to parameter y | SSA param(y) | 0 | 0 |
+| ModulusAnalysis.cs:39:28:39:28 | [cond (line 9): true] access to parameter y | SSA param(y) | 0 | 0 |
+| ModulusAnalysis.cs:39:32:39:33 | [cond (line 9): false] access to constant c1 | 0 | 42 | 0 |
+| ModulusAnalysis.cs:39:32:39:33 | [cond (line 9): false] access to constant c1 | SSA entry def(ModulusAnalysis.c1) | 0 | 0 |
+| ModulusAnalysis.cs:39:32:39:33 | [cond (line 9): true] access to constant c1 | 0 | 42 | 0 |
+| ModulusAnalysis.cs:39:32:39:33 | [cond (line 9): true] access to constant c1 | SSA entry def(ModulusAnalysis.c1) | 0 | 0 |
+| ModulusAnalysis.cs:39:38:39:38 | [cond (line 9): false] 7 | 0 | 7 | 0 |
+| ModulusAnalysis.cs:39:38:39:38 | [cond (line 9): true] 7 | 0 | 7 | 0 |
+| ModulusAnalysis.cs:41:38:41:38 | [cond (line 9): false] access to parameter x | SSA param(x) | 0 | 0 |
+| ModulusAnalysis.cs:41:38:41:38 | [cond (line 9): true] access to parameter x | SSA param(x) | 0 | 0 |
+| ModulusAnalysis.cs:41:42:41:42 | [cond (line 9): false] access to parameter y | SSA param(y) | 0 | 0 |
+| ModulusAnalysis.cs:41:42:41:42 | [cond (line 9): true] access to parameter y | SSA param(y) | 0 | 0 |
+| ModulusAnalysis.cs:44:17:44:26 | [cond (line 9): false] access to property Length | [cond (line 9): false] access to property Length | 0 | 0 |
+| ModulusAnalysis.cs:44:17:44:26 | [cond (line 9): true] access to property Length | [cond (line 9): true] access to property Length | 0 | 0 |
+| ModulusAnalysis.cs:44:17:44:30 | [cond (line 9): false] ... * ... | 0 | 0 | 4 |
+| ModulusAnalysis.cs:44:17:44:30 | [cond (line 9): true] ... * ... | 0 | 0 | 4 |
+| ModulusAnalysis.cs:44:17:44:35 | [cond (line 9): false] ... - ... | 0 | 1 | 4 |
+| ModulusAnalysis.cs:44:17:44:35 | [cond (line 9): true] ... - ... | 0 | 1 | 4 |
+| ModulusAnalysis.cs:44:30:44:30 | [cond (line 9): false] 4 | 0 | 4 | 0 |
+| ModulusAnalysis.cs:44:30:44:30 | [cond (line 9): true] 4 | 0 | 4 | 0 |
+| ModulusAnalysis.cs:44:34:44:35 | [cond (line 9): false] 11 | 0 | 11 | 0 |
+| ModulusAnalysis.cs:44:34:44:35 | [cond (line 9): true] 11 | 0 | 11 | 0 |
+| ModulusAnalysis.cs:45:34:45:34 | [cond (line 9): false] access to local variable l | 0 | 1 | 4 |
+| ModulusAnalysis.cs:45:34:45:34 | [cond (line 9): false] access to local variable l | [cond (line 9): false] SSA def(l) | 0 | 0 |
+| ModulusAnalysis.cs:45:34:45:34 | [cond (line 9): true] access to local variable l | 0 | 1 | 4 |
+| ModulusAnalysis.cs:45:34:45:34 | [cond (line 9): true] access to local variable l | [cond (line 9): true] SSA def(l) | 0 | 0 |
+| ModulusAnalysis.cs:47:9:47:38 | [cond (line 9): false] ... = ... | 0 | 1 | 4 |
+| ModulusAnalysis.cs:47:9:47:38 | [cond (line 9): true] ... = ... | 0 | 1 | 4 |
+| ModulusAnalysis.cs:47:13:47:29 | [cond (line 9): false] access to property Length | [cond (line 9): false] access to property Length | 0 | 0 |
+| ModulusAnalysis.cs:47:13:47:29 | [cond (line 9): true] access to property Length | [cond (line 9): true] access to property Length | 0 | 0 |
+| ModulusAnalysis.cs:47:13:47:33 | [cond (line 9): false] ... * ... | 0 | 0 | 4 |
+| ModulusAnalysis.cs:47:13:47:33 | [cond (line 9): true] ... * ... | 0 | 0 | 4 |
+| ModulusAnalysis.cs:47:13:47:38 | [cond (line 9): false] ... - ... | 0 | 1 | 4 |
+| ModulusAnalysis.cs:47:13:47:38 | [cond (line 9): true] ... - ... | 0 | 1 | 4 |
+| ModulusAnalysis.cs:47:33:47:33 | [cond (line 9): false] 4 | 0 | 4 | 0 |
+| ModulusAnalysis.cs:47:33:47:33 | [cond (line 9): true] 4 | 0 | 4 | 0 |
+| ModulusAnalysis.cs:47:37:47:38 | [cond (line 9): false] 11 | 0 | 11 | 0 |
+| ModulusAnalysis.cs:47:37:47:38 | [cond (line 9): true] 11 | 0 | 11 | 0 |
+| ModulusAnalysis.cs:48:34:48:34 | [cond (line 9): false] access to local variable l | 0 | 1 | 4 |
+| ModulusAnalysis.cs:48:34:48:34 | [cond (line 9): false] access to local variable l | [cond (line 9): false] SSA def(l) | 0 | 0 |
+| ModulusAnalysis.cs:48:34:48:34 | [cond (line 9): true] access to local variable l | 0 | 1 | 4 |
+| ModulusAnalysis.cs:48:34:48:34 | [cond (line 9): true] access to local variable l | [cond (line 9): true] SSA def(l) | 0 | 0 |
+| ModulusAnalysis.cs:52:13:52:25 | [cond (line 9): true] ... = ... | 0 | 3 | 4 |
+| ModulusAnalysis.cs:52:17:52:17 | [cond (line 9): true] access to parameter i | SSA param(i) | 0 | 0 |
+| ModulusAnalysis.cs:52:17:52:21 | [cond (line 9): true] ... * ... | 0 | 0 | 4 |
+| ModulusAnalysis.cs:52:17:52:25 | [cond (line 9): true] ... + ... | 0 | 3 | 4 |
+| ModulusAnalysis.cs:52:21:52:21 | [cond (line 9): true] 4 | 0 | 4 | 0 |
+| ModulusAnalysis.cs:52:25:52:25 | [cond (line 9): true] 3 | 0 | 3 | 0 |
+| ModulusAnalysis.cs:56:13:56:25 | [cond (line 9): false] ... = ... | 0 | 7 | 8 |
+| ModulusAnalysis.cs:56:17:56:17 | [cond (line 9): false] access to parameter i | SSA param(i) | 0 | 0 |
+| ModulusAnalysis.cs:56:17:56:21 | [cond (line 9): false] ... * ... | 0 | 0 | 8 |
+| ModulusAnalysis.cs:56:17:56:25 | [cond (line 9): false] ... + ... | 0 | 7 | 8 |
+| ModulusAnalysis.cs:56:21:56:21 | [cond (line 9): false] 8 | 0 | 8 | 0 |
+| ModulusAnalysis.cs:56:25:56:25 | [cond (line 9): false] 7 | 0 | 7 | 0 |
+| ModulusAnalysis.cs:58:34:58:34 | [cond (line 9): false] access to local variable j | 0 | 7 | 8 |
+| ModulusAnalysis.cs:58:34:58:34 | [cond (line 9): false] access to local variable j | [cond (line 9): false] SSA def(j) | 0 | 0 |
+| ModulusAnalysis.cs:58:34:58:34 | [cond (line 9): true] access to local variable j | 0 | 3 | 4 |
+| ModulusAnalysis.cs:58:34:58:34 | [cond (line 9): true] access to local variable j | [cond (line 9): true] SSA def(j) | 0 | 0 |
 | ModulusAnalysis.cs:62:38:62:38 | access to local variable j | 0 | 3 | 4 |
 | ModulusAnalysis.cs:62:38:62:38 | access to local variable j | [cond (line 9): true] SSA def(j) | 0 | 0 |
 | ModulusAnalysis.cs:66:38:66:38 | access to local variable j | 0 | 7 | 8 |
@@ -135,4 +159,36 @@
 | ModulusAnalysis.cs:75:25:75:25 | 3 | 0 | 3 | 0 |
 | ModulusAnalysis.cs:77:38:77:38 | access to parameter x | 0 | 3 | 16 |
 | ModulusAnalysis.cs:77:38:77:38 | access to parameter x | SSA param(x) | 0 | 0 |
-| ModulusAnalysis.cs:83:38:83:39 | 42 | 0 | 42 | 0 |
+| ModulusAnalysis.cs:83:22:83:22 | 0 | 0 | 0 | 0 |
+| ModulusAnalysis.cs:83:25:83:25 | access to local variable i | SSA phi(i) | 0 | 0 |
+| ModulusAnalysis.cs:83:29:83:31 | access to parameter cap | SSA param(cap) | 0 | 0 |
+| ModulusAnalysis.cs:83:34:83:34 | access to local variable i | SSA phi(i) | 0 | 0 |
+| ModulusAnalysis.cs:83:34:83:36 | ...++ | SSA phi(i) | 0 | 0 |
+| ModulusAnalysis.cs:84:38:84:38 | access to local variable i | SSA phi(i) | 0 | 0 |
+| ModulusAnalysis.cs:86:22:86:22 | 0 | 0 | 0 | 0 |
+| ModulusAnalysis.cs:86:25:86:25 | access to local variable j | SSA phi(j) | 0 | 0 |
+| ModulusAnalysis.cs:86:29:86:31 | access to parameter cap | SSA param(cap) | 0 | 0 |
+| ModulusAnalysis.cs:86:34:86:34 | access to local variable j | SSA phi(j) | 0 | 0 |
+| ModulusAnalysis.cs:86:34:86:39 | ... + ... | SSA phi(j) | 1 | 0 |
+| ModulusAnalysis.cs:86:34:86:39 | ... = ... | SSA phi(j) | 1 | 0 |
+| ModulusAnalysis.cs:86:39:86:39 | 1 | 0 | 1 | 0 |
+| ModulusAnalysis.cs:87:38:87:38 | access to local variable j | SSA phi(j) | 0 | 0 |
+| ModulusAnalysis.cs:89:22:89:22 | 0 | 0 | 0 | 0 |
+| ModulusAnalysis.cs:89:25:89:25 | access to local variable k | 0 | 0 | 3 |
+| ModulusAnalysis.cs:89:25:89:25 | access to local variable k | SSA def(k) | 0 | 3 |
+| ModulusAnalysis.cs:89:25:89:25 | access to local variable k | SSA phi(k) | 0 | 0 |
+| ModulusAnalysis.cs:89:29:89:31 | access to parameter cap | SSA param(cap) | 0 | 0 |
+| ModulusAnalysis.cs:89:34:89:34 | access to local variable k | 0 | 0 | 3 |
+| ModulusAnalysis.cs:89:34:89:34 | access to local variable k | SSA def(k) | 0 | 3 |
+| ModulusAnalysis.cs:89:34:89:34 | access to local variable k | SSA phi(k) | 0 | 0 |
+| ModulusAnalysis.cs:89:34:89:39 | ... + ... | 0 | 0 | 3 |
+| ModulusAnalysis.cs:89:34:89:39 | ... + ... | SSA def(k) | 0 | 3 |
+| ModulusAnalysis.cs:89:34:89:39 | ... + ... | SSA phi(k) | 3 | 0 |
+| ModulusAnalysis.cs:89:34:89:39 | ... = ... | 0 | 0 | 3 |
+| ModulusAnalysis.cs:89:34:89:39 | ... = ... | SSA def(k) | 0 | 3 |
+| ModulusAnalysis.cs:89:34:89:39 | ... = ... | SSA phi(k) | 3 | 0 |
+| ModulusAnalysis.cs:89:39:89:39 | 3 | 0 | 3 | 0 |
+| ModulusAnalysis.cs:90:38:90:38 | access to local variable k | 0 | 0 | 3 |
+| ModulusAnalysis.cs:90:38:90:38 | access to local variable k | SSA def(k) | 0 | 3 |
+| ModulusAnalysis.cs:90:38:90:38 | access to local variable k | SSA phi(k) | 0 | 0 |
+| ModulusAnalysis.cs:94:39:94:40 | 42 | 0 | 42 | 0 |
diff --git a/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.ql b/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.ql
index f92649fa5b2..b07608ea009 100644
--- a/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.ql
+++ b/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.ql
@@ -1,7 +1,8 @@
 import csharp
+import semmle.code.csharp.dataflow.internal.rangeanalysis.RangeUtils
 import semmle.code.csharp.dataflow.ModulusAnalysis
 import semmle.code.csharp.dataflow.Bound
 
-from Expr e, Bound b, int delta, int mod
+from ControlFlow::Nodes::ExprNode e, Bound b, int delta, int mod
 where exprModulus(e, b, delta, mod)
 select e, b.toString(), delta, mod
diff --git a/csharp/ql/test/library-tests/dataflow/signanalysis/MissingSign.ql b/csharp/ql/test/library-tests/dataflow/signanalysis/MissingSign.ql
index 836980829a3..70f9af36494 100644
--- a/csharp/ql/test/library-tests/dataflow/signanalysis/MissingSign.ql
+++ b/csharp/ql/test/library-tests/dataflow/signanalysis/MissingSign.ql
@@ -1,10 +1,10 @@
 import csharp
-import semmle.code.csharp.dataflow.SignAnalysis
+import semmle.code.csharp.dataflow.internal.rangeanalysis.SignAnalysisCommon
 
-from Expr e
+from ControlFlow::Nodes::ExprNode e
 where
   not exists(exprSign(e)) and
-  not e instanceof TypeAccess and
+  not e.getExpr() instanceof TypeAccess and
   (
     e.getType() instanceof CharType or
     e.getType() instanceof IntegralType or
diff --git a/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.cs b/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.cs
index de8f52d77f3..8f094033bb7 100644
--- a/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.cs
+++ b/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.cs
@@ -464,6 +464,28 @@ class SignAnalysis
         x++;
         System.Console.WriteLine(x); // strictly positive
     }
+
+    void Splitting1(bool b)
+    {
+        var x = b ? 1 : -1;
+        if (b)
+            System.Console.WriteLine(x); // strictly positive [MISSING]
+        else
+            System.Console.WriteLine(x); // strictly negative [MISSING]
+    }
+
+    void Splitting2(bool b)
+    {
+        int x;
+        if (b) x = 1; else x = -1;
+
+        System.Console.WriteLine(x); // strictly positive (b = true) or strictly negative (b = false)
+
+        if (b)
+            System.Console.WriteLine(x); // strictly positive
+        else
+            System.Console.WriteLine(x); // strictly negative
+    }
 }
 
 // semmle-extractor-options: /r:System.Linq.dll
\ No newline at end of file
diff --git a/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.expected b/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.expected
index 0e6cc20f05d..303715e1894 100644
--- a/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.expected
+++ b/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.expected
@@ -53,7 +53,6 @@
 | SignAnalysis.cs:80:17:80:17 | access to parameter i | strictlyNegative |
 | SignAnalysis.cs:81:13:81:13 | access to local variable x | strictlyNegative |
 | SignAnalysis.cs:81:13:81:18 | ... + ... | strictlyNegative |
-| SignAnalysis.cs:81:13:81:18 | ... += ... | strictlyNegative |
 | SignAnalysis.cs:81:13:81:18 | ... = ... | strictlyNegative |
 | SignAnalysis.cs:81:18:81:18 | access to parameter i | strictlyNegative |
 | SignAnalysis.cs:82:38:82:38 | access to local variable x | strictlyNegative |
@@ -90,14 +89,12 @@
 | SignAnalysis.cs:108:13:108:21 | Decimal de = ... | strictlyPositive |
 | SignAnalysis.cs:108:18:108:21 | 4.2 | strictlyPositive |
 | SignAnalysis.cs:109:34:109:35 | access to local variable de | strictlyPositive |
-| SignAnalysis.cs:110:13:110:13 | access to local variable c | positive |
 | SignAnalysis.cs:110:13:110:19 | Char c = ... | strictlyPositive |
 | SignAnalysis.cs:110:17:110:19 | a | strictlyPositive |
 | SignAnalysis.cs:111:34:111:34 | access to local variable c | strictlyPositive |
 | SignAnalysis.cs:120:9:120:10 | access to field f0 | positive |
 | SignAnalysis.cs:120:9:120:12 | ...++ | positive |
 | SignAnalysis.cs:121:34:121:35 | access to field f0 | strictlyPositive |
-| SignAnalysis.cs:122:9:122:10 | access to field f0 | positive |
 | SignAnalysis.cs:129:9:129:16 | ... = ... | strictlyNegative |
 | SignAnalysis.cs:129:14:129:16 | -... | strictlyNegative |
 | SignAnalysis.cs:129:15:129:16 | 10 | strictlyPositive |
@@ -164,8 +161,6 @@
 | SignAnalysis.cs:306:21:306:22 | -... | strictlyNegative |
 | SignAnalysis.cs:306:22:306:22 | 1 | strictlyPositive |
 | SignAnalysis.cs:309:38:309:38 | access to local variable x | strictlyNegative |
-| SignAnalysis.cs:315:13:315:15 | access to local variable min | positive |
-| SignAnalysis.cs:316:13:316:15 | access to local variable max | positive |
 | SignAnalysis.cs:316:13:316:31 | Char max = ... | strictlyPositive |
 | SignAnalysis.cs:316:19:316:31 | access to constant MaxValue | strictlyPositive |
 | SignAnalysis.cs:317:13:317:23 | Int32 c = ... | strictlyPositive |
@@ -200,7 +195,6 @@
 | SignAnalysis.cs:357:13:357:13 | access to parameter i | positive |
 | SignAnalysis.cs:359:38:359:38 | access to parameter i | strictlyPositive |
 | SignAnalysis.cs:371:38:371:38 | access to local variable y | strictlyNegative |
-| SignAnalysis.cs:377:16:377:17 | access to local variable dp | positive |
 | SignAnalysis.cs:377:16:377:22 | Single* dp = ... | positive |
 | SignAnalysis.cs:377:21:377:22 | &... | positive |
 | SignAnalysis.cs:378:18:378:19 | access to local variable dp | positive |
@@ -221,7 +215,6 @@
 | SignAnalysis.cs:414:13:414:13 | access to local variable i | strictlyPositive |
 | SignAnalysis.cs:415:31:415:31 | access to local variable i | strictlyPositive |
 | SignAnalysis.cs:424:31:424:31 | access to local variable x | strictlyNegative |
-| SignAnalysis.cs:428:19:428:19 | access to constant A | strictlyPositive |
 | SignAnalysis.cs:428:19:428:24 | ... = ... | strictlyPositive |
 | SignAnalysis.cs:428:23:428:24 | 12 | strictlyPositive |
 | SignAnalysis.cs:434:38:434:38 | access to local variable i | strictlyNegative |
@@ -229,7 +222,6 @@
 | SignAnalysis.cs:440:29:440:31 | access to parameter dst | positive |
 | SignAnalysis.cs:443:38:443:38 | access to local variable x | strictlyNegative |
 | SignAnalysis.cs:446:31:446:32 | 10 | strictlyPositive |
-| SignAnalysis.cs:448:22:448:23 | access to local variable to | positive |
 | SignAnalysis.cs:448:22:448:29 | Byte* to = ... | positive |
 | SignAnalysis.cs:448:27:448:29 | (...) ... | positive |
 | SignAnalysis.cs:450:38:450:44 | (...) ... | positive |
@@ -241,9 +233,20 @@
 | SignAnalysis.cs:457:18:457:27 | call to method Unsigned | positive |
 | SignAnalysis.cs:458:13:458:13 | access to local variable l | positive |
 | SignAnalysis.cs:460:38:460:38 | access to local variable l | strictlyPositive |
-| SignAnalysis.cs:463:14:463:14 | access to local variable x | positive |
 | SignAnalysis.cs:463:14:463:24 | UInt32 x = ... | positive |
 | SignAnalysis.cs:463:18:463:24 | (...) ... | positive |
 | SignAnalysis.cs:464:9:464:9 | access to local variable x | positive |
 | SignAnalysis.cs:464:9:464:11 | ...++ | positive |
 | SignAnalysis.cs:465:34:465:34 | access to local variable x | strictlyPositive |
+| SignAnalysis.cs:470:21:470:21 | [b (line 468): true] 1 | strictlyPositive |
+| SignAnalysis.cs:470:25:470:26 | [b (line 468): false] -... | strictlyNegative |
+| SignAnalysis.cs:470:26:470:26 | [b (line 468): false] 1 | strictlyPositive |
+| SignAnalysis.cs:480:16:480:20 | [b (line 477): true] ... = ... | strictlyPositive |
+| SignAnalysis.cs:480:20:480:20 | [b (line 477): true] 1 | strictlyPositive |
+| SignAnalysis.cs:480:28:480:33 | [b (line 477): false] ... = ... | strictlyNegative |
+| SignAnalysis.cs:480:32:480:33 | [b (line 477): false] -... | strictlyNegative |
+| SignAnalysis.cs:480:33:480:33 | [b (line 477): false] 1 | strictlyPositive |
+| SignAnalysis.cs:482:34:482:34 | [b (line 477): false] access to local variable x | strictlyNegative |
+| SignAnalysis.cs:482:34:482:34 | [b (line 477): true] access to local variable x | strictlyPositive |
+| SignAnalysis.cs:485:38:485:38 | access to local variable x | strictlyPositive |
+| SignAnalysis.cs:487:38:487:38 | access to local variable x | strictlyNegative |
diff --git a/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.ql b/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.ql
index 4350e8f1742..5427cdc631d 100644
--- a/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.ql
+++ b/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.ql
@@ -1,7 +1,7 @@
 import csharp
 import semmle.code.csharp.dataflow.SignAnalysis
 
-string getASignString(Expr e) {
+string getASignString(ControlFlow::Nodes::ExprNode e) {
   positive(e) and
   not strictlyPositive(e) and
   result = "positive"
@@ -17,5 +17,5 @@ string getASignString(Expr e) {
   result = "strictlyNegative"
 }
 
-from Expr e
+from ControlFlow::Nodes::ExprNode e
 select e, strictconcat(string s | s = getASignString(e) | s, " ")
diff --git a/java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll b/java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll
index 2b3c3402415..2964353ce69 100644
--- a/java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll
+++ b/java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll
@@ -111,18 +111,6 @@ private predicate evenlyDivisibleExpr(Expr e, int factor) {
   )
 }
 
-/**
- * Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
- * in an arbitrary 1-based numbering of the input edges to `phi`.
- */
-private predicate rankedPhiInput(
-  SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r
-) {
-  edge.phiInput(phi, inp) and
-  edge =
-    rank[r](SsaReadPositionPhiInputEdge e | e.phiInput(phi, _) | e order by getId(e.getOrigBlock()))
-}
-
 /**
  * Holds if `rix` is the number of input edges to `phi`.
  */
diff --git a/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
index 374cb102e0a..fc17dbfd979 100644
--- a/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
+++ b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
@@ -4,6 +4,7 @@ module Private {
   private import semmle.code.java.dataflow.RangeUtils as RU
   private import semmle.code.java.controlflow.Guards as G
   private import semmle.code.java.controlflow.BasicBlocks as BB
+  private import SsaReadPositionCommon
 
   class BasicBlock = BB::BasicBlock;
 
@@ -115,5 +116,19 @@ module Private {
 
   private predicate idOf(BasicBlock x, int y) = equivalenceRelation(id/2)(x, y)
 
-  int getId(BasicBlock bb) { idOf(bb, result) }
+  private int getId(BasicBlock bb) { idOf(bb, result) }
+
+  /**
+   * Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
+   * in an arbitrary 1-based numbering of the input edges to `phi`.
+   */
+  predicate rankedPhiInput(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r) {
+    edge.phiInput(phi, inp) and
+    edge =
+      rank[r](SsaReadPositionPhiInputEdge e |
+        e.phiInput(phi, _)
+      |
+        e order by getId(e.getOrigBlock())
+      )
+  }
 }
diff --git a/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll
index d00a38bac73..06af17094a5 100644
--- a/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll
+++ b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll
@@ -51,7 +51,7 @@ private predicate unknownSign(Expr e) {
     or
     exists(CastExpr cast, Type fromtyp |
       cast = e and
-      fromtyp = cast.getExpr().getType() and
+      fromtyp = cast.getSourceType() and
       not fromtyp instanceof NumericOrCharType
     )
     or
diff --git a/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll
index 4c3c42b76fe..8c4eb2a1144 100644
--- a/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll
+++ b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll
@@ -27,7 +27,10 @@ module Private {
 
   class LongLiteral = J::LongLiteral;
 
-  class CastExpr = J::CastExpr;
+  class CastExpr extends J::CastExpr {
+    /** Gets the source type of this cast. */
+    J::Type getSourceType() { result = this.getExpr().getType() }
+  }
 
   class Type = J::Type;
 
diff --git a/java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.expected b/java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.expected
index 597b4795fcb..c7fd9c91264 100644
--- a/java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.expected
+++ b/java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.expected
@@ -104,4 +104,32 @@
 | ModulusAnalysis.java:49:25:49:25 | 3 | 0 | 3 | 0 |
 | ModulusAnalysis.java:50:32:50:32 | x | 0 | 3 | 16 |
 | ModulusAnalysis.java:50:32:50:32 | x | SSA init(x) | 0 | 0 |
-| ModulusAnalysis.java:54:38:54:39 | 42 | 0 | 42 | 0 |
+| ModulusAnalysis.java:56:22:56:22 | 0 | 0 | 0 | 0 |
+| ModulusAnalysis.java:56:25:56:25 | i | SSA phi(i) | 0 | 0 |
+| ModulusAnalysis.java:56:29:56:31 | cap | SSA init(cap) | 0 | 0 |
+| ModulusAnalysis.java:56:34:56:34 | i | SSA phi(i) | 0 | 0 |
+| ModulusAnalysis.java:56:34:56:36 | ...++ | SSA phi(i) | 0 | 0 |
+| ModulusAnalysis.java:57:32:57:32 | i | SSA phi(i) | 0 | 0 |
+| ModulusAnalysis.java:59:22:59:22 | 0 | 0 | 0 | 0 |
+| ModulusAnalysis.java:59:25:59:25 | j | SSA phi(j) | 0 | 0 |
+| ModulusAnalysis.java:59:29:59:31 | cap | SSA init(cap) | 0 | 0 |
+| ModulusAnalysis.java:59:34:59:34 | j | SSA phi(j) | 0 | 0 |
+| ModulusAnalysis.java:59:34:59:39 | ...+=... | SSA phi(j) | 1 | 0 |
+| ModulusAnalysis.java:59:39:59:39 | 1 | 0 | 1 | 0 |
+| ModulusAnalysis.java:60:32:60:32 | j | SSA phi(j) | 0 | 0 |
+| ModulusAnalysis.java:62:22:62:22 | 0 | 0 | 0 | 0 |
+| ModulusAnalysis.java:62:25:62:25 | k | 0 | 0 | 3 |
+| ModulusAnalysis.java:62:25:62:25 | k | SSA def(k) | 0 | 3 |
+| ModulusAnalysis.java:62:25:62:25 | k | SSA phi(k) | 0 | 0 |
+| ModulusAnalysis.java:62:29:62:31 | cap | SSA init(cap) | 0 | 0 |
+| ModulusAnalysis.java:62:34:62:34 | k | 0 | 0 | 3 |
+| ModulusAnalysis.java:62:34:62:34 | k | SSA def(k) | 0 | 3 |
+| ModulusAnalysis.java:62:34:62:34 | k | SSA phi(k) | 0 | 0 |
+| ModulusAnalysis.java:62:34:62:39 | ...+=... | 0 | 0 | 3 |
+| ModulusAnalysis.java:62:34:62:39 | ...+=... | SSA def(k) | 0 | 3 |
+| ModulusAnalysis.java:62:34:62:39 | ...+=... | SSA phi(k) | 3 | 0 |
+| ModulusAnalysis.java:62:39:62:39 | 3 | 0 | 3 | 0 |
+| ModulusAnalysis.java:63:32:63:32 | k | 0 | 0 | 3 |
+| ModulusAnalysis.java:63:32:63:32 | k | SSA def(k) | 0 | 3 |
+| ModulusAnalysis.java:63:32:63:32 | k | SSA phi(k) | 0 | 0 |
+| ModulusAnalysis.java:66:38:66:39 | 42 | 0 | 42 | 0 |
diff --git a/java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.java b/java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.java
index 5b251894166..7c322051229 100644
--- a/java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.java
+++ b/java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.java
@@ -51,5 +51,17 @@ class ModulusAnalysis
         }
     }
 
+    void loops(int cap)
+    {
+        for (int i = 0; i < cap; i++)
+            System.out.println(i);
+
+        for (int j = 0; j < cap; j += 1)
+            System.out.println(j);
+
+        for (int k = 0; k < cap; k += 3)
+            System.out.println(k); // congruent 0 mod 3
+    }
+
     int[] getArray(){ return new int[42]; }
 }
\ No newline at end of file