diff --git a/csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll b/csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll
index aa7bf06f2a25..6e232bf79dab 100644
--- a/csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll
+++ b/csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll
@@ -2516,8 +2516,12 @@ module ControlFlow {
           result = strictcount(getAnElement())
         }
 
+        predicate immediatelyDominates(PreBasicBlock bb) {
+          bbIDominates(this, bb)
+        }
+
         predicate strictlyDominates(PreBasicBlock bb) {
-          bbIDominates+(this, bb)
+          this.immediatelyDominates+(bb)
         }
 
         predicate dominates(PreBasicBlock bb) {
@@ -2565,7 +2569,8 @@ module ControlFlow {
 
     /**
      * Provides an SSA implementation based on "pre-basic-blocks", restricted
-     * to local scope variables.
+     * to local scope variables and fields/properties that behave like local
+     * scope variables.
      *
      * The logic is duplicated from the implementation in `SSA.qll`, and
      * being an internal class, all predicate documentation has been removed.
@@ -2574,17 +2579,40 @@ module ControlFlow {
       private import PreBasicBlocks
       private import AssignableDefinitions
 
-      class SimpleLocalScopeVariable extends LocalScopeVariable {
-        SimpleLocalScopeVariable() {
-          not exists(AssignableDefinition def1, AssignableDefinition def2 |
-            def1.getTarget() = this and
-            def2.getTarget() = this and
-            def1.getEnclosingCallable() != def2.getEnclosingCallable()
+      /**
+       * A simple assignable. Either a local scope variable or a field/property
+       * that behaves like a local scope variable.
+       */
+      class SimpleAssignable extends Assignable {
+        private Callable c;
+
+        SimpleAssignable() {
+          (
+            this instanceof LocalScopeVariable
+            or
+            this instanceof Field
+            or
+            this = any(TrivialProperty tp | not tp.isOverridableOrImplementable())
+          ) and
+          forall(AssignableDefinition def |
+            def.getTarget() = this |
+            c = def.getEnclosingCallable()
+            or
+            def.getEnclosingCallable() instanceof Constructor
+          ) and
+          exists(AssignableAccess aa |
+            aa.getTarget() = this |
+            c = aa.getEnclosingCallable()
+          ) and
+          forall(QualifiableExpr qe |
+            qe.(AssignableAccess).getTarget() = this |
+            qe.targetIsThisInstance()
           )
         }
-      }
 
-      private newtype SsaRefKind = SsaRead() or SsaDef()
+        /** Gets a callable in which this simple assignable can be analyzed. */
+        Callable getACallable() { result = c }
+      }
 
       class Definition extends TPreSsaDef {
         string toString() {
@@ -2593,22 +2621,29 @@ module ControlFlow {
             result = def.toString()
           )
           or
-          exists(SimpleLocalScopeVariable v |
-            this = TPhiPreSsaDef(_, v) |
-            result = "phi(" + v.toString() + ")"
+          exists(SimpleAssignable a |
+            this = TImplicitEntryPreSsaDef(_, _, a) |
+            result = "implicit(" + a + ")"
+          )
+          or
+          exists(SimpleAssignable a |
+            this = TPhiPreSsaDef(_, a) |
+            result = "phi(" + a.toString() + ")"
           )
         }
 
-        SimpleLocalScopeVariable getVariable() {
+        SimpleAssignable getAssignable() {
           this = TExplicitPreSsaDef(_, _, _, result)
           or
+          this = TImplicitEntryPreSsaDef(_, _, result)
+          or
           this = TPhiPreSsaDef(_, result)
         }
 
-        LocalScopeVariableRead getARead() {
+        AssignableRead getARead() {
           firstReadSameVar(this, result)
           or
-          exists(LocalScopeVariableRead read |
+          exists(AssignableRead read |
             firstReadSameVar(this, read) |
             adjacentReadPairSameVar+(read, result)
           )
@@ -2620,141 +2655,270 @@ module ControlFlow {
             result = def.getLocation()
           )
           or
+          exists(Callable c |
+            this = TImplicitEntryPreSsaDef(c, _, _) |
+            result = c.getLocation()
+          )
+          or
           exists(PreBasicBlock bb |
             this = TPhiPreSsaDef(bb, _) |
             result = bb.getLocation()
           )
         }
 
+        PreBasicBlock getBasicBlock() {
+          this = TExplicitPreSsaDef(result, _, _, _)
+          or
+          this = TImplicitEntryPreSsaDef(_, result, _)
+          or
+          this = TPhiPreSsaDef(result, _)
+        }
+
+        Callable getCallable() {
+          result = this.getBasicBlock().getEnclosingCallable()
+        }
+
         AssignableDefinition getDefinition() {
           this = TExplicitPreSsaDef(_, _, result, _)
         }
+
+        Definition getAPhiInput() {
+          exists(PreBasicBlock bb, PreBasicBlock phiPred, SimpleAssignable a |
+            this = TPhiPreSsaDef(bb, a) |
+            bb.getAPredecessor() = phiPred and
+            ssaDefReachesEndOfBlock(phiPred, result, a)
+          )
+        }
+      }
+
+      predicate implicitEntryDef(Callable c, PreBasicBlock bb, SimpleAssignable a) {
+        not a instanceof LocalScopeVariable and
+        c = a.getACallable() and
+        bb = succEntry(c)
       }
 
-      predicate assignableDefAt(PreBasicBlocks::PreBasicBlock bb, int i, AssignableDefinition def, SimpleLocalScopeVariable v) {
+      private predicate assignableDefAt(PreBasicBlocks::PreBasicBlock bb, int i, AssignableDefinition def, SimpleAssignable a) {
         bb.getElement(i) = def.getExpr() and
-        v = def.getTarget() and
+        a = def.getTarget() and
         // In cases like `(x, x) = (0, 1)`, we discard the first (dead) definition of `x`
         not exists(TupleAssignmentDefinition first, TupleAssignmentDefinition second |
           first = def |
           second.getAssignment() = first.getAssignment() and
           second.getEvaluationOrder() > first.getEvaluationOrder() and
-          second.getTarget() = v
+          second.getTarget() = a
         )
         or
-        def.(ImplicitParameterDefinition).getParameter() = v and
+        def.(ImplicitParameterDefinition).getParameter() = a and
         exists(Callable c |
-          v = c.getAParameter() |
+          a = c.getAParameter() |
           bb = succEntry(c) and
           i = -1
         )
       }
 
-      predicate defAt(PreBasicBlock bb, int i, Definition def, SimpleLocalScopeVariable v) {
-        def = TExplicitPreSsaDef(bb, i, _, v)
+      private predicate readAt(PreBasicBlock bb, int i, AssignableRead read, SimpleAssignable a) {
+        read = bb.getElement(i) and
+        read.getTarget() = a
+      }
+
+      pragma[noinline]
+      private predicate exitBlock(PreBasicBlock bb, Callable c) {
+        exists(succExit(bb.getLastElement(), _)) and
+        c = bb.getEnclosingCallable()
+      }
+
+      private predicate outRefExitRead(PreBasicBlock bb, int i, LocalScopeVariable v) {
+        exitBlock(bb, v.getCallable()) and
+        i = bb.length() + 1 and
+        (v.isRef() or v.(Parameter).isOut())
+      }
+
+      private newtype RefKind =
+        Read()
+        or
+        Write(boolean certain) { certain = true or certain = false }
+
+      private predicate ref(PreBasicBlock bb, int i, SimpleAssignable a, RefKind k) {
+        (readAt(bb, i, _, a) or outRefExitRead(bb, i, a)) and
+        k = Read()
+        or
+        exists(AssignableDefinition def, boolean certain |
+          assignableDefAt(bb, i, def, a) |
+          if def.getTargetAccess().isRefArgument() then certain = false else certain = true and
+          k = Write(certain)
+        )
+      }
+
+      private int refRank(PreBasicBlock bb, int i, SimpleAssignable a, RefKind k) {
+        i = rank[result](int j | ref(bb, j, a, _)) and
+        ref(bb, i, a, k)
+      }
+
+      private int maxRefRank(PreBasicBlock bb, SimpleAssignable a) {
+        result = refRank(bb, _, a, _) and
+        not result + 1 = refRank(bb, _, a, _)
+      }
+
+      private int firstReadOrCertainWrite(PreBasicBlock bb, SimpleAssignable a) {
+        result = min(int r, RefKind k |
+          r = refRank(bb, _, a, k) and
+          k != Write(false)
+          |
+          r
+        )
+      }
+
+      predicate liveAtEntry(PreBasicBlock bb, SimpleAssignable a) {
+        refRank(bb, _, a, Read()) = firstReadOrCertainWrite(bb, a)
         or
-        def = TPhiPreSsaDef(bb, v) and i = -1
+        not exists(firstReadOrCertainWrite(bb, a)) and
+        liveAtExit(bb, a)
       }
 
-      private predicate readAt(PreBasicBlock bb, int i, LocalScopeVariableRead read, SimpleLocalScopeVariable v) {
-        read = bb.getElement(i) and
-        read.getTarget() = v
+      private predicate liveAtExit(PreBasicBlock bb, SimpleAssignable a) {
+        liveAtEntry(bb.getASuccessor(), a)
+      }
+
+      predicate assignableDefAtLive(PreBasicBlocks::PreBasicBlock bb, int i, AssignableDefinition def, SimpleAssignable a) {
+        assignableDefAt(bb, i, def, a) and
+        exists(int rnk |
+          rnk = refRank(bb, i, a, Write(_)) |
+          rnk + 1 = refRank(bb, _, a, Read())
+          or
+          rnk = maxRefRank(bb, a) and
+          liveAtExit(bb, a)
+        )
+      }
+
+      predicate defAt(PreBasicBlock bb, int i, Definition def, SimpleAssignable a) {
+        def = TExplicitPreSsaDef(bb, i, _, a)
+        or
+        def = TImplicitEntryPreSsaDef(_, bb, a) and i = -1
+        or
+        def = TPhiPreSsaDef(bb, a) and i = -1
       }
 
-      private predicate ssaRef(PreBasicBlock bb, int i, SimpleLocalScopeVariable v, SsaRefKind k) {
-        readAt(bb, i, _, v) and
+      private newtype SsaRefKind = SsaRead() or SsaDef()
+
+      private predicate ssaRef(PreBasicBlock bb, int i, SimpleAssignable a, SsaRefKind k) {
+        readAt(bb, i, _, a) and
         k = SsaRead()
         or
-        defAt(bb, i, _, v) and
+        defAt(bb, i, _, a) and
         k = SsaDef()
       }
 
-      private int ssaRefRank(PreBasicBlock bb, int i, SimpleLocalScopeVariable v, SsaRefKind k) {
-        i = rank[result](int j | ssaRef(bb, j, v, _)) and
-        ssaRef(bb, i, v, k)
+      private int ssaRefRank(PreBasicBlock bb, int i, SimpleAssignable a, SsaRefKind k) {
+        i = rank[result](int j | ssaRef(bb, j, a, _)) and
+        ssaRef(bb, i, a, k)
       }
 
-      private predicate defReachesRank(PreBasicBlock bb, Definition def, SimpleLocalScopeVariable v, int rnk) {
+      private predicate defReachesRank(PreBasicBlock bb, Definition def, SimpleAssignable a, int rnk) {
         exists(int i |
-          rnk = ssaRefRank(bb, i, v, SsaDef()) and
-          defAt(bb, i, def, v)
+          rnk = ssaRefRank(bb, i, a, SsaDef()) and
+          defAt(bb, i, def, a)
         )
         or
-        defReachesRank(bb, def, v, rnk - 1) and
-        rnk = ssaRefRank(bb, _, v, SsaRead())
+        defReachesRank(bb, def, a, rnk - 1) and
+        rnk = ssaRefRank(bb, _, a, SsaRead())
       }
 
-      private predicate reachesEndOf(Definition def, SimpleLocalScopeVariable v, PreBasicBlock bb) {
-        exists(int rnk |
-          defReachesRank(bb, def, v, rnk) and
-          rnk = max(ssaRefRank(bb, _, v, _))
+      private int maxSsaRefRank(PreBasicBlock bb, SimpleAssignable a) {
+        result = ssaRefRank(bb, _, a, _) and
+        not result + 1 = ssaRefRank(bb, _, a, _)
+      }
+
+      private predicate reachesEndOf(Definition def, SimpleAssignable a, PreBasicBlock bb) {
+        exists(int last |
+          last = maxSsaRefRank(bb, a) |
+          defReachesRank(bb, def, a, last)
         )
         or
         exists(PreBasicBlock mid |
-          reachesEndOf(def, v, mid) and
-          not exists(ssaRefRank(mid, _, v, SsaDef())) and
+          reachesEndOf(def, a, mid) and
+          not exists(ssaRefRank(mid, _, a, SsaDef())) and
           bb = mid.getASuccessor()
         )
       }
 
-      private predicate varOccursInBlock(SimpleLocalScopeVariable v, PreBasicBlock bb) {
-        exists(ssaRefRank(bb, _, v, _))
+      private predicate varOccursInBlock(SimpleAssignable a, PreBasicBlock bb) {
+        exists(ssaRefRank(bb, _, a, _))
       }
 
       pragma [nomagic]
-      private predicate blockPrecedesVar(SimpleLocalScopeVariable v, PreBasicBlock bb) {
-        varOccursInBlock(v, bb.getASuccessor*())
+      private predicate blockPrecedesVar(SimpleAssignable a, PreBasicBlock bb) {
+        varOccursInBlock(a, bb.getASuccessor*())
       }
 
-      private predicate varBlockReaches(SimpleLocalScopeVariable v, PreBasicBlock bb1, PreBasicBlock bb2) {
-        varOccursInBlock(v, bb1) and
+      private predicate varBlockReaches(SimpleAssignable a, PreBasicBlock bb1, PreBasicBlock bb2) {
+        varOccursInBlock(a, bb1) and
         bb2 = bb1.getASuccessor() and
-        blockPrecedesVar(v, bb2)
+        blockPrecedesVar(a, bb2)
         or
-        varBlockReachesRec(v, bb1, bb2) and
-        blockPrecedesVar(v, bb2)
+        varBlockReachesRec(a, bb1, bb2) and
+        blockPrecedesVar(a, bb2)
       }
 
       pragma [nomagic]
-      private predicate varBlockReachesRec(SimpleLocalScopeVariable v, PreBasicBlock bb1, PreBasicBlock bb2) {
+      private predicate varBlockReachesRec(SimpleAssignable a, PreBasicBlock bb1, PreBasicBlock bb2) {
         exists(PreBasicBlock mid |
-          varBlockReaches(v, bb1, mid) |
+          varBlockReaches(a, bb1, mid) |
           bb2 = mid.getASuccessor() and
-          not varOccursInBlock(v, mid)
+          not varOccursInBlock(a, mid)
         )
       }
 
-      private predicate varBlockStep(SimpleLocalScopeVariable v, PreBasicBlock bb1, PreBasicBlock bb2) {
-        varBlockReaches(v, bb1, bb2) and
-        varOccursInBlock(v, bb2)
+      private predicate varBlockStep(SimpleAssignable a, PreBasicBlock bb1, PreBasicBlock bb2) {
+        varBlockReaches(a, bb1, bb2) and
+        varOccursInBlock(a, bb2)
       }
 
-      private predicate adjacentVarRefs(SimpleLocalScopeVariable v, PreBasicBlock bb1, int i1, PreBasicBlock bb2, int i2) {
+      private predicate adjacentVarRefs(SimpleAssignable a, PreBasicBlock bb1, int i1, PreBasicBlock bb2, int i2) {
         exists(int rankix |
           bb1 = bb2 and
-          rankix = ssaRefRank(bb1, i1, v, _) and
-          rankix + 1 = ssaRefRank(bb2, i2, v, _)
+          rankix = ssaRefRank(bb1, i1, a, _) and
+          rankix + 1 = ssaRefRank(bb2, i2, a, _)
         )
         or
-        ssaRefRank(bb1, i1, v, _) = max(ssaRefRank(bb1, _, v, _)) and
-        varBlockStep(v, bb1, bb2) and
-        ssaRefRank(bb2, i2, v, _) = 1
+        ssaRefRank(bb1, i1, a, _) = maxSsaRefRank(bb1, a) and
+        varBlockStep(a, bb1, bb2) and
+        ssaRefRank(bb2, i2, a, _) = 1
+      }
+
+      predicate firstReadSameVar(Definition def, AssignableRead read) {
+        exists(SimpleAssignable a, PreBasicBlock b1, int i1, PreBasicBlock b2, int i2 |
+          adjacentVarRefs(a, b1, i1, b2, i2) and
+          defAt(b1, i1, def, a) and
+          readAt(b2, i2, read, a)
+        )
+      }
+
+      predicate adjacentReadPairSameVar(AssignableRead read1, AssignableRead read2) {
+        exists(SimpleAssignable a, PreBasicBlock bb1, int i1, PreBasicBlock bb2, int i2 |
+          adjacentVarRefs(a, bb1, i1, bb2, i2) and
+          readAt(bb1, i1, read1, a) and
+          readAt(bb2, i2, read2, a)
+        )
       }
 
-      predicate firstReadSameVar(Definition def, LocalScopeVariableRead read) {
-        exists(SimpleLocalScopeVariable v, PreBasicBlock b1, int i1, PreBasicBlock b2, int i2 |
-          adjacentVarRefs(v, b1, i1, b2, i2) and
-          defAt(b1, i1, def, v) and
-          readAt(b2, i2, read, v)
+      pragma[noinline]
+      private predicate ssaDefReachesEndOfBlockRec(PreBasicBlock bb, Definition def, SimpleAssignable a) {
+        exists(PreBasicBlock idom |
+          ssaDefReachesEndOfBlock(idom, def, a) |
+          idom.immediatelyDominates(bb)
         )
       }
 
-      predicate adjacentReadPairSameVar(LocalScopeVariableRead read1, LocalScopeVariableRead read2) {
-        exists(SimpleLocalScopeVariable v, PreBasicBlock bb1, int i1, PreBasicBlock bb2, int i2 |
-          adjacentVarRefs(v, bb1, i1, bb2, i2) and
-          readAt(bb1, i1, read1, v) and
-          readAt(bb2, i2, read2, v)
+      predicate ssaDefReachesEndOfBlock(PreBasicBlock bb, Definition def, SimpleAssignable a) {
+        exists(int last |
+          last = maxSsaRefRank(bb, a) |
+          defReachesRank(bb, def, a, last) and
+          liveAtExit(bb, a)
         )
+        or
+        ssaDefReachesEndOfBlockRec(bb, def, a) and
+        liveAtExit(bb, a) and
+        not ssaRef(bb, _, a, SsaDef())
       }
     }
 
@@ -3356,11 +3520,11 @@ module ControlFlow {
            * and `cb` can be reached from `read` without passing through another
            * condition that reads the same SSA variable.
            */
-          private predicate defConditionReachableFromRead(ConditionBlock cb, LocalScopeVariableRead read) {
+          private predicate defConditionReachableFromRead(ConditionBlock cb, AssignableRead read) {
             this.defCondition(cb) and
             read = cb.getLastElement()
             or
-            exists(LocalScopeVariableRead mid |
+            exists(AssignableRead mid |
               this.defConditionReachableFromRead(cb, mid) |
               adjacentReadPairSameVar(read, mid) and
               not this.defCondition(read)
@@ -3373,7 +3537,7 @@ module ControlFlow {
            * another condition that reads the same SSA variable.
            */
           private predicate firstDefCondition(ConditionBlock cb) {
-            exists(LocalScopeVariableRead read |
+            exists(AssignableRead read |
               this.defConditionReachableFromRead(cb, read) |
               firstReadSameVar(def, read)
             )
@@ -3381,7 +3545,7 @@ module ControlFlow {
 
           override predicate correlatesConditions(ConditionBlock cb1, ConditionBlock cb2, boolean inverted) {
             this.firstDefCondition(cb1) and
-            exists(LocalScopeVariableRead read1, LocalScopeVariableRead read2 |
+            exists(AssignableRead read1, AssignableRead read2 |
               read1 = cb1.getLastElement() and
               adjacentReadPairSameVar+(read1, read2) and
               read2 = cb2.getLastElement() and
@@ -3390,11 +3554,11 @@ module ControlFlow {
           }
 
           override Callable getEnclosingCallable() {
-            result = def.getVariable().getCallable()
+            result = def.getCallable()
           }
 
           override string toString() {
-            result = def.getVariable().toString()
+            result = def.getAssignable().toString()
           }
 
           override Location getLocation() {
@@ -3843,18 +4007,29 @@ module ControlFlow {
     private cached module Cached {
       private import semmle.code.csharp.controlflow.Guards as Guards
 
+      pragma[noinline]
+      private predicate phiNodeMaybeLive(PreBasicBlocks::PreBasicBlock bb, PreSsa::SimpleAssignable a) {
+        exists(PreBasicBlocks::PreBasicBlock def |
+          PreSsa::defAt(def, _, _, a) |
+          def.inDominanceFrontier(bb)
+        )
+      }
+
       cached
       newtype TPreSsaDef =
-        TExplicitPreSsaDef(PreBasicBlocks::PreBasicBlock bb, int i, AssignableDefinition def, LocalScopeVariable v) {
+        TExplicitPreSsaDef(PreBasicBlocks::PreBasicBlock bb, int i, AssignableDefinition def, PreSsa::SimpleAssignable a) {
           Guards::Internal::CachedWithCFG::forceCachingInSameStage() and
-          PreSsa::assignableDefAt(bb, i, def, v)
+          PreSsa::assignableDefAtLive(bb, i, def, a)
         }
         or
-        TPhiPreSsaDef(PreBasicBlocks::PreBasicBlock bb, LocalScopeVariable v) {
-          exists(PreBasicBlocks::PreBasicBlock def |
-            def.inDominanceFrontier(bb) |
-            PreSsa::defAt(def, _, _, v)
-          )
+        TImplicitEntryPreSsaDef(Callable c, PreBasicBlocks::PreBasicBlock bb, Assignable a) {
+          PreSsa::implicitEntryDef(c, bb, a) and
+          PreSsa::liveAtEntry(bb, a)
+        }
+        or
+        TPhiPreSsaDef(PreBasicBlocks::PreBasicBlock bb, PreSsa::SimpleAssignable a) {
+          phiNodeMaybeLive(bb, a) and
+          PreSsa::liveAtEntry(bb, a)
         }
 
       cached
diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/SSA.qll b/csharp/ql/src/semmle/code/csharp/dataflow/SSA.qll
index 863f46d8ca7a..ae2f0654f455 100644
--- a/csharp/ql/src/semmle/code/csharp/dataflow/SSA.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/SSA.qll
@@ -283,6 +283,11 @@ module Ssa {
       ref(bb, i, v, k)
     }
 
+    private int maxRefRank(BasicBlock bb, SourceVariable v) {
+      result = refRank(bb, _, v, _) and
+      not result + 1 = refRank(bb, _, v, _)
+    }
+
     /**
      * Gets the (1-based) rank of the first reference to `v` inside basic block `bb`
      * that is either a read or a certain write.
@@ -335,7 +340,7 @@ module Ssa {
     predicate liveAtRank(BasicBlock bb, int i, SourceVariable v, int rnk, ReadKind rk) {
       rnk = refRank(bb, i, v, _) and
       (
-        rnk = max(refRank(bb, _, v, _)) and
+        rnk = maxRefRank(bb, v) and
         liveAtExit(bb, v, rk)
         or
         ref(bb, i, v, Read(rk))
@@ -641,6 +646,11 @@ module Ssa {
       ssaRef(bb, i, v, k)
     }
 
+    private int maxSsaRefRank(BasicBlock bb, SourceVariable v) {
+      result = ssaRefRank(bb, _, v, _) and
+      not result + 1 = ssaRefRank(bb, _, v, _)
+    }
+
     /**
      * Holds if the non-trivial SSA definition `def` reaches rank index `rankix`
      * in its own basic block `bb`.
@@ -734,7 +744,7 @@ module Ssa {
         rankix + 1 = ssaRefRank(bb2, i2, v, _)
       )
       or
-      ssaRefRank(bb1, i1, v, _) = max(ssaRefRank(bb1, _, v, _)) and
+      ssaRefRank(bb1, i1, v, _) = maxSsaRefRank(bb1, v) and
       varBlockStep(v, bb1, bb2) and
       ssaRefRank(bb2, i2, v, _) = 1
     }
@@ -792,7 +802,7 @@ module Ssa {
           rnk + 1 = ssaRefRank(bb, _, v, SsaDef())
           or
           // No next reference to `v` inside `bb`
-          rnk = max(ssaRefRank(bb, _, v, _)) and
+          rnk = maxSsaRefRank(bb, v) and
           (
             // Read reaches end of enclosing callable
             not varBlockReaches(v, bb, _)
@@ -806,6 +816,21 @@ module Ssa {
         )
       }
 
+      pragma[noinline]
+      private predicate ssaDefReachesEndOfBlockRec(BasicBlock bb, TrackedDefinition def, TrackedVar v) {
+        exists(BasicBlock idom |
+          ssaDefReachesEndOfBlock(idom, def, v) |
+          /* The construction of SSA form ensures that each read of a variable is
+           * dominated by its definition. An SSA definition therefore reaches a
+           * control flow node if it is the _closest_ SSA definition that dominates
+           * the node. If two definitions dominate a node then one must dominate the
+           * other, so therefore the definition of _closest_ is given by the dominator
+           * tree. Thus, reaching definitions can be calculated in terms of dominance.
+           */
+          idom = bb.getImmediateDominator()
+        )
+      }
+
       /**
        * Holds if the non-trivial SSA definition of `v` at `def` reaches the end of a
        * basic block `bb`, at which point it is still live, without crossing another
@@ -813,26 +838,15 @@ module Ssa {
        */
       cached
       predicate ssaDefReachesEndOfBlock(BasicBlock bb, TrackedDefinition def, TrackedVar v) {
-        liveAtExit(bb, v, _) and
-        (
-          exists(int last |
-            last = max(ssaRefRank(bb, _, v, _)) |
-            ssaDefReachesRank(bb, def, last, v)
-          )
-          or
-          exists(BasicBlock idom |
-            /* The construction of SSA form ensures that each read of a variable is
-             * dominated by its definition. An SSA definition therefore reaches a
-             * control flow node if it is the _closest_ SSA definition that dominates
-             * the node. If two definitions dominate a node then one must dominate the
-             * other, so therefore the definition of _closest_ is given by the dominator
-             * tree. Thus, reaching definitions can be calculated in terms of dominance.
-             */
-            idom = bb.getImmediateDominator() and
-            ssaDefReachesEndOfBlock(idom, def, v) and
-            not exists(ssaRefRank(bb, _, v, SsaDef()))
-          )
+        exists(int last |
+          last = maxSsaRefRank(bb, v) |
+          ssaDefReachesRank(bb, def, last, v) and
+          liveAtExit(bb, v, _)
         )
+        or
+        ssaDefReachesEndOfBlockRec(bb, def, v) and
+        liveAtExit(bb, v, _) and
+        not ssaRef(bb, _, v, SsaDef())
       }
 
       /**
@@ -1896,14 +1910,18 @@ module Ssa {
       }
       or
       TPhiNode(TrackedVar v, ControlFlow::BasicBlocks::JoinBlock bb) {
+        phiNodeMaybeLive(bb, v) and
         liveAtEntry(bb, v, _)
-        and
-        exists(BasicBlock bb1, Definition def |
-          bb1.inDominanceFrontier(bb) and
-          definesAt(def, bb1, _, v)
-        )
       }
 
+    pragma[noinline]
+    private predicate phiNodeMaybeLive(ControlFlow::BasicBlocks::JoinBlock bb, TrackedVar v) {
+      exists(Definition def, BasicBlock bb1 |
+        definesAt(def, bb1, _, v) |
+        bb1.inDominanceFrontier(bb)
+      )
+    }
+
     /**
      * Holds if the SSA definition `def` defines source variable `v` at index `i`
      * in basic block `bb`. Phi nodes and entry nodes (captured variables and
diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/BaseSSA.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/BaseSSA.qll
index 9f005557d92a..367358931b18 100644
--- a/csharp/ql/src/semmle/code/csharp/dataflow/internal/BaseSSA.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/BaseSSA.qll
@@ -114,10 +114,9 @@ module BaseSsa {
    */
   cached AssignableRead getARead(AssignableDefinition def, SimpleLocalScopeVariable v) {
     exists(BasicBlock bb, int i, int rnk |
-      result.getTarget() = v and
       result.getAControlFlowNode() = bb.getNode(i) and
       rnk = ssaRefRank(bb, i, v, SsaRead())
-      |
+    |
       defReachesRank(bb, def, v, rnk)
       or
       reachesEndOf(def, v, bb.getAPredecessor()) and
diff --git a/csharp/ql/test/library-tests/dataflow/ssa/PreSsaConsistency.expected b/csharp/ql/test/library-tests/dataflow/ssa/PreSsaConsistency.expected
index e69de29bb2d1..4fa64b476744 100644
--- a/csharp/ql/test/library-tests/dataflow/ssa/PreSsaConsistency.expected
+++ b/csharp/ql/test/library-tests/dataflow/ssa/PreSsaConsistency.expected
@@ -0,0 +1,3 @@
+defReadInconsistency
+readReadInconsistency
+phiInconsistency
diff --git a/csharp/ql/test/library-tests/dataflow/ssa/PreSsaConsistency.ql b/csharp/ql/test/library-tests/dataflow/ssa/PreSsaConsistency.ql
index caa9144fe155..dea9b67b0593 100644
--- a/csharp/ql/test/library-tests/dataflow/ssa/PreSsaConsistency.ql
+++ b/csharp/ql/test/library-tests/dataflow/ssa/PreSsaConsistency.ql
@@ -1,11 +1,13 @@
 import csharp
 import ControlFlow::Internal
 
-predicate defReadInconsistency(AssignableRead ar, Expr e, boolean b) {
+query
+predicate defReadInconsistency(AssignableRead ar, Expr e, PreSsa::SimpleAssignable a, boolean b) {
   exists(AssignableDefinition def |
     e = def.getExpr() |
     b = true and
     exists(PreSsa::Definition ssaDef |
+      ssaDef.getAssignable() = a |
       PreSsa::firstReadSameVar(ssaDef, ar) and
       ssaDef.getDefinition() = def and
       not exists(Ssa::ExplicitDefinition edef |
@@ -18,7 +20,7 @@ predicate defReadInconsistency(AssignableRead ar, Expr e, boolean b) {
     exists(Ssa::ExplicitDefinition edef |
       edef.getADefinition() = def and
       edef.getAFirstRead() = ar and
-      def.getTarget() instanceof PreSsa::SimpleLocalScopeVariable and
+      def.getTarget() = a and
       not exists(PreSsa::Definition ssaDef |
         PreSsa::firstReadSameVar(ssaDef, ar) and
         ssaDef.getDefinition() = def
@@ -27,22 +29,48 @@ predicate defReadInconsistency(AssignableRead ar, Expr e, boolean b) {
   )
 }
 
-predicate readReadInconsistency(LocalScopeVariableRead read1, LocalScopeVariableRead read2, boolean b) {
+query
+predicate readReadInconsistency(LocalScopeVariableRead read1, LocalScopeVariableRead read2, PreSsa::SimpleAssignable a, boolean b) {
   b = true and
+  a = read1.getTarget() and
   PreSsa::adjacentReadPairSameVar(read1, read2) and
   not Ssa::Internal::adjacentReadPairSameVar(read1, read2)
   or
   b = false and
+  a = read1.getTarget() and
   Ssa::Internal::adjacentReadPairSameVar(read1, read2) and
-  read1.getTarget() instanceof PreSsa::SimpleLocalScopeVariable and
+  read1.getTarget() instanceof PreSsa::SimpleAssignable and
   not PreSsa::adjacentReadPairSameVar(read1, read2)
 }
 
-from Element e1, Element e2, boolean b, string s
-where
-  defReadInconsistency(e1, e2, b) and
-  s = "def-read inconsistency (" + b + ")"
-  or
-  readReadInconsistency(e1, e2, b) and
-  s = "read-read inconsistency (" + b + ")"
-select e1, e2, s
+query
+predicate phiInconsistency(ControlFlowElement cfe, Expr e, PreSsa::SimpleAssignable a, boolean b) {
+  exists(AssignableDefinition adef |
+    e = adef.getExpr() |
+    b = true and
+    exists(PreSsa::Definition def |
+      a = def.getAssignable() |
+      adef = def.getAPhiInput+().getDefinition() and
+      cfe = def.getBasicBlock().getFirstElement() and
+      not exists(Ssa::PhiNode phi, ControlFlow::BasicBlock bb, Ssa::ExplicitDefinition edef |
+        edef = phi.getAnUltimateDefinition() |
+        edef.getADefinition() = adef and
+        phi.definesAt(bb, _) and
+        cfe = bb.getFirstNode().getElement()
+      )
+    )
+    or
+    b = false and
+    exists(Ssa::PhiNode phi, ControlFlow::BasicBlock bb, Ssa::ExplicitDefinition edef |
+      a = phi.getSourceVariable().getAssignable() |
+      edef = phi.getAnUltimateDefinition() and
+      edef.getADefinition() = adef and
+      phi.definesAt(bb, _) and
+      cfe = bb.getFirstNode().getElement() and
+      not exists(PreSsa::Definition def |
+        adef = def.getAPhiInput+().getDefinition() and
+        cfe = def.getBasicBlock().getFirstElement()
+      )
+    )
+  )
+}