diff --git a/config/identical-files.json b/config/identical-files.json
index e0a4e8dabf4..9be5c0d0dd2 100644
--- a/config/identical-files.json
+++ b/config/identical-files.json
@@ -62,6 +62,14 @@
     "java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll",
     "csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll"
   ],
+  "Bound Java/C#": [
+    "java/ql/src/semmle/code/java/dataflow/Bound.qll",
+    "csharp/ql/src/semmle/code/csharp/dataflow/Bound.qll"
+  ],
+  "ModulusAnalysis Java/C#": [
+    "java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll",
+    "csharp/ql/src/semmle/code/csharp/dataflow/ModulusAnalysis.qll"
+  ],
   "C++ SubBasicBlocks": [
     "cpp/ql/src/semmle/code/cpp/controlflow/SubBasicBlocks.qll",
     "cpp/ql/src/semmle/code/cpp/dataflow/internal/SubBasicBlocks.qll"
diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/Bound.qll b/csharp/ql/src/semmle/code/csharp/dataflow/Bound.qll
new file mode 100644
index 00000000000..b129203db70
--- /dev/null
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/Bound.qll
@@ -0,0 +1,78 @@
+/**
+ * Provides classes for representing abstract bounds for use in, for example, range analysis.
+ */
+
+private import internal.rangeanalysis.BoundSpecific
+
+private newtype TBound =
+  TBoundZero() or
+  TBoundSsa(SsaVariable v) { v.getSourceVariable().getType() instanceof IntegralType } or
+  TBoundExpr(Expr e) {
+    interestingExprBound(e) and
+    not exists(SsaVariable v | e = v.getAUse())
+  }
+
+/**
+ * A bound that may be inferred for an expression plus/minus an integer delta.
+ */
+abstract class Bound extends TBound {
+  /** Gets a textual representation of this bound. */
+  abstract string toString();
+
+  /** Gets an expression that equals this bound plus `delta`. */
+  abstract Expr getExpr(int delta);
+
+  /** Gets an expression that equals this bound. */
+  Expr getExpr() { result = getExpr(0) }
+
+  /**
+   * Holds if this element is at the specified location.
+   * The location spans column `sc` of line `sl` to
+   * column `ec` of line `el` in file `path`.
+   * For more information, see
+   * [Locations](https://help.semmle.com/QL/learn-ql/ql/locations.html).
+   */
+  predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
+    path = "" and sl = 0 and sc = 0 and el = 0 and ec = 0
+  }
+}
+
+/**
+ * The bound that corresponds to the integer 0. This is used to represent all
+ * integer bounds as bounds are always accompanied by an added integer delta.
+ */
+class ZeroBound extends Bound, TBoundZero {
+  override string toString() { result = "0" }
+
+  override Expr getExpr(int delta) { result.(ConstantIntegerExpr).getIntValue() = delta }
+}
+
+/**
+ * A bound corresponding to the value of an SSA variable.
+ */
+class SsaBound extends Bound, TBoundSsa {
+  /** Gets the SSA variable that equals this bound. */
+  SsaVariable getSsa() { this = TBoundSsa(result) }
+
+  override string toString() { result = getSsa().toString() }
+
+  override Expr getExpr(int delta) { result = getSsa().getAUse() and delta = 0 }
+
+  override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
+    getSsa().getLocation().hasLocationInfo(path, sl, sc, el, ec)
+  }
+}
+
+/**
+ * A bound that corresponds to the value of a specific expression that might be
+ * interesting, but isn't otherwise represented by the value of an SSA variable.
+ */
+class ExprBound extends Bound, TBoundExpr {
+  override string toString() { result = getExpr().toString() }
+
+  override Expr getExpr(int delta) { this = TBoundExpr(result) and delta = 0 }
+
+  override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
+    getExpr().getLocation().hasLocationInfo(path, sl, sc, el, ec)
+  }
+}
diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/ModulusAnalysis.qll b/csharp/ql/src/semmle/code/csharp/dataflow/ModulusAnalysis.qll
new file mode 100644
index 00000000000..2b3c3402415
--- /dev/null
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/ModulusAnalysis.qll
@@ -0,0 +1,302 @@
+/**
+ * Provides inferences of the form: `e` equals `b + v` modulo `m` where `e` is
+ * an expression, `b` is a `Bound` (typically zero or the value of an SSA
+ * variable), and `v` is an integer in the range `[0 .. m-1]`.
+ */
+
+private import internal.rangeanalysis.ModulusAnalysisSpecific::Private
+private import Bound
+private import internal.rangeanalysis.SsaReadPositionCommon
+
+/**
+ * Holds if `e + delta` equals `v` at `pos`.
+ */
+private predicate valueFlowStepSsa(SsaVariable v, SsaReadPosition pos, Expr e, int delta) {
+  ssaUpdateStep(v, e, delta) and pos.hasReadOfVar(v)
+  or
+  exists(Guard guard, boolean testIsTrue |
+    pos.hasReadOfVar(v) and
+    guard = eqFlowCond(v, e, delta, true, testIsTrue) and
+    guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
+  )
+}
+
+/**
+ * Holds if `add` is the addition of `larg` and `rarg`, neither of which are
+ * `ConstantIntegerExpr`s.
+ */
+private predicate nonConstAddition(Expr add, Expr larg, Expr rarg) {
+  exists(AddExpr a | a = add |
+    larg = a.getLhs() and
+    rarg = a.getRhs()
+  ) and
+  not larg instanceof ConstantIntegerExpr and
+  not rarg instanceof ConstantIntegerExpr
+}
+
+/**
+ * Holds if `sub` is the subtraction of `larg` and `rarg`, where `rarg` is not
+ * a `ConstantIntegerExpr`.
+ */
+private predicate nonConstSubtraction(Expr sub, Expr larg, Expr rarg) {
+  exists(SubExpr s | s = sub |
+    larg = s.getLhs() and
+    rarg = s.getRhs()
+  ) and
+  not rarg instanceof ConstantIntegerExpr
+}
+
+/** Gets an expression that is the remainder modulo `mod` of `arg`. */
+private Expr modExpr(Expr arg, int mod) {
+  exists(RemExpr rem |
+    result = rem and
+    arg = rem.getLeftOperand() and
+    rem.getRightOperand().(ConstantIntegerExpr).getIntValue() = mod and
+    mod >= 2
+  )
+  or
+  exists(ConstantIntegerExpr c |
+    mod = 2.pow([1 .. 30]) and
+    c.getIntValue() = mod - 1 and
+    result.(BitwiseAndExpr).hasOperands(arg, c)
+  )
+}
+
+/**
+ * Gets a guard that tests whether `v` is congruent with `val` modulo `mod` on
+ * its `testIsTrue` branch.
+ */
+private Guard moduloCheck(SsaVariable v, int val, int mod, boolean testIsTrue) {
+  exists(Expr rem, ConstantIntegerExpr c, int r, boolean polarity |
+    result.isEquality(rem, c, polarity) and
+    c.getIntValue() = r and
+    rem = modExpr(v.getAUse(), mod) and
+    (
+      testIsTrue = polarity and val = r
+      or
+      testIsTrue = polarity.booleanNot() and
+      mod = 2 and
+      val = 1 - r and
+      (r = 0 or r = 1)
+    )
+  )
+}
+
+/**
+ * Holds if a guard ensures that `v` at `pos` is congruent with `val` modulo `mod`.
+ */
+private predicate moduloGuardedRead(SsaVariable v, SsaReadPosition pos, int val, int mod) {
+  exists(Guard guard, boolean testIsTrue |
+    pos.hasReadOfVar(v) and
+    guard = moduloCheck(v, val, mod, testIsTrue) and
+    guardControlsSsaRead(guard, pos, testIsTrue)
+  )
+}
+
+/** Holds if `factor` is a power of 2 that divides `mask`. */
+bindingset[mask]
+private predicate andmaskFactor(int mask, int factor) {
+  mask % factor = 0 and
+  factor = 2.pow([1 .. 30])
+}
+
+/** Holds if `e` is evenly divisible by `factor`. */
+private predicate evenlyDivisibleExpr(Expr e, int factor) {
+  exists(ConstantIntegerExpr c, int k | k = c.getIntValue() |
+    e.(MulExpr).getAnOperand() = c and factor = k.abs() and factor >= 2
+    or
+    e.(LShiftExpr).getRhs() = c and factor = 2.pow(k) and k > 0
+    or
+    e.(BitwiseAndExpr).getAnOperand() = c and factor = max(int f | andmaskFactor(k, f))
+  )
+}
+
+/**
+ * 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`.
+ */
+private predicate maxPhiInputRank(SsaPhiNode phi, int rix) {
+  rix = max(int r | rankedPhiInput(phi, _, _, r))
+}
+
+/**
+ * Gets the remainder of `val` modulo `mod`.
+ *
+ * For `mod = 0` the result equals `val` and for `mod > 1` the result is within
+ * the range `[0 .. mod-1]`.
+ */
+bindingset[val, mod]
+private int remainder(int val, int mod) {
+  mod = 0 and result = val
+  or
+  mod > 1 and result = ((val % mod) + mod) % mod
+}
+
+/**
+ * Holds if `inp` is an input to `phi` and equals `phi` modulo `mod` along `edge`.
+ */
+private predicate phiSelfModulus(
+  SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int mod
+) {
+  exists(SsaBound phibound, int v, int m |
+    edge.phiInput(phi, inp) and
+    phibound.getSsa() = phi and
+    ssaModulus(inp, edge, phibound, v, m) and
+    mod = m.gcd(v) and
+    mod != 1
+  )
+}
+
+/**
+ * Holds if `b + val` modulo `mod` is a candidate congruence class for `phi`.
+ */
+private predicate phiModulusInit(SsaPhiNode phi, Bound b, int val, int mod) {
+  exists(SsaVariable inp, SsaReadPositionPhiInputEdge edge |
+    edge.phiInput(phi, inp) and
+    ssaModulus(inp, edge, b, val, mod)
+  )
+}
+
+/**
+ * Holds if all inputs to `phi` numbered `1` to `rix` are equal to `b + val` modulo `mod`.
+ */
+private predicate phiModulusRankStep(SsaPhiNode phi, Bound b, int val, int mod, int rix) {
+  rix = 0 and
+  phiModulusInit(phi, b, val, mod)
+  or
+  exists(SsaVariable inp, SsaReadPositionPhiInputEdge edge, int v1, int m1 |
+    mod != 1 and
+    val = remainder(v1, mod)
+  |
+    exists(int v2, int m2 |
+      rankedPhiInput(phi, inp, edge, rix) and
+      phiModulusRankStep(phi, b, v1, m1, rix - 1) and
+      ssaModulus(inp, edge, b, v2, m2) and
+      mod = m1.gcd(m2).gcd(v1 - v2)
+    )
+    or
+    exists(int m2 |
+      rankedPhiInput(phi, inp, edge, rix) and
+      phiModulusRankStep(phi, b, v1, m1, rix - 1) and
+      phiSelfModulus(phi, inp, edge, m2) and
+      mod = m1.gcd(m2)
+    )
+  )
+}
+
+/**
+ * Holds if `phi` is equal to `b + val` modulo `mod`.
+ */
+private predicate phiModulus(SsaPhiNode phi, Bound b, int val, int mod) {
+  exists(int r |
+    maxPhiInputRank(phi, r) and
+    phiModulusRankStep(phi, b, val, mod, r)
+  )
+}
+
+/**
+ * Holds if `v` at `pos` is equal to `b + val` modulo `mod`.
+ */
+private predicate ssaModulus(SsaVariable v, SsaReadPosition pos, Bound b, int val, int mod) {
+  phiModulus(v, b, val, mod) and pos.hasReadOfVar(v)
+  or
+  b.(SsaBound).getSsa() = v and pos.hasReadOfVar(v) and val = 0 and mod = 0
+  or
+  exists(Expr e, int val0, int delta |
+    exprModulus(e, b, val0, mod) and
+    valueFlowStepSsa(v, pos, e, delta) and
+    val = remainder(val0 + delta, mod)
+  )
+  or
+  moduloGuardedRead(v, pos, val, mod) and b instanceof ZeroBound
+}
+
+/**
+ * Holds if `e` is equal to `b + val` modulo `mod`.
+ *
+ * There are two cases for the modulus:
+ * - `mod = 0`: The equality `e = b + val` is an ordinary equality.
+ * - `mod > 1`: `val` lies within the range `[0 .. mod-1]`.
+ */
+cached
+predicate exprModulus(Expr e, Bound b, int val, int mod) {
+  e = b.getExpr(val) and mod = 0
+  or
+  evenlyDivisibleExpr(e, mod) and val = 0 and b instanceof ZeroBound
+  or
+  exists(SsaVariable v, SsaReadPositionBlock bb |
+    ssaModulus(v, bb, b, val, mod) and
+    e = v.getAUse() and
+    getABasicBlockExpr(bb.getBlock()) = e
+  )
+  or
+  exists(Expr mid, int val0, int delta |
+    exprModulus(mid, b, val0, mod) and
+    valueFlowStep(e, mid, delta) and
+    val = remainder(val0 + delta, mod)
+  )
+  or
+  exists(ConditionalExpr cond, int v1, int v2, int m1, int m2 |
+    cond = e and
+    condExprBranchModulus(cond, true, b, v1, m1) and
+    condExprBranchModulus(cond, false, b, v2, m2) and
+    mod = m1.gcd(m2).gcd(v1 - v2) and
+    mod != 1 and
+    val = remainder(v1, mod)
+  )
+  or
+  exists(Bound b1, Bound b2, int v1, int v2, int m1, int m2 |
+    addModulus(e, true, b1, v1, m1) and
+    addModulus(e, false, b2, v2, m2) and
+    mod = m1.gcd(m2) and
+    mod != 1 and
+    val = remainder(v1 + v2, mod)
+  |
+    b = b1 and b2 instanceof ZeroBound
+    or
+    b = b2 and b1 instanceof ZeroBound
+  )
+  or
+  exists(int v1, int v2, int m1, int m2 |
+    subModulus(e, true, b, v1, m1) and
+    subModulus(e, false, any(ZeroBound zb), v2, m2) and
+    mod = m1.gcd(m2) and
+    mod != 1 and
+    val = remainder(v1 - v2, mod)
+  )
+}
+
+private predicate condExprBranchModulus(
+  ConditionalExpr cond, boolean branch, Bound b, int val, int mod
+) {
+  exprModulus(cond.getTrueExpr(), b, val, mod) and branch = true
+  or
+  exprModulus(cond.getFalseExpr(), b, val, mod) and branch = false
+}
+
+private predicate addModulus(Expr add, boolean isLeft, Bound b, int val, int mod) {
+  exists(Expr larg, Expr rarg | nonConstAddition(add, larg, rarg) |
+    exprModulus(larg, b, val, mod) and isLeft = true
+    or
+    exprModulus(rarg, b, val, mod) and isLeft = false
+  )
+}
+
+private predicate subModulus(Expr sub, boolean isLeft, Bound b, int val, int mod) {
+  exists(Expr larg, Expr rarg | nonConstSubtraction(sub, larg, rarg) |
+    exprModulus(larg, b, val, mod) and isLeft = true
+    or
+    exprModulus(rarg, b, val, mod) and isLeft = false
+  )
+}
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
new file mode 100644
index 00000000000..edf437e919c
--- /dev/null
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/BoundSpecific.qll
@@ -0,0 +1,21 @@
+/**
+ * Provides C#-specific definitions for bounds.
+ */
+
+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
+
+class SsaVariable extends Ssa::Definition {
+  /** Gets a read of the source variable underlying this SSA definition. */
+  Expr getAUse() { result = getARead() }
+}
+
+class Expr = CS::Expr;
+
+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)) }
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 e283909155c..08b64321a38 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
@@ -17,6 +17,13 @@ predicate propertyOverrides(Property p, string baseClass, string property) {
   )
 }
 
+/**
+ * Holds if `pa` is an access to the `Length` property of an array.
+ */
+predicate systemArrayLengthAccess(PropertyAccess pa) {
+  propertyOverrides(pa.getTarget(), "System.Array", "Length")
+}
+
 /**
  * Holds if expression `e` is either
  * - a compile time constant with integer value `val`, or
@@ -47,7 +54,7 @@ private int getArrayLengthRec(ArrayCreation arrCreation, int index) {
 }
 
 private predicate isArrayLengthAccess(PropertyAccess pa, int length) {
-  propertyOverrides(pa.getTarget(), "System.Array", "Length") and
+  systemArrayLengthAccess(pa) and
   exists(ExplicitDefinition arr, ArrayCreation arrCreation |
     getArrayLengthRec(arrCreation, arrCreation.getNumberOfLengthArguments() - 1) = length and
     arrCreation = arr.getADefinition().getSource() and
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
new file mode 100644
index 00000000000..2cdbfbf65f4
--- /dev/null
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
@@ -0,0 +1,110 @@
+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
+
+  class BasicBlock = CS::Ssa::BasicBlock;
+
+  class SsaVariable extends CS::Ssa::Definition {
+    CS::AssignableRead getAUse() { result = this.getARead() }
+  }
+
+  class SsaPhiNode = CS::Ssa::PhiNode;
+
+  class Expr = CS::Expr;
+
+  class Guard = G::Guard;
+
+  class ConstantIntegerExpr = CU::ConstantIntegerExpr;
+
+  class ConditionalExpr extends CS::ConditionalExpr {
+    /** Gets the "then" expression of this conditional expression. */
+    Expr getTrueExpr() { result = this.getThen() }
+
+    /** Gets the "else" expression of this conditional expression. */
+    Expr getFalseExpr() { result = this.getElse() }
+  }
+
+  /** Represent an addition expression. */
+  class AddExpr extends CS::AddExpr {
+    /** Gets the LHS operand of this add expression. */
+    Expr getLhs() { result = this.getLeftOperand() }
+
+    /** Gets the RHS operand of this add expression. */
+    Expr getRhs() { result = this.getRightOperand() }
+  }
+
+  /** Represent a subtraction expression. */
+  class SubExpr extends CS::SubExpr {
+    /** Gets the LHS operand of this subtraction expression. */
+    Expr getLhs() { result = this.getLeftOperand() }
+
+    /** Gets the RHS operand of this subtraction expression. */
+    Expr getRhs() { result = this.getRightOperand() }
+  }
+
+  class RemExpr = CS::RemExpr;
+
+  /** Represent a bitwise and or an assign-and expression. */
+  class BitwiseAndExpr extends CS::Expr {
+    BitwiseAndExpr() { this instanceof CS::BitwiseAndExpr or this instanceof CS::AssignAndExpr }
+
+    /** 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 valueFlowStep = RU::valueFlowStep/3;
+
+  predicate eqFlowCond = RU::eqFlowCond/5;
+
+  predicate ssaUpdateStep = RU::ssaUpdateStep/3;
+
+  Expr getABasicBlockExpr(BasicBlock bb) { result = bb.getANode().getElement() }
+
+  private predicate id(CS::ControlFlowElement x, CS::ControlFlowElement y) { x = y }
+
+  private predicate idOf(CS::ControlFlowElement x, int y) = equivalenceRelation(id/2)(x, y)
+
+  int getId(BasicBlock bb) { idOf(bb.getFirstNode().getElement(), result) }
+}
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
new file mode 100644
index 00000000000..4abfb2d1779
--- /dev/null
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/RangeUtils.qll
@@ -0,0 +1,98 @@
+/**
+ * Provides predicates for range and modulus analysis.
+ */
+
+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;
+
+/**
+ * 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 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)
+  )
+}
+
+/**
+ * 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 `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
+    )
+  |
+    x.getIntValue() = -delta
+  )
+}
+
+/**
+ * Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
+ */
+predicate guardControlsSsaRead(G::Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
+  exists(BooleanValue b | b.getValue() = testIsTrue |
+    guard.controlsBasicBlock(controlled.(SsaReadPositionBlock).getBlock(), b)
+  )
+}
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 813834c3fd8..9893ebc5dad 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
@@ -2,9 +2,10 @@
  * Provides C#-specific definitions for use in sign analysis.
  */
 module Private {
-  private import SsaUtils as SU
   private import csharp as CS
+  private import SsaUtils as SU
   private import ConstantUtils as CU
+  private import RangeUtils as RU
   private import semmle.code.csharp.controlflow.Guards as G
   import Impl
 
@@ -33,6 +34,8 @@ module Private {
   class Expr = CS::Expr;
 
   predicate ssaRead = SU::ssaRead/2;
+
+  predicate guardControlsSsaRead = RU::guardControlsSsaRead/3;
 }
 
 private module Impl {
@@ -254,15 +257,6 @@ private module Impl {
 
   Guard getComparisonGuard(ComparisonExpr ce) { result = ce.getExpr() }
 
-  /**
-   * 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)
-    )
-  }
-
   /** A relational comparison */
   class ComparisonExpr extends ComparisonTest {
     private boolean strict;
diff --git a/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.cs b/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.cs
new file mode 100644
index 00000000000..8c55e74372b
--- /dev/null
+++ b/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.cs
@@ -0,0 +1,84 @@
+using System;
+using System.Linq;
+
+class ModulusAnalysis
+{
+    const int c1 = 42;
+    const int c2 = 43;
+
+    void M(int i, bool cond, int x, int y, int[] arr, int otherSeven)
+    {
+        var eq = i + 3;
+
+        var mul = eq * c1 + 3; // congruent 3 mod 42
+
+        int seven = 7;
+        if (mul % c2 == seven)
+        {
+            System.Console.WriteLine(mul); // congruent 7 mod 43, 3 mod 42
+        }
+
+        if (otherSeven == 7)
+        {
+            if (mul % c2 == otherSeven)
+            {
+                System.Console.WriteLine(mul); // congruent 3 mod 42, 7 mod 43 missing
+            }
+        }
+
+        var j = cond
+            ? i * 4 + 3
+            : i * 8 + 7;
+        System.Console.WriteLine(j); // congruent 3 mod 4
+
+        if (x % c1 == 3 && y % c1 == 7)
+        {
+            System.Console.WriteLine(x + y); // congruent 10 mod 42
+        }
+
+        if (x % c1 == 3 && y % c1 == 7)
+        {
+            System.Console.WriteLine(x - y); // congruent 38 mod 42
+        }
+
+        var l = arr.Length * 4 - 11; // congruent 1 mod 4
+        System.Console.WriteLine(l);
+
+        l = GetArray().Length * 4 - 11;
+        System.Console.WriteLine(l); // congruent 1 mod 4
+
+        if (cond)
+        {
+            j = i * 4 + 3;
+        }
+        else
+        {
+            j = i * 8 + 7;
+        }
+        System.Console.WriteLine(j); // congruent 3 mod 4 or 7 mod 8
+
+        if (cond)
+        {
+            System.Console.WriteLine(j); // congruent 3 mod 4
+        }
+        else
+        {
+            System.Console.WriteLine(j); // congruent 7 mod 8
+        }
+
+        var t = 64;
+        System.Console.WriteLine(t & 32); // congruent 0 mod 32
+        System.Console.WriteLine(t & 16); // congruent 0 mod 16
+        t = 1;
+        System.Console.WriteLine(t << 2); // congruent 0 mod 4
+
+        if ((x & 15) == 3)
+        {
+            System.Console.WriteLine(x); // congruent 3 mod 16
+        }
+    }
+
+
+
+    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
new file mode 100644
index 00000000000..c7bacd76943
--- /dev/null
+++ b/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.expected
@@ -0,0 +1,138 @@
+| ModulusAnalysis.cs:6:15:6:21 | ... = ... | 0 | 42 | 0 |
+| ModulusAnalysis.cs:6:20:6:21 | 42 | 0 | 42 | 0 |
+| ModulusAnalysis.cs:7:15:7:21 | ... = ... | 0 | 43 | 0 |
+| ModulusAnalysis.cs:7:20:7:21 | 43 | 0 | 43 | 0 |
+| ModulusAnalysis.cs:11:18:11:18 | access to parameter i | SSA param(i) | 0 | 0 |
+| ModulusAnalysis.cs:11:18:11:22 | ... + ... | SSA param(i) | 3 | 0 |
+| ModulusAnalysis.cs:11:22:11:22 | 3 | 0 | 3 | 0 |
+| ModulusAnalysis.cs:13:19:13:20 | access to local variable eq | SSA def(eq) | 0 | 0 |
+| ModulusAnalysis.cs:13:19:13:20 | access to local variable eq | SSA param(i) | 3 | 0 |
+| ModulusAnalysis.cs:13:19:13:25 | ... * ... | 0 | 0 | 42 |
+| ModulusAnalysis.cs:13:19:13:29 | ... + ... | 0 | 3 | 42 |
+| ModulusAnalysis.cs:13:24:13:25 | access to constant c1 | 0 | 42 | 0 |
+| ModulusAnalysis.cs:13:24:13:25 | access to constant c1 | SSA entry def(ModulusAnalysis.c1) | 0 | 0 |
+| ModulusAnalysis.cs:13:29:13:29 | 3 | 0 | 3 | 0 |
+| ModulusAnalysis.cs:15:21:15:21 | 7 | 0 | 7 | 0 |
+| ModulusAnalysis.cs:16:13:16:15 | access to local variable mul | 0 | 3 | 42 |
+| ModulusAnalysis.cs:16:13:16:15 | access to local variable mul | SSA def(mul) | 0 | 0 |
+| ModulusAnalysis.cs:16:19:16:20 | access to constant c2 | 0 | 43 | 0 |
+| ModulusAnalysis.cs:16:19:16:20 | access to constant c2 | SSA entry def(ModulusAnalysis.c2) | 0 | 0 |
+| ModulusAnalysis.cs:16:25:16:29 | access to local variable seven | 0 | 7 | 0 |
+| ModulusAnalysis.cs:16:25:16:29 | access to local variable seven | SSA def(seven) | 0 | 0 |
+| ModulusAnalysis.cs:18:38:18:40 | access to local variable mul | 0 | 3 | 42 |
+| ModulusAnalysis.cs:18:38:18:40 | access to local variable mul | 0 | 7 | 43 |
+| ModulusAnalysis.cs:18:38:18:40 | access to local variable mul | SSA def(mul) | 0 | 0 |
+| ModulusAnalysis.cs:21:13:21:22 | access to parameter otherSeven | SSA param(otherSeven) | 0 | 0 |
+| ModulusAnalysis.cs:21:27:21:27 | 7 | 0 | 7 | 0 |
+| ModulusAnalysis.cs:23:17:23:19 | access to local variable mul | 0 | 3 | 42 |
+| ModulusAnalysis.cs:23:17:23:19 | access to local variable mul | SSA def(mul) | 0 | 0 |
+| ModulusAnalysis.cs:23:23:23:24 | access to constant c2 | 0 | 43 | 0 |
+| ModulusAnalysis.cs:23:23:23:24 | access to constant c2 | SSA entry def(ModulusAnalysis.c2) | 0 | 0 |
+| ModulusAnalysis.cs:23:29:23:38 | access to parameter otherSeven | 0 | 7 | 0 |
+| ModulusAnalysis.cs:23:29:23:38 | access to parameter otherSeven | SSA param(otherSeven) | 0 | 0 |
+| 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: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 |
+| ModulusAnalysis.cs:66:38:66:38 | access to local variable j | [cond (line 9): false] SSA def(j) | 0 | 0 |
+| ModulusAnalysis.cs:69:17:69:18 | 64 | 0 | 64 | 0 |
+| ModulusAnalysis.cs:70:34:70:34 | access to local variable t | 0 | 64 | 0 |
+| ModulusAnalysis.cs:70:34:70:34 | access to local variable t | SSA def(t) | 0 | 0 |
+| ModulusAnalysis.cs:70:34:70:39 | ... & ... | 0 | 0 | 32 |
+| ModulusAnalysis.cs:70:34:70:39 | ... & ... | 0 | 0 | 64 |
+| ModulusAnalysis.cs:70:38:70:39 | 32 | 0 | 32 | 0 |
+| ModulusAnalysis.cs:71:34:71:34 | access to local variable t | 0 | 64 | 0 |
+| ModulusAnalysis.cs:71:34:71:34 | access to local variable t | SSA def(t) | 0 | 0 |
+| ModulusAnalysis.cs:71:34:71:39 | ... & ... | 0 | 0 | 16 |
+| ModulusAnalysis.cs:71:34:71:39 | ... & ... | 0 | 0 | 64 |
+| ModulusAnalysis.cs:71:38:71:39 | 16 | 0 | 16 | 0 |
+| ModulusAnalysis.cs:72:9:72:13 | ... = ... | 0 | 1 | 0 |
+| ModulusAnalysis.cs:72:13:72:13 | 1 | 0 | 1 | 0 |
+| ModulusAnalysis.cs:73:34:73:34 | access to local variable t | 0 | 1 | 0 |
+| ModulusAnalysis.cs:73:34:73:34 | access to local variable t | SSA def(t) | 0 | 0 |
+| ModulusAnalysis.cs:73:34:73:39 | ... << ... | 0 | 0 | 4 |
+| ModulusAnalysis.cs:73:39:73:39 | 2 | 0 | 2 | 0 |
+| ModulusAnalysis.cs:75:14:75:14 | access to parameter x | SSA param(x) | 0 | 0 |
+| ModulusAnalysis.cs:75:18:75:19 | 15 | 0 | 15 | 0 |
+| 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 |
diff --git a/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.ql b/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.ql
new file mode 100644
index 00000000000..f92649fa5b2
--- /dev/null
+++ b/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.ql
@@ -0,0 +1,7 @@
+import csharp
+import semmle.code.csharp.dataflow.ModulusAnalysis
+import semmle.code.csharp.dataflow.Bound
+
+from Expr e, Bound b, int delta, int mod
+where exprModulus(e, b, delta, mod)
+select e, b.toString(), delta, mod
diff --git a/java/ql/src/semmle/code/java/dataflow/Bound.qll b/java/ql/src/semmle/code/java/dataflow/Bound.qll
index 4a89f8cfeba..b129203db70 100644
--- a/java/ql/src/semmle/code/java/dataflow/Bound.qll
+++ b/java/ql/src/semmle/code/java/dataflow/Bound.qll
@@ -2,15 +2,13 @@
  * Provides classes for representing abstract bounds for use in, for example, range analysis.
  */
 
-import java
-private import SSA
-private import RangeUtils
+private import internal.rangeanalysis.BoundSpecific
 
 private newtype TBound =
   TBoundZero() or
   TBoundSsa(SsaVariable v) { v.getSourceVariable().getType() instanceof IntegralType } or
   TBoundExpr(Expr e) {
-    e.(FieldRead).getField() instanceof ArrayLengthField and
+    interestingExprBound(e) and
     not exists(SsaVariable v | e = v.getAUse())
   }
 
@@ -75,6 +73,6 @@ class ExprBound extends Bound, TBoundExpr {
   override Expr getExpr(int delta) { this = TBoundExpr(result) and delta = 0 }
 
   override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
-    getExpr().hasLocationInfo(path, sl, sc, el, ec)
+    getExpr().getLocation().hasLocationInfo(path, sl, sc, el, ec)
   }
 }
diff --git a/java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll b/java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll
index b153e9fbd04..2b3c3402415 100644
--- a/java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll
+++ b/java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll
@@ -4,12 +4,9 @@
  * variable), and `v` is an integer in the range `[0 .. m-1]`.
  */
 
-import java
-private import SSA
-private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon
-private import RangeUtils
-private import semmle.code.java.controlflow.Guards
-import Bound
+private import internal.rangeanalysis.ModulusAnalysisSpecific::Private
+private import Bound
+private import internal.rangeanalysis.SsaReadPositionCommon
 
 /**
  * Holds if `e + delta` equals `v` at `pos`.
@@ -29,16 +26,9 @@ private predicate valueFlowStepSsa(SsaVariable v, SsaReadPosition pos, Expr e, i
  * `ConstantIntegerExpr`s.
  */
 private predicate nonConstAddition(Expr add, Expr larg, Expr rarg) {
-  (
-    exists(AddExpr a | a = add |
-      larg = a.getLeftOperand() and
-      rarg = a.getRightOperand()
-    )
-    or
-    exists(AssignAddExpr a | a = add |
-      larg = a.getDest() and
-      rarg = a.getRhs()
-    )
+  exists(AddExpr a | a = add |
+    larg = a.getLhs() and
+    rarg = a.getRhs()
   ) and
   not larg instanceof ConstantIntegerExpr and
   not rarg instanceof ConstantIntegerExpr
@@ -49,16 +39,9 @@ private predicate nonConstAddition(Expr add, Expr larg, Expr rarg) {
  * a `ConstantIntegerExpr`.
  */
 private predicate nonConstSubtraction(Expr sub, Expr larg, Expr rarg) {
-  (
-    exists(SubExpr s | s = sub |
-      larg = s.getLeftOperand() and
-      rarg = s.getRightOperand()
-    )
-    or
-    exists(AssignSubExpr s | s = sub |
-      larg = s.getDest() and
-      rarg = s.getRhs()
-    )
+  exists(SubExpr s | s = sub |
+    larg = s.getLhs() and
+    rarg = s.getRhs()
   ) and
   not rarg instanceof ConstantIntegerExpr
 }
@@ -68,14 +51,14 @@ private Expr modExpr(Expr arg, int mod) {
   exists(RemExpr rem |
     result = rem and
     arg = rem.getLeftOperand() and
-    rem.getRightOperand().(CompileTimeConstantExpr).getIntValue() = mod and
+    rem.getRightOperand().(ConstantIntegerExpr).getIntValue() = mod and
     mod >= 2
   )
   or
-  exists(CompileTimeConstantExpr c |
+  exists(ConstantIntegerExpr c |
     mod = 2.pow([1 .. 30]) and
     c.getIntValue() = mod - 1 and
-    result.(AndBitwiseExpr).hasOperands(arg, c)
+    result.(BitwiseAndExpr).hasOperands(arg, c)
   )
 }
 
@@ -84,7 +67,7 @@ private Expr modExpr(Expr arg, int mod) {
  * its `testIsTrue` branch.
  */
 private Guard moduloCheck(SsaVariable v, int val, int mod, boolean testIsTrue) {
-  exists(Expr rem, CompileTimeConstantExpr c, int r, boolean polarity |
+  exists(Expr rem, ConstantIntegerExpr c, int r, boolean polarity |
     result.isEquality(rem, c, polarity) and
     c.getIntValue() = r and
     rem = modExpr(v.getAUse(), mod) and
@@ -122,24 +105,12 @@ private predicate evenlyDivisibleExpr(Expr e, int factor) {
   exists(ConstantIntegerExpr c, int k | k = c.getIntValue() |
     e.(MulExpr).getAnOperand() = c and factor = k.abs() and factor >= 2
     or
-    e.(AssignMulExpr).getSource() = c and factor = k.abs() and factor >= 2
+    e.(LShiftExpr).getRhs() = c and factor = 2.pow(k) and k > 0
     or
-    e.(LShiftExpr).getRightOperand() = c and factor = 2.pow(k) and k > 0
-    or
-    e.(AssignLShiftExpr).getRhs() = c and factor = 2.pow(k) and k > 0
-    or
-    e.(AndBitwiseExpr).getAnOperand() = c and factor = max(int f | andmaskFactor(k, f))
-    or
-    e.(AssignAndExpr).getSource() = c and factor = max(int f | andmaskFactor(k, f))
+    e.(BitwiseAndExpr).getAnOperand() = c and factor = max(int f | andmaskFactor(k, f))
   )
 }
 
-private predicate id(BasicBlock x, BasicBlock y) { x = y }
-
-private predicate idOf(BasicBlock x, int y) = equivalenceRelation(id/2)(x, y)
-
-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`.
@@ -267,7 +238,7 @@ predicate exprModulus(Expr e, Bound b, int val, int mod) {
   exists(SsaVariable v, SsaReadPositionBlock bb |
     ssaModulus(v, bb, b, val, mod) and
     e = v.getAUse() and
-    bb.getBlock() = e.getBasicBlock()
+    getABasicBlockExpr(bb.getBlock()) = e
   )
   or
   exists(Expr mid, int val0, int delta |
diff --git a/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/BoundSpecific.qll b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/BoundSpecific.qll
new file mode 100644
index 00000000000..f7fca3a184f
--- /dev/null
+++ b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/BoundSpecific.qll
@@ -0,0 +1,20 @@
+/**
+ * Provides Java-specific definitions for bounds.
+ */
+
+private import java as J
+private import semmle.code.java.dataflow.SSA as Ssa
+private import semmle.code.java.dataflow.RangeUtils as RU
+
+class SsaVariable = Ssa::SsaVariable;
+
+class Expr = J::Expr;
+
+class IntegralType = J::IntegralType;
+
+class ConstantIntegerExpr = RU::ConstantIntegerExpr;
+
+/** Holds if `e` is a bound expression and it is not an SSA variable read. */
+predicate interestingExprBound(Expr e) {
+  e.(J::FieldRead).getField() instanceof J::ArrayLengthField
+}
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
new file mode 100644
index 00000000000..374cb102e0a
--- /dev/null
+++ b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
@@ -0,0 +1,119 @@
+module Private {
+  private import java as J
+  private import semmle.code.java.dataflow.SSA as Ssa
+  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
+
+  class BasicBlock = BB::BasicBlock;
+
+  class SsaVariable = Ssa::SsaVariable;
+
+  class SsaPhiNode = Ssa::SsaPhiNode;
+
+  class Expr = J::Expr;
+
+  class Guard = G::Guard;
+
+  class ConstantIntegerExpr = RU::ConstantIntegerExpr;
+
+  class ConditionalExpr = J::ConditionalExpr;
+
+  /** An addition or an assign-add expression. */
+  class AddExpr extends J::Expr {
+    AddExpr() { this instanceof J::AddExpr or this instanceof J::AssignAddExpr }
+
+    /** Gets the LHS operand of this add expression. */
+    Expr getLhs() {
+      result = this.(J::AddExpr).getLeftOperand()
+      or
+      result = this.(J::AssignAddExpr).getDest()
+    }
+
+    /** Gets the RHS operand of this add expression. */
+    Expr getRhs() {
+      result = this.(J::AddExpr).getRightOperand()
+      or
+      result = this.(J::AssignAddExpr).getRhs()
+    }
+  }
+
+  /** A subtraction or an assign-sub expression. */
+  class SubExpr extends J::Expr {
+    SubExpr() { this instanceof J::SubExpr or this instanceof J::AssignSubExpr }
+
+    /** Gets the LHS operand of this subtraction expression. */
+    Expr getLhs() {
+      result = this.(J::SubExpr).getLeftOperand()
+      or
+      result = this.(J::AssignSubExpr).getDest()
+    }
+
+    /** Gets the RHS operand of this subtraction expression. */
+    Expr getRhs() {
+      result = this.(J::SubExpr).getRightOperand()
+      or
+      result = this.(J::AssignSubExpr).getRhs()
+    }
+  }
+
+  class RemExpr = J::RemExpr;
+
+  /** A multiplication or an assign-mul expression. */
+  class MulExpr extends J::Expr {
+    MulExpr() { this instanceof J::MulExpr or this instanceof J::AssignMulExpr }
+
+    /** Gets an operand of this multiplication. */
+    Expr getAnOperand() {
+      result = this.(J::MulExpr).getAnOperand() or
+      result = this.(J::AssignMulExpr).getSource()
+    }
+  }
+
+  /** A left shift or an assign-lshift expression. */
+  class LShiftExpr extends J::Expr {
+    LShiftExpr() { this instanceof J::LShiftExpr or this instanceof J::AssignLShiftExpr }
+
+    /** Gets the RHS operand of this shift. */
+    Expr getRhs() {
+      result = this.(J::LShiftExpr).getRightOperand() or
+      result = this.(J::AssignLShiftExpr).getRhs()
+    }
+  }
+
+  /** A bitwise and or an assign-and expression. */
+  class BitwiseAndExpr extends J::Expr {
+    BitwiseAndExpr() { this instanceof J::AndBitwiseExpr or this instanceof J::AssignAndExpr }
+
+    /** Gets an operand of this bitwise and operation. */
+    Expr getAnOperand() {
+      result = this.(J::AndBitwiseExpr).getAnOperand() or
+      result = this.(J::AssignAndExpr).getSource()
+    }
+
+    /** 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
+    }
+  }
+
+  predicate guardDirectlyControlsSsaRead = RU::guardDirectlyControlsSsaRead/3;
+
+  predicate guardControlsSsaRead = RU::guardControlsSsaRead/3;
+
+  predicate valueFlowStep = RU::valueFlowStep/3;
+
+  predicate eqFlowCond = RU::eqFlowCond/5;
+
+  predicate ssaUpdateStep = RU::ssaUpdateStep/3;
+
+  Expr getABasicBlockExpr(BasicBlock bb) { result = bb.getANode() }
+
+  private predicate id(BasicBlock x, BasicBlock y) { x = y }
+
+  private predicate idOf(BasicBlock x, int y) = equivalenceRelation(id/2)(x, y)
+
+  int getId(BasicBlock bb) { idOf(bb, result) }
+}
diff --git a/java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.expected b/java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.expected
new file mode 100644
index 00000000000..597b4795fcb
--- /dev/null
+++ b/java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.expected
@@ -0,0 +1,107 @@
+| ModulusAnalysis.java:3:5:3:22 | ...=... | 0 | 42 | 0 |
+| ModulusAnalysis.java:3:5:3:22 | c1 | 0 | 42 | 0 |
+| ModulusAnalysis.java:3:20:3:21 | 42 | 0 | 42 | 0 |
+| ModulusAnalysis.java:4:5:4:22 | ...=... | 0 | 43 | 0 |
+| ModulusAnalysis.java:4:5:4:22 | c2 | 0 | 43 | 0 |
+| ModulusAnalysis.java:4:20:4:21 | 43 | 0 | 43 | 0 |
+| ModulusAnalysis.java:7:18:7:18 | i | SSA init(i) | 0 | 0 |
+| ModulusAnalysis.java:7:18:7:22 | ... + ... | SSA init(i) | 3 | 0 |
+| ModulusAnalysis.java:7:22:7:22 | 3 | 0 | 3 | 0 |
+| ModulusAnalysis.java:9:19:9:20 | eq | SSA def(eq) | 0 | 0 |
+| ModulusAnalysis.java:9:19:9:20 | eq | SSA init(i) | 3 | 0 |
+| ModulusAnalysis.java:9:19:9:25 | ... * ... | 0 | 0 | 42 |
+| ModulusAnalysis.java:9:19:9:29 | ... + ... | 0 | 3 | 42 |
+| ModulusAnalysis.java:9:24:9:25 | c1 | 0 | 42 | 0 |
+| ModulusAnalysis.java:9:24:9:25 | c1 | SSA init(this.c1) | 0 | 0 |
+| ModulusAnalysis.java:9:29:9:29 | 3 | 0 | 3 | 0 |
+| ModulusAnalysis.java:11:21:11:21 | 7 | 0 | 7 | 0 |
+| ModulusAnalysis.java:12:13:12:15 | mul | 0 | 3 | 42 |
+| ModulusAnalysis.java:12:13:12:15 | mul | SSA def(mul) | 0 | 0 |
+| ModulusAnalysis.java:12:19:12:20 | c2 | 0 | 43 | 0 |
+| ModulusAnalysis.java:12:19:12:20 | c2 | SSA impl upd[untracked](this.c2) | 0 | 0 |
+| ModulusAnalysis.java:12:25:12:29 | seven | 0 | 7 | 0 |
+| ModulusAnalysis.java:12:25:12:29 | seven | SSA def(seven) | 0 | 0 |
+| ModulusAnalysis.java:13:32:13:34 | mul | 0 | 3 | 42 |
+| ModulusAnalysis.java:13:32:13:34 | mul | 0 | 7 | 43 |
+| ModulusAnalysis.java:13:32:13:34 | mul | SSA def(mul) | 0 | 0 |
+| ModulusAnalysis.java:16:17:18:23 | ...?...:... | 0 | 3 | 4 |
+| ModulusAnalysis.java:17:15:17:15 | i | SSA init(i) | 0 | 0 |
+| ModulusAnalysis.java:17:15:17:19 | ... * ... | 0 | 0 | 4 |
+| ModulusAnalysis.java:17:15:17:23 | ... + ... | 0 | 3 | 4 |
+| ModulusAnalysis.java:17:19:17:19 | 4 | 0 | 4 | 0 |
+| ModulusAnalysis.java:17:23:17:23 | 3 | 0 | 3 | 0 |
+| ModulusAnalysis.java:18:15:18:15 | i | SSA init(i) | 0 | 0 |
+| ModulusAnalysis.java:18:15:18:19 | ... * ... | 0 | 0 | 8 |
+| ModulusAnalysis.java:18:15:18:23 | ... + ... | 0 | 7 | 8 |
+| ModulusAnalysis.java:18:19:18:19 | 8 | 0 | 8 | 0 |
+| ModulusAnalysis.java:18:23:18:23 | 7 | 0 | 7 | 0 |
+| ModulusAnalysis.java:19:28:19:28 | j | 0 | 3 | 4 |
+| ModulusAnalysis.java:19:28:19:28 | j | SSA def(j) | 0 | 0 |
+| ModulusAnalysis.java:21:13:21:13 | x | SSA init(x) | 0 | 0 |
+| ModulusAnalysis.java:21:17:21:18 | c1 | 0 | 42 | 0 |
+| ModulusAnalysis.java:21:17:21:18 | c1 | SSA init(this.c1) | 0 | 0 |
+| ModulusAnalysis.java:21:23:21:23 | 3 | 0 | 3 | 0 |
+| ModulusAnalysis.java:21:28:21:28 | y | SSA init(y) | 0 | 0 |
+| ModulusAnalysis.java:21:32:21:33 | c1 | 0 | 42 | 0 |
+| ModulusAnalysis.java:21:32:21:33 | c1 | SSA init(this.c1) | 0 | 0 |
+| ModulusAnalysis.java:21:38:21:38 | 7 | 0 | 7 | 0 |
+| ModulusAnalysis.java:22:32:22:32 | x | 0 | 3 | 42 |
+| ModulusAnalysis.java:22:32:22:32 | x | SSA init(x) | 0 | 0 |
+| ModulusAnalysis.java:22:32:22:36 | ... + ... | 0 | 10 | 42 |
+| ModulusAnalysis.java:22:32:22:36 | ... + ... | SSA init(x) | 7 | 42 |
+| ModulusAnalysis.java:22:32:22:36 | ... + ... | SSA init(y) | 3 | 42 |
+| ModulusAnalysis.java:22:36:22:36 | y | 0 | 7 | 42 |
+| ModulusAnalysis.java:22:36:22:36 | y | SSA init(y) | 0 | 0 |
+| ModulusAnalysis.java:25:13:25:13 | x | SSA init(x) | 0 | 0 |
+| ModulusAnalysis.java:25:17:25:18 | c1 | 0 | 42 | 0 |
+| ModulusAnalysis.java:25:17:25:18 | c1 | SSA init(this.c1) | 0 | 0 |
+| ModulusAnalysis.java:25:23:25:23 | 3 | 0 | 3 | 0 |
+| ModulusAnalysis.java:25:28:25:28 | y | SSA init(y) | 0 | 0 |
+| ModulusAnalysis.java:25:32:25:33 | c1 | 0 | 42 | 0 |
+| ModulusAnalysis.java:25:32:25:33 | c1 | SSA init(this.c1) | 0 | 0 |
+| ModulusAnalysis.java:25:38:25:38 | 7 | 0 | 7 | 0 |
+| ModulusAnalysis.java:26:32:26:32 | x | 0 | 3 | 42 |
+| ModulusAnalysis.java:26:32:26:32 | x | SSA init(x) | 0 | 0 |
+| ModulusAnalysis.java:26:32:26:36 | ... - ... | 0 | 38 | 42 |
+| ModulusAnalysis.java:26:32:26:36 | ... - ... | SSA init(x) | 35 | 42 |
+| ModulusAnalysis.java:26:36:26:36 | y | 0 | 7 | 42 |
+| ModulusAnalysis.java:26:36:26:36 | y | SSA init(y) | 0 | 0 |
+| ModulusAnalysis.java:29:17:29:26 | arr.length | SSA impl upd[untracked](arr.length) | 0 | 0 |
+| ModulusAnalysis.java:29:17:29:30 | ... * ... | 0 | 0 | 4 |
+| ModulusAnalysis.java:29:17:29:35 | ... - ... | 0 | 1 | 4 |
+| ModulusAnalysis.java:29:30:29:30 | 4 | 0 | 4 | 0 |
+| ModulusAnalysis.java:29:34:29:35 | 11 | 0 | 11 | 0 |
+| ModulusAnalysis.java:30:28:30:28 | l | 0 | 1 | 4 |
+| ModulusAnalysis.java:30:28:30:28 | l | SSA def(l) | 0 | 0 |
+| ModulusAnalysis.java:32:9:32:38 | ...=... | 0 | 1 | 4 |
+| ModulusAnalysis.java:32:13:32:29 | getArray(...).length | getArray(...).length | 0 | 0 |
+| ModulusAnalysis.java:32:13:32:33 | ... * ... | 0 | 0 | 4 |
+| ModulusAnalysis.java:32:13:32:38 | ... - ... | 0 | 1 | 4 |
+| ModulusAnalysis.java:32:33:32:33 | 4 | 0 | 4 | 0 |
+| ModulusAnalysis.java:32:37:32:38 | 11 | 0 | 11 | 0 |
+| ModulusAnalysis.java:33:28:33:28 | l | 0 | 1 | 4 |
+| ModulusAnalysis.java:33:28:33:28 | l | SSA def(l) | 0 | 0 |
+| ModulusAnalysis.java:36:13:36:25 | ...=... | 0 | 3 | 4 |
+| ModulusAnalysis.java:36:17:36:17 | i | SSA init(i) | 0 | 0 |
+| ModulusAnalysis.java:36:17:36:21 | ... * ... | 0 | 0 | 4 |
+| ModulusAnalysis.java:36:17:36:25 | ... + ... | 0 | 3 | 4 |
+| ModulusAnalysis.java:36:21:36:21 | 4 | 0 | 4 | 0 |
+| ModulusAnalysis.java:36:25:36:25 | 3 | 0 | 3 | 0 |
+| ModulusAnalysis.java:39:13:39:25 | ...=... | 0 | 7 | 8 |
+| ModulusAnalysis.java:39:17:39:17 | i | SSA init(i) | 0 | 0 |
+| ModulusAnalysis.java:39:17:39:21 | ... * ... | 0 | 0 | 8 |
+| ModulusAnalysis.java:39:17:39:25 | ... + ... | 0 | 7 | 8 |
+| ModulusAnalysis.java:39:21:39:21 | 8 | 0 | 8 | 0 |
+| ModulusAnalysis.java:39:25:39:25 | 7 | 0 | 7 | 0 |
+| ModulusAnalysis.java:41:28:41:28 | j | 0 | 3 | 4 |
+| ModulusAnalysis.java:41:28:41:28 | j | SSA phi(j) | 0 | 0 |
+| ModulusAnalysis.java:44:32:44:32 | j | 0 | 3 | 4 |
+| ModulusAnalysis.java:44:32:44:32 | j | SSA phi(j) | 0 | 0 |
+| ModulusAnalysis.java:46:32:46:32 | j | 0 | 3 | 4 |
+| ModulusAnalysis.java:46:32:46:32 | j | SSA phi(j) | 0 | 0 |
+| ModulusAnalysis.java:49:14:49:14 | x | SSA init(x) | 0 | 0 |
+| ModulusAnalysis.java:49:18:49:19 | 15 | 0 | 15 | 0 |
+| 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 |
diff --git a/java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.java b/java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.java
new file mode 100644
index 00000000000..5b251894166
--- /dev/null
+++ b/java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.java
@@ -0,0 +1,55 @@
+class ModulusAnalysis
+{
+    final int c1 = 42;
+    final int c2 = 43;
+
+    void m(int i, boolean cond, int x, int y, int[] arr) {
+        int eq = i + 3;
+
+        int mul = eq * c1 + 3; // congruent 3 mod 42
+
+        int seven = 7;
+        if (mul % c2 == seven) {
+            System.out.println(mul); // congruent 3 mod 42, 7 mod 43
+        }
+
+        int j = cond
+            ? i * 4 + 3
+            : i * 8 + 7;
+        System.out.println(j); // congruent 3 mod 4
+
+        if (x % c1 == 3 && y % c1 == 7) {
+            System.out.println(x + y); // congruent 10 mod 42
+        }
+
+        if (x % c1 == 3 && y % c1 == 7) {
+            System.out.println(x - y); // congruent 38 mod 42
+        }
+
+        int l = arr.length * 4 - 11;
+        System.out.println(l); // congruent 1 mod 4
+
+        l = getArray().length * 4 - 11;
+        System.out.println(l); // congruent 1 mod 4
+
+        if (cond) {
+            j = i * 4 + 3;
+        }
+        else {
+            j = i * 8 + 7;
+        }
+        System.out.println(j); // congruent 3 mod 4
+
+        if (cond) {
+            System.out.println(j); // congruent 3 mod 4
+        } else {
+            System.out.println(j); // congruent 3 mod 4
+        }
+
+        if ((x & 15) == 3) {
+            System.out.println(x); // congruent 3 mod 16
+        }
+    }
+
+    int[] getArray(){ return new int[42]; }
+}
\ No newline at end of file
diff --git a/java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.ql b/java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.ql
new file mode 100644
index 00000000000..b9a71b74412
--- /dev/null
+++ b/java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.ql
@@ -0,0 +1,7 @@
+import java
+import semmle.code.java.dataflow.ModulusAnalysis
+import semmle.code.java.dataflow.Bound
+
+from Expr e, Bound b, int delta, int mod
+where exprModulus(e, b, delta, mod)
+select e, b.toString(), delta, mod