diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll
index bccadc5fee03..61787debca4f 100644
--- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll
+++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll
@@ -734,7 +734,7 @@ private predicate variableReadPseudo(ControlFlow::BasicBlock bb, int i, Ssa::Sou
 }
 
 pragma[noinline]
-private predicate adjacentDefRead(
+deprecated private predicate adjacentDefRead(
   Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2,
   SsaInput::SourceVariable v
 ) {
@@ -742,7 +742,7 @@ private predicate adjacentDefRead(
   v = def.getSourceVariable()
 }
 
-private predicate adjacentDefReachesRead(
+deprecated private predicate adjacentDefReachesRead(
   Definition def, SsaInput::SourceVariable v, SsaInput::BasicBlock bb1, int i1,
   SsaInput::BasicBlock bb2, int i2
 ) {
@@ -760,18 +760,7 @@ private predicate adjacentDefReachesRead(
   )
 }
 
-/** Same as `adjacentDefRead`, but skips uncertain reads. */
-pragma[nomagic]
-private predicate adjacentDefSkipUncertainReads(
-  Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
-) {
-  exists(SsaInput::SourceVariable v |
-    adjacentDefReachesRead(def, v, bb1, i1, bb2, i2) and
-    SsaInput::variableRead(bb2, i2, v, true)
-  )
-}
-
-private predicate adjacentDefReachesUncertainRead(
+deprecated private predicate adjacentDefReachesUncertainRead(
   Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
 ) {
   exists(SsaInput::SourceVariable v |
@@ -933,10 +922,8 @@ private module Cached {
    */
   cached
   predicate firstReadSameVar(Definition def, ControlFlow::Node cfn) {
-    exists(ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2 |
-      def.definesAt(_, bb1, i1) and
-      adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and
-      cfn = bb2.getNode(i2)
+    exists(ControlFlow::BasicBlock bb, int i |
+      Impl::firstUse(def, bb, i, true) and cfn = bb.getNode(i)
     )
   }
 
@@ -947,25 +934,17 @@ private module Cached {
    */
   cached
   predicate adjacentReadPairSameVar(Definition def, ControlFlow::Node cfn1, ControlFlow::Node cfn2) {
-    exists(ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2 |
+    exists(
+      ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2,
+      Ssa::SourceVariable v
+    |
+      Impl::ssaDefReachesRead(v, def, bb1, i1) and
+      Impl::adjacentUseUse(bb1, i1, bb2, i2, v, true) and
       cfn1 = bb1.getNode(i1) and
-      variableReadActual(bb1, i1, _) and
-      adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and
       cfn2 = bb2.getNode(i2)
     )
   }
 
-  cached
-  predicate lastRefBeforeRedef(Definition def, ControlFlow::BasicBlock bb, int i, Definition next) {
-    Impl::lastRefRedef(def, bb, i, next) and
-    not SsaInput::variableRead(bb, i, def.getSourceVariable(), false)
-    or
-    exists(SsaInput::BasicBlock bb0, int i0 |
-      Impl::lastRefRedef(def, bb0, i0, next) and
-      adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
-    )
-  }
-
   cached
   Definition uncertainWriteDefinitionInput(UncertainWriteDefinition def) {
     Impl::uncertainWriteDefinitionInput(def, result)
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll b/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll
index bcc68cfd8739..d5fdf4ef829a 100644
--- a/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll
@@ -490,26 +490,11 @@ private module Cached {
     )
   }
 
-  pragma[nomagic]
-  private predicate captureDefReaches(Definition def, SsaInput::BasicBlock bb2, int i2) {
-    variableCapture(def.getSourceVariable(), _, _, _) and
-    exists(SsaInput::BasicBlock bb1, int i1 |
-      Impl::adjacentDefRead(def, bb1, i1, bb2, i2) and
-      def.definesAt(_, bb1, i1)
-    )
-    or
-    exists(SsaInput::BasicBlock bb3, int i3 |
-      captureDefReaches(def, bb3, i3) and
-      SsaInput::variableRead(bb3, i3, _, _) and
-      Impl::adjacentDefRead(def, bb3, i3, bb2, i2)
-    )
-  }
-
   /** Holds if `init` is a closure variable that captures the value of `capturedvar`. */
   cached
   predicate captures(SsaImplicitInit init, SsaVariable capturedvar) {
     exists(BasicBlock bb, int i |
-      captureDefReaches(capturedvar, bb, i) and
+      Impl::ssaDefReachesRead(_, capturedvar, bb, i) and
       variableCapture(capturedvar.getSourceVariable(), init.getSourceVariable(), bb, i)
     )
   }
@@ -523,34 +508,15 @@ private module Cached {
     Impl::uncertainWriteDefinitionInput(redef, def)
   }
 
-  pragma[nomagic]
-  private predicate defReaches(Definition def, DataFlowIntegration::Node node) {
-    exists(DataFlowIntegration::SsaDefinitionExtNode nodeFrom |
-      nodeFrom.getDefinitionExt() = def and
-      DataFlowIntegrationImpl::localFlowStep(_, nodeFrom, node, false)
-    )
-    or
-    exists(DataFlowIntegration::Node mid |
-      defReaches(def, mid) and
-      DataFlowIntegrationImpl::localFlowStep(_, mid, node, _)
-    |
-      // flow into phi input node
-      mid instanceof DataFlowIntegration::SsaInputNode
-      or
-      // flow into definition
-      mid instanceof DataFlowIntegration::SsaDefinitionExtNode
-    )
-  }
-
   /**
    * Holds if the value defined at `def` can reach `use` without passing through
    * any other uses, but possibly through phi nodes and uncertain implicit updates.
    */
   cached
   predicate firstUse(Definition def, VarRead use) {
-    exists(DataFlowIntegration::ExprNode nodeTo |
-      nodeTo.getExpr() = use and
-      defReaches(def, nodeTo)
+    exists(BasicBlock bb, int i |
+      Impl::firstUse(def, bb, i, _) and
+      use.getControlFlowNode() = bb.getNode(i)
     )
   }
 
@@ -609,30 +575,6 @@ private module Cached {
 
   cached
   module SsaPublic {
-    pragma[nomagic]
-    private predicate useReaches(VarRead use, DataFlowIntegration::Node node, boolean sameVar) {
-      exists(DataFlowIntegration::ExprNode nodeFrom |
-        nodeFrom.getExpr() = use and
-        DataFlowIntegration::localFlowStep(_, nodeFrom, node, true) and
-        sameVar = true
-      )
-      or
-      exists(DataFlowIntegration::Node mid, boolean sameVarMid |
-        useReaches(use, mid, sameVarMid) and
-        DataFlowIntegration::localFlowStep(_, mid, node, _)
-      |
-        exists(Impl::DefinitionExt def |
-          // flow into definition
-          def = mid.(DataFlowIntegration::SsaDefinitionExtNode).getDefinitionExt()
-          or
-          // flow into phi input node
-          def = mid.(DataFlowIntegration::SsaInputNode).getDefinitionExt()
-        |
-          if def instanceof Impl::PhiReadNode then sameVar = sameVarMid else sameVar = false
-        )
-      )
-    }
-
     /**
      * Holds if `use1` and `use2` form an adjacent use-use-pair of the same SSA
      * variable, that is, the value read in `use1` can reach `use2` without passing
@@ -640,9 +582,10 @@ private module Cached {
      */
     cached
     predicate adjacentUseUseSameVar(VarRead use1, VarRead use2) {
-      exists(DataFlowIntegration::ExprNode nodeTo |
-        nodeTo.getExpr() = use2 and
-        useReaches(use1, nodeTo, true)
+      exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
+        use1.getControlFlowNode() = bb1.getNode(i1) and
+        use2.getControlFlowNode() = bb2.getNode(i2) and
+        Impl::adjacentUseUse(bb1, i1, bb2, i2, _, true)
       )
     }
 
@@ -654,9 +597,10 @@ private module Cached {
      */
     cached
     predicate adjacentUseUse(VarRead use1, VarRead use2) {
-      exists(DataFlowIntegration::ExprNode nodeTo |
-        nodeTo.getExpr() = use2 and
-        useReaches(use1, nodeTo, _)
+      exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
+        use1.getControlFlowNode() = bb1.getNode(i1) and
+        use2.getControlFlowNode() = bb2.getNode(i2) and
+        Impl::adjacentUseUse(bb1, i1, bb2, i2, _, _)
       )
     }
   }
diff --git a/java/ql/test/library-tests/dataflow/ssa/A.java b/java/ql/test/library-tests/dataflow/ssa/A.java
new file mode 100644
index 000000000000..79303697d646
--- /dev/null
+++ b/java/ql/test/library-tests/dataflow/ssa/A.java
@@ -0,0 +1,24 @@
+public class A {
+  Object source() { return null; }
+  void sink(Object o) { }
+
+  boolean isSafe(Object o) { return o == null; }
+
+  void foo() {
+    Object x = source();
+    if (!isSafe(x)) {
+      x = null;
+    }
+    sink(x);
+
+    x = source();
+    if (!isSafe(x)) {
+      if (isSafe(x)) {
+        sink(x);
+      } else {
+        throw new RuntimeException();
+      }
+    }
+    sink(x);
+  }
+}
diff --git a/java/ql/test/library-tests/dataflow/ssa/test.expected b/java/ql/test/library-tests/dataflow/ssa/test.expected
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/java/ql/test/library-tests/dataflow/ssa/test.ql b/java/ql/test/library-tests/dataflow/ssa/test.ql
new file mode 100644
index 000000000000..cb601dab5eb1
--- /dev/null
+++ b/java/ql/test/library-tests/dataflow/ssa/test.ql
@@ -0,0 +1,31 @@
+import java
+import semmle.code.java.controlflow.Guards
+import semmle.code.java.dataflow.DataFlow
+
+private predicate isSafe(Guard g, Expr checked, boolean branch) {
+  exists(MethodCall mc | g = mc |
+    mc.getMethod().hasName("isSafe") and
+    checked = mc.getAnArgument() and
+    branch = true
+  )
+}
+
+module TestConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) {
+    source.asExpr().(MethodCall).getMethod().hasName("source")
+  }
+
+  predicate isSink(DataFlow::Node sink) {
+    exists(MethodCall mc | mc.getMethod().hasName("sink") and mc.getAnArgument() = sink.asExpr())
+  }
+
+  predicate isBarrier(DataFlow::Node node) {
+    node = DataFlow::BarrierGuard<isSafe/3>::getABarrierNode()
+  }
+}
+
+module Flow = DataFlow::Global<TestConfig>;
+
+from DataFlow::Node source, DataFlow::Node sink
+where Flow::flow(source, sink)
+select source, sink
diff --git a/java/ql/test/library-tests/pattern-switch/dfg/GuardTest.java b/java/ql/test/library-tests/pattern-switch/dfg/GuardTest.java
index e0d3494aa208..f49b69f3b610 100644
--- a/java/ql/test/library-tests/pattern-switch/dfg/GuardTest.java
+++ b/java/ql/test/library-tests/pattern-switch/dfg/GuardTest.java
@@ -24,13 +24,6 @@ case String s when isSafe(s):
         break;
 
     }
-
-    String s2 = "string";
-
-    if (!isSafe(s2)) {
-      s2 = null;
-    }
-    sink(s2);
   }
 
 }
diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll
index 7185f0389aaa..b8757e489dcf 100644
--- a/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll
+++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll
@@ -222,15 +222,6 @@ private predicate hasVariableReadWithCapturedWrite(
   variableReadActualInOuterScope(bb, i, v, scope)
 }
 
-pragma[noinline]
-private predicate adjacentDefRead(
-  Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2,
-  SsaInput::SourceVariable v
-) {
-  Impl::adjacentDefRead(def, bb1, i1, bb2, i2) and
-  v = def.getSourceVariable()
-}
-
 pragma[noinline]
 deprecated private predicate adjacentDefReadExt(
   DefinitionExt def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2,
@@ -240,22 +231,6 @@ deprecated private predicate adjacentDefReadExt(
   v = def.getSourceVariable()
 }
 
-private predicate adjacentDefReachesRead(
-  Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
-) {
-  exists(SsaInput::SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
-    def.definesAt(v, bb1, i1)
-    or
-    SsaInput::variableRead(bb1, i1, v, true)
-  )
-  or
-  exists(SsaInput::BasicBlock bb3, int i3 |
-    adjacentDefReachesRead(def, bb1, i1, bb3, i3) and
-    SsaInput::variableRead(bb3, i3, _, false) and
-    Impl::adjacentDefRead(def, bb3, i3, bb2, i2)
-  )
-}
-
 deprecated private predicate adjacentDefReachesReadExt(
   DefinitionExt def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
 ) {
@@ -272,15 +247,6 @@ deprecated private predicate adjacentDefReachesReadExt(
   )
 }
 
-/** Same as `adjacentDefRead`, but skips uncertain reads. */
-pragma[nomagic]
-private predicate adjacentDefSkipUncertainReads(
-  Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
-) {
-  adjacentDefReachesRead(def, bb1, i1, bb2, i2) and
-  SsaInput::variableRead(bb2, i2, _, true)
-}
-
 deprecated private predicate adjacentDefReachesUncertainReadExt(
   DefinitionExt def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
 ) {
@@ -391,11 +357,7 @@ private module Cached {
    */
   cached
   predicate firstRead(Definition def, VariableReadAccessCfgNode read) {
-    exists(Cfg::BasicBlock bb1, int i1, Cfg::BasicBlock bb2, int i2 |
-      def.definesAt(_, bb1, i1) and
-      adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and
-      read = bb2.getNode(i2)
-    )
+    exists(Cfg::BasicBlock bb, int i | Impl::firstUse(def, bb, i, true) and read = bb.getNode(i))
   }
 
   /**
@@ -407,10 +369,10 @@ private module Cached {
   predicate adjacentReadPair(
     Definition def, VariableReadAccessCfgNode read1, VariableReadAccessCfgNode read2
   ) {
-    exists(Cfg::BasicBlock bb1, int i1, Cfg::BasicBlock bb2, int i2 |
+    exists(Cfg::BasicBlock bb1, int i1, Cfg::BasicBlock bb2, int i2, LocalVariable v |
+      Impl::ssaDefReachesRead(v, def, bb1, i1) and
+      Impl::adjacentUseUse(bb1, i1, bb2, i2, v, true) and
       read1 = bb1.getNode(i1) and
-      variableReadActual(bb1, i1, _) and
-      adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and
       read2 = bb2.getNode(i2)
     )
   }
diff --git a/ruby/ql/test/library-tests/variables/ssa.expected b/ruby/ql/test/library-tests/variables/ssa.expected
index 05acf5dbb59e..b998016a39ff 100644
--- a/ruby/ql/test/library-tests/variables/ssa.expected
+++ b/ruby/ql/test/library-tests/variables/ssa.expected
@@ -527,7 +527,6 @@ adjacentReads
 | nested_scopes.rb:8:5:35:7 | self (N) | nested_scopes.rb:8:5:35:7 | self | nested_scopes.rb:30:16:30:19 | self | nested_scopes.rb:34:7:34:12 | self |
 | nested_scopes.rb:13:11:13:11 | a | nested_scopes.rb:13:11:13:11 | a | nested_scopes.rb:14:16:14:16 | a | nested_scopes.rb:15:11:15:11 | a |
 | nested_scopes.rb:27:7:29:9 | self (show) | nested_scopes.rb:27:7:29:9 | self | nested_scopes.rb:28:11:28:16 | self | nested_scopes.rb:28:16:28:16 | self |
-| nested_scopes.rb:30:16:30:19 | self (class << ...) | nested_scopes.rb:30:7:33:9 | self | nested_scopes.rb:30:16:30:19 | self | nested_scopes.rb:32:11:32:16 | self |
 | parameters.rb:1:9:5:3 | <captured entry> self | parameters.rb:1:1:62:1 | self | parameters.rb:3:4:3:9 | self | parameters.rb:4:4:4:9 | self |
 | parameters.rb:7:26:7:31 | pizzas | parameters.rb:7:26:7:31 | pizzas | parameters.rb:8:6:8:11 | pizzas | parameters.rb:11:14:11:19 | pizzas |
 | parameters.rb:25:1:28:3 | self (opt_param) | parameters.rb:25:1:28:3 | self | parameters.rb:26:3:26:11 | self | parameters.rb:27:3:27:11 | self |
diff --git a/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll b/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll
index ce45059ec37e..430049a5006d 100644
--- a/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll
+++ b/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll
@@ -120,14 +120,6 @@ module ExposedForTestingOnly {
   predicate phiHasInputFromBlockExt = Impl::phiHasInputFromBlockExt/3;
 }
 
-pragma[noinline]
-private predicate adjacentDefRead(
-  Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2, SsaInput::SourceVariable v
-) {
-  Impl::adjacentDefRead(def, bb1, i1, bb2, i2) and
-  v = def.getSourceVariable()
-}
-
 /** Holds if `v` is read at index `i` in basic block `bb`. */
 private predicate variableReadActual(BasicBlock bb, int i, Variable v) {
   exists(VariableAccess read |
@@ -167,31 +159,6 @@ private predicate hasVariableReadWithCapturedWrite(
   variableReadActualInOuterScope(bb, i, v, scope)
 }
 
-private predicate adjacentDefReachesRead(
-  Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
-) {
-  exists(SsaInput::SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
-    def.definesAt(v, bb1, i1)
-    or
-    SsaInput::variableRead(bb1, i1, v, true)
-  )
-  or
-  exists(BasicBlock bb3, int i3 |
-    adjacentDefReachesRead(def, bb1, i1, bb3, i3) and
-    SsaInput::variableRead(bb3, i3, _, false) and
-    Impl::adjacentDefRead(def, bb3, i3, bb2, i2)
-  )
-}
-
-/** Same as `adjacentDefRead`, but skips uncertain reads. */
-pragma[nomagic]
-private predicate adjacentDefSkipUncertainReads(
-  Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
-) {
-  adjacentDefReachesRead(def, bb1, i1, bb2, i2) and
-  SsaInput::variableRead(bb2, i2, _, true)
-}
-
 private VariableAccess getACapturedVariableAccess(BasicBlock bb, Variable v) {
   result = bb.getANode().getAstNode() and
   result.isCapture() and
@@ -314,11 +281,7 @@ private module Cached {
    */
   cached
   predicate firstRead(Definition def, CfgNode read) {
-    exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
-      def.definesAt(_, bb1, i1) and
-      adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and
-      read = bb2.getNode(i2)
-    )
+    exists(BasicBlock bb, int i | Impl::firstUse(def, bb, i, true) and read = bb.getNode(i))
   }
 
   /**
@@ -328,10 +291,10 @@ private module Cached {
    */
   cached
   predicate adjacentReadPair(Definition def, CfgNode read1, CfgNode read2) {
-    exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
+    exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2, Variable v |
+      Impl::ssaDefReachesRead(v, def, bb1, i1) and
+      Impl::adjacentUseUse(bb1, i1, bb2, i2, v, true) and
       read1 = bb1.getNode(i1) and
-      variableReadActual(bb1, i1, _) and
-      adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and
       read2 = bb2.getNode(i2)
     )
   }
diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll
index dacc323f43e6..407169cc6be7 100644
--- a/shared/ssa/codeql/ssa/Ssa.qll
+++ b/shared/ssa/codeql/ssa/Ssa.qll
@@ -114,43 +114,41 @@ module Make<LocationSig Location, InputSig<Location> Input> {
   }
 
   /**
-   * Liveness analysis (based on source variables) to restrict the size of the
-   * SSA representation.
+   * A classification of variable references into reads and
+   * (certain or uncertain) writes / definitions.
    */
-  private module Liveness {
-    /**
-     * A classification of variable references into reads (of a given kind) and
-     * (certain or uncertain) writes.
-     */
-    private newtype TRefKind =
-      Read(boolean certain) { certain in [false, true] } or
-      Write(boolean certain) { certain in [false, true] }
-
-    private class RefKind extends TRefKind {
-      string toString() {
-        exists(boolean certain | this = Read(certain) and result = "read (" + certain + ")")
-        or
-        exists(boolean certain | this = Write(certain) and result = "write (" + certain + ")")
-      }
-
-      int getOrder() {
-        this = Read(_) and
-        result = 0
-        or
-        this = Write(_) and
-        result = 1
-      }
+  private newtype TRefKind =
+    Read() or
+    Write(boolean certain) { certain in [false, true] } or
+    Def()
+
+  private class RefKind extends TRefKind {
+    string toString() {
+      this = Read() and result = "read"
+      or
+      exists(boolean certain | this = Write(certain) and result = "write (" + certain + ")")
+      or
+      this = Def() and result = "def"
     }
 
-    /**
-     * Holds if the `i`th node of basic block `bb` is a reference to `v` of kind `k`.
-     */
-    predicate ref(BasicBlock bb, int i, SourceVariable v, RefKind k) {
-      exists(boolean certain | variableRead(bb, i, v, certain) | k = Read(certain))
+    int getOrder() {
+      this = Read() and
+      result = 0
       or
-      exists(boolean certain | variableWrite(bb, i, v, certain) | k = Write(certain))
+      this = Write(_) and
+      result = 1
+      or
+      this = Def() and
+      result = 1
     }
+  }
+
+  /**
+   * Holds if the `i`th node of basic block `bb` is a reference to `v` of kind `k`.
+   */
+  private signature predicate refSig(BasicBlock bb, int i, SourceVariable v, RefKind k);
 
+  private module RankRefs<refSig/4 ref> {
     private newtype OrderedRefIndex =
       MkOrderedRefIndex(int i, int tag) {
         exists(RefKind rk | ref(_, i, _, rk) | tag = rk.getOrder())
@@ -168,7 +166,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
      *
      * Reads are considered before writes when they happen at the same index.
      */
-    private int refRank(BasicBlock bb, int i, SourceVariable v, RefKind k) {
+    int refRank(BasicBlock bb, int i, SourceVariable v, RefKind k) {
       refOrd(bb, i, v, k, _) =
         rank[result](int j, int ord, OrderedRefIndex res |
           res = refOrd(bb, j, v, _, ord)
@@ -177,18 +175,39 @@ module Make<LocationSig Location, InputSig<Location> Input> {
         )
     }
 
-    private int maxRefRank(BasicBlock bb, SourceVariable v) {
+    int maxRefRank(BasicBlock bb, SourceVariable v) {
       result = refRank(bb, _, v, _) and
       not result + 1 = refRank(bb, _, v, _)
     }
+  }
 
-    predicate lastRefIsRead(BasicBlock bb, SourceVariable v) {
-      maxRefRank(bb, v) = refRank(bb, _, v, Read(_))
+  /**
+   * Liveness analysis (based on source variables) to restrict the size of the
+   * SSA representation.
+   */
+  private module Liveness {
+    /**
+     * Holds if the `i`th node of basic block `bb` is a reference to `v` of kind `k`.
+     */
+    predicate varRef(BasicBlock bb, int i, SourceVariable v, RefKind k) {
+      variableRead(bb, i, v, _) and k = Read()
+      or
+      exists(boolean certain | variableWrite(bb, i, v, certain) | k = Write(certain))
     }
 
+    private import RankRefs<varRef/4>
+
     /**
      * Gets the (1-based) rank of the first reference to `v` inside basic block `bb`
      * that is either a read or a certain write.
+     *
+     * Note that uncertain writes have no impact on liveness: a variable is
+     * live before an uncertain write if and only if it is live after.
+     * The reference identified here therefore determines liveness at the
+     * beginning of `bb`: if it is a read then the variable is live and if it
+     * is a write then it is not. For basic blocks without reads or certain
+     * writes, liveness at the beginning of the block is equivalent to liveness
+     * at the end of the block.
      */
     private int firstReadOrCertainWrite(BasicBlock bb, SourceVariable v) {
       result =
@@ -205,7 +224,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
      */
     predicate liveAtEntry(BasicBlock bb, SourceVariable v) {
       // The first read or certain write to `v` inside `bb` is a read
-      refRank(bb, _, v, Read(_)) = firstReadOrCertainWrite(bb, v)
+      refRank(bb, _, v, Read()) = firstReadOrCertainWrite(bb, v)
       or
       // There is no certain write to `v` inside `bb`, but `v` is live at entry
       // to a successor basic block of `bb`
@@ -221,19 +240,17 @@ module Make<LocationSig Location, InputSig<Location> Input> {
     }
 
     /**
-     * Holds if variable `v` is live in basic block `bb` at index `i`.
-     * The rank of `i` is `rnk` as defined by `refRank()`.
+     * Holds if variable `v` is live in basic block `bb` at rank `rnk`.
      */
-    private predicate liveAtRank(BasicBlock bb, int i, SourceVariable v, int rnk) {
-      exists(RefKind kind | rnk = refRank(bb, i, v, kind) |
+    private predicate liveAtRank(BasicBlock bb, SourceVariable v, int rnk) {
+      exists(RefKind kind | rnk = refRank(bb, _, v, kind) |
         rnk = maxRefRank(bb, v) and
         liveAtExit(bb, v)
         or
-        ref(bb, i, v, kind) and
-        kind = Read(_)
+        kind = Read()
         or
         exists(RefKind nextKind |
-          liveAtRank(bb, _, v, rnk + 1) and
+          liveAtRank(bb, v, rnk + 1) and
           rnk + 1 = refRank(bb, _, v, nextKind) and
           nextKind != Write(true)
         )
@@ -245,7 +262,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
      * index `i` inside basic block `bb`.
      */
     predicate liveAfterWrite(BasicBlock bb, int i, SourceVariable v) {
-      exists(int rnk | rnk = refRank(bb, i, v, Write(_)) | liveAtRank(bb, i, v, rnk))
+      exists(int rnk | rnk = refRank(bb, i, v, Write(_)) | liveAtRank(bb, v, rnk))
     }
   }
 
@@ -289,13 +306,29 @@ module Make<LocationSig Location, InputSig<Location> Input> {
   pragma[nomagic]
   private predicate inReadDominanceFrontier(BasicBlock bb, SourceVariable v) {
     exists(BasicBlock readbb | inDominanceFrontier(readbb, bb) |
-      lastRefIsRead(readbb, v)
+      ssaDefReachesRead(v, _, readbb, _) and
+      not variableWrite(readbb, _, v, _)
       or
-      exists(TPhiReadNode(v, readbb)) and
-      not ref(readbb, _, v, _)
+      synthPhiRead(readbb, v) and
+      not varRef(readbb, _, v, _)
     )
   }
 
+  /**
+   * Holds if we should synthesize a pseudo-read of `v` at the beginning of `bb`.
+   *
+   * These reads are named phi-reads, since they are constructed in the same
+   * way as ordinary phi nodes except all reads are treated as potential
+   * "definitions". This ensures that use-use flow has the same dominance
+   * properties as def-use flow.
+   */
+  private predicate synthPhiRead(BasicBlock bb, SourceVariable v) {
+    inReadDominanceFrontier(bb, v) and
+    liveAtEntry(bb, v) and
+    // no need to create a phi-read if there is already a normal phi
+    not any(PhiNode def).definesAt(v, bb, _)
+  }
+
   cached
   private newtype TDefinitionExt =
     TWriteDef(SourceVariable v, BasicBlock bb, int i) {
@@ -306,15 +339,273 @@ module Make<LocationSig Location, InputSig<Location> Input> {
       inDefDominanceFrontier(bb, v) and
       liveAtEntry(bb, v)
     } or
-    TPhiReadNode(SourceVariable v, BasicBlock bb) {
-      inReadDominanceFrontier(bb, v) and
-      liveAtEntry(bb, v) and
-      // no need to create a phi-read if there is already a normal phi
-      not any(PhiNode def).definesAt(v, bb, _)
-    }
+    TPhiReadNode(SourceVariable v, BasicBlock bb) { synthPhiRead(bb, v) }
 
   private class TDefinition = TWriteDef or TPhiNode;
 
+  private module SsaDefReachesNew {
+    /**
+     * Holds if the `i`th node of basic block `bb` is a reference to `v`,
+     * either a read (when `k` is `Read()`) or an SSA definition (when
+     * `k` is `Def()`).
+     *
+     * Unlike `Liveness::varRef`, this includes `phi` nodes and pseudo-reads
+     * associated with uncertain writes.
+     */
+    pragma[nomagic]
+    predicate ssaRef(BasicBlock bb, int i, SourceVariable v, RefKind k) {
+      variableRead(bb, i, v, _) and
+      k = Read()
+      or
+      variableWrite(bb, i, v, false) and
+      k = Read()
+      or
+      any(Definition def).definesAt(v, bb, i) and
+      k = Def()
+    }
+
+    private import RankRefs<ssaRef/4>
+
+    /**
+     * Holds if the SSA definition `def` reaches rank index `rnk` in its own
+     * basic block `bb`.
+     */
+    predicate ssaDefReachesRank(BasicBlock bb, Definition def, int rnk, SourceVariable v) {
+      exists(int i |
+        rnk = refRank(bb, i, v, Def()) and
+        def.definesAt(v, bb, i)
+      )
+      or
+      ssaDefReachesRank(bb, def, rnk - 1, v) and
+      rnk = refRank(bb, _, v, Read())
+    }
+
+    /**
+     * Holds if `v` is live at the end of basic block `bb` with the same value as at
+     * the end of the immediate dominator, `idom`, of `bb`.
+     */
+    pragma[nomagic]
+    private predicate liveThrough(BasicBlock idom, BasicBlock bb, SourceVariable v) {
+      idom = getImmediateBasicBlockDominator(bb) and
+      liveAtExit(bb, v) and
+      not any(Definition def).definesAt(v, bb, _)
+    }
+
+    /**
+     * Holds if the SSA definition of `v` at `def` reaches the end of basic
+     * block `bb`, at which point it is still live, without crossing another
+     * SSA definition of `v`.
+     */
+    pragma[nomagic]
+    predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable v) {
+      exists(int last |
+        last = maxRefRank(pragma[only_bind_into](bb), pragma[only_bind_into](v)) and
+        ssaDefReachesRank(bb, def, last, v) and
+        liveAtExit(bb, 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.
+        ssaDefReachesEndOfBlock(idom, def, v) and
+        liveThrough(idom, bb, v)
+      )
+    }
+
+    /**
+     * Holds if the SSA definition of `v` at `def` reaches index `i` in its own
+     * basic block `bb`, without crossing another SSA definition of `v`.
+     */
+    predicate ssaDefReachesReadWithinBlock(SourceVariable v, Definition def, BasicBlock bb, int i) {
+      exists(int rnk |
+        ssaDefReachesRank(bb, def, rnk, v) and
+        rnk = refRank(bb, i, v, Read())
+      )
+    }
+
+    /**
+     * Holds if the SSA definition of `v` at `def` reaches a read at index `i` in
+     * basic block `bb`, without crossing another SSA definition of `v`.
+     */
+    pragma[nomagic]
+    predicate ssaDefReachesRead(SourceVariable v, Definition def, BasicBlock bb, int i) {
+      ssaDefReachesReadWithinBlock(v, def, bb, i)
+      or
+      ssaRef(bb, i, v, Read()) and
+      ssaDefReachesEndOfBlock(getImmediateBasicBlockDominator(bb), def, v) and
+      not ssaDefReachesReadWithinBlock(v, _, bb, i)
+    }
+
+    predicate uncertainWriteDefinitionInput(UncertainWriteDefinition def, Definition inp) {
+      exists(SourceVariable v, BasicBlock bb, int i |
+        def.definesAt(v, bb, i) and
+        ssaDefReachesRead(v, inp, bb, i)
+      )
+    }
+  }
+
+  private module AdjacentSsaRefs {
+    /**
+     * Holds if the `i`th node of basic block `bb` is a reference to `v`,
+     * either a read (when `k` is `Read()`) or an SSA definition (when
+     * `k` is `Def()`).
+     *
+     * Unlike `Liveness::varRef`, this includes phi nodes, phi reads, and
+     * pseudo-reads associated with uncertain writes, but excludes uncertain
+     * reads.
+     */
+    pragma[nomagic]
+    predicate ssaRef(BasicBlock bb, int i, SourceVariable v, RefKind k) {
+      variableRead(bb, i, v, true) and
+      k = Read()
+      or
+      variableWrite(bb, i, v, false) and
+      k = Read()
+      or
+      any(Definition def).definesAt(v, bb, i) and
+      k = Def()
+      or
+      synthPhiRead(bb, v) and i = -1 and k = Def()
+    }
+
+    private import RankRefs<ssaRef/4>
+
+    /**
+     * Holds if `v` is live at the end of basic block `bb`, which contains no
+     * reference to `v`, and `idom` is the immediate dominator of `bb`.
+     */
+    pragma[nomagic]
+    private predicate liveThrough(BasicBlock idom, BasicBlock bb, SourceVariable v) {
+      idom = getImmediateBasicBlockDominator(bb) and
+      liveAtExit(bb, v) and
+      not ssaRef(bb, _, v, _)
+    }
+
+    pragma[nomagic]
+    private predicate refReachesEndOfBlock(BasicBlock bbRef, int i, BasicBlock bb, SourceVariable v) {
+      maxRefRank(bb, v) = refRank(bb, i, v, _) and
+      liveAtExit(bb, v) and
+      bbRef = bb
+      or
+      exists(BasicBlock idom |
+        refReachesEndOfBlock(bbRef, i, idom, v) and
+        liveThrough(idom, bb, v)
+      )
+    }
+
+    /**
+     * Holds if `v` has adjacent references at index `i1` in basic block `bb1`
+     * and index `i2` in basic block `bb2`, that is, there is a path between
+     * the first reference to the second without any other reference to `v` in
+     * between. References include certain reads, SSA definitions, and
+     * pseudo-reads in the form of phi-reads. The first reference can be any of
+     * these kinds while the second is restricted to certain reads and
+     * uncertain writes.
+     *
+     * Note that the placement of phi-reads ensures that the first reference is
+     * uniquely determined by the second and that the first reference dominates
+     * the second.
+     */
+    predicate adjacentRefRead(BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v) {
+      bb1 = bb2 and
+      refRank(bb1, i1, v, _) + 1 = refRank(bb2, i2, v, Read())
+      or
+      refReachesEndOfBlock(bb1, i1, getImmediateBasicBlockDominator(bb2), v) and
+      1 = refRank(bb2, i2, v, Read())
+    }
+
+    /**
+     * Holds if the phi node or phi-read for `v` in basic block `bbPhi` takes
+     * input from basic block `input`, and that the reference to `v` at index
+     * `i` in basic block `bb` reaches the end of `input` without going through
+     * any other reference to `v`.
+     */
+    predicate adjacentRefPhi(
+      BasicBlock bb, int i, BasicBlock input, BasicBlock bbPhi, SourceVariable v
+    ) {
+      refReachesEndOfBlock(bb, i, input, v) and
+      input = getABasicBlockPredecessor(bbPhi) and
+      1 = refRank(bbPhi, -1, v, _)
+    }
+
+    private predicate adjacentRefs(BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v) {
+      adjacentRefRead(bb1, i1, bb2, i2, v)
+      or
+      adjacentRefPhi(bb1, i1, _, bb2, v) and i2 = -1
+    }
+
+    /**
+     * Holds if the reference to `v` at index `i1` in basic block `bb1` reaches
+     * the certain read at index `i2` in basic block `bb2` without going
+     * through any other certain read. The boolean `samevar` indicates whether
+     * the two references are to the same SSA variable.
+     *
+     * Note that since this relation skips over phi nodes and phi reads, it may
+     * be quadratic in the number of variable references for certain access
+     * patterns.
+     */
+    predicate firstUseAfterRef(
+      BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v, boolean samevar
+    ) {
+      adjacentRefs(bb1, i1, bb2, i2, v) and
+      variableRead(bb2, i2, v, _) and
+      samevar = true
+      or
+      exists(BasicBlock bb0, int i0, boolean samevar0 |
+        firstUseAfterRef(bb0, i0, bb2, i2, v, samevar0) and
+        adjacentRefs(bb1, i1, bb0, i0, v) and
+        not variableWrite(bb0, i0, v, true) and
+        if any(Definition def).definesAt(v, bb0, i0)
+        then samevar = false
+        else (
+          samevar = samevar0 and synthPhiRead(bb0, v) and i0 = -1
+        )
+      )
+    }
+  }
+
+  /**
+   * Holds if `def` reaches the certain read at index `i` in basic block `bb`
+   * without going through any other certain read. The boolean `samevar`
+   * indicates whether the read is a use of `def` or whether some number of phi
+   * nodes and/or uncertain reads occur between `def` and the read.
+   *
+   * Note that since this relation skips over phi nodes and phi reads, it may
+   * be quadratic in the number of variable references for certain access
+   * patterns.
+   */
+  predicate firstUse(Definition def, BasicBlock bb, int i, boolean samevar) {
+    exists(BasicBlock bb1, int i1, SourceVariable v |
+      def.definesAt(v, bb1, i1) and
+      AdjacentSsaRefs::firstUseAfterRef(bb1, i1, bb, i, v, samevar)
+    )
+  }
+
+  /**
+   * Holds if the certain read at index `i1` in basic block `bb1` reaches the
+   * certain read at index `i2` in basic block `bb2` without going through any
+   * other certain read. The boolean `samevar` indicates whether the two reads
+   * are of the same SSA variable.
+   *
+   * Note that since this relation skips over phi nodes and phi reads, it may
+   * be quadratic in the number of variable references for certain access
+   * patterns.
+   */
+  predicate adjacentUseUse(
+    BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v, boolean samevar
+  ) {
+    exists(boolean samevar0 |
+      variableRead(bb1, i1, v, true) and
+      not variableWrite(bb1, i1, v, true) and
+      AdjacentSsaRefs::firstUseAfterRef(bb1, i1, bb2, i2, v, samevar0) and
+      if any(Definition def).definesAt(v, bb1, i1) then samevar = false else samevar = samevar0
+    )
+  }
+
   private module SsaDefReaches {
     newtype TSsaRefKind =
       SsaActualRead() or
@@ -356,14 +647,17 @@ module Make<LocationSig Location, InputSig<Location> Input> {
      * either a read (when `k` is `SsaActualRead()`), an SSA definition (when `k`
      * is `SsaDef()`), or a phi-read (when `k` is `SsaPhiRead()`).
      *
-     * Unlike `Liveness::ref`, this includes `phi` (read) nodes.
+     * Unlike `Liveness::varRef`, this includes `phi` (read) nodes.
      */
     pragma[nomagic]
     predicate ssaRef(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) {
       variableRead(bb, i, v, _) and
       k = SsaActualRead()
       or
-      any(DefinitionExt def).definesAt(v, bb, i, k)
+      any(Definition def).definesAt(v, bb, i) and
+      k = SsaDef()
+      or
+      synthPhiRead(bb, v) and i = -1 and k = SsaPhiRead()
     }
 
     /**
@@ -485,7 +779,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
     pragma[noinline]
     predicate ssaDefReachesThroughBlock(DefinitionExt def, BasicBlock bb) {
       exists(SourceVariable v |
-        ssaDefReachesEndOfBlockExt(bb, def, v) and
+        ssaDefReachesEndOfBlockExt0(bb, def, v) and
         not defOccursInBlock(_, bb, v, _)
       )
     }
@@ -513,7 +807,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
       exists(SourceVariable v |
         varBlockReachesExt(pragma[only_bind_into](def), v, bb1, pragma[only_bind_into](bb2)) and
         phi.definesAt(v, bb2, _, _) and
-        not ref(bb2, _, v, _)
+        not varRef(bb2, _, v, _)
       )
     }
 
@@ -569,7 +863,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
     predicate varBlockReachesExitExt(DefinitionExt def, BasicBlock bb) {
       exists(BasicBlock bb2 | varBlockReachesExt(def, _, bb, bb2) |
         not defOccursInBlock(def, bb2, _, _) and
-        not ssaDefReachesEndOfBlockExt(bb2, def, _)
+        not ssaDefReachesEndOfBlockExt0(bb2, def, _)
       )
     }
 
@@ -578,7 +872,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
       exists(BasicBlock bb2, SourceVariable v |
         varBlockReachesExt(def, v, bb, bb2) and
         not defOccursInBlock(def, bb2, _, _) and
-        not ssaDefReachesEndOfBlockExt(bb2, def, _) and
+        not ssaDefReachesEndOfBlockExt0(bb2, def, _) and
         not any(PhiReadNode phi).definesAt(v, bb2, _, _)
       )
       or
@@ -613,7 +907,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
    * SSA definition of `v`.
    */
   pragma[nomagic]
-  predicate ssaDefReachesEndOfBlockExt(BasicBlock bb, DefinitionExt def, SourceVariable v) {
+  private predicate ssaDefReachesEndOfBlockExt0(BasicBlock bb, DefinitionExt def, SourceVariable v) {
     exists(int last |
       last = maxSsaRefRank(pragma[only_bind_into](bb), pragma[only_bind_into](v)) and
       ssaDefReachesRank(bb, def, last, v) and
@@ -626,32 +920,18 @@ module Make<LocationSig Location, InputSig<Location> Input> {
     // 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.
-    ssaDefReachesEndOfBlockExt(getImmediateBasicBlockDominator(bb), def, pragma[only_bind_into](v)) and
+    ssaDefReachesEndOfBlockExt0(getImmediateBasicBlockDominator(bb), def, pragma[only_bind_into](v)) and
     liveThroughExt(bb, pragma[only_bind_into](v))
   }
 
-  pragma[nomagic]
-  private predicate phiReadReachesEndOfBlock(BasicBlock pred, BasicBlock bb, SourceVariable v) {
-    exists(PhiReadNode phi |
-      ssaDefReachesEndOfBlockExt(bb, phi, v) and
-      pred = getImmediateBasicBlockDominator(phi.getBasicBlock())
-    )
-  }
+  deprecated predicate ssaDefReachesEndOfBlockExt = ssaDefReachesEndOfBlockExt0/3;
 
   /**
    * NB: If this predicate is exposed, it should be cached.
    *
    * Same as `ssaDefReachesEndOfBlockExt`, but ignores phi-reads.
    */
-  pragma[nomagic]
-  predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable v) {
-    ssaDefReachesEndOfBlockExt(bb, def, v)
-    or
-    exists(BasicBlock mid |
-      ssaDefReachesEndOfBlock(mid, def, v) and
-      phiReadReachesEndOfBlock(mid, bb, v)
-    )
-  }
+  predicate ssaDefReachesEndOfBlock = SsaDefReachesNew::ssaDefReachesEndOfBlock/3;
 
   /**
    * NB: If this predicate is exposed, it should be cached.
@@ -677,7 +957,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
     exists(SourceVariable v, BasicBlock bbDef |
       phi.definesAt(v, bbDef, _, _) and
       getABasicBlockPredecessor(bbDef) = bb and
-      ssaDefReachesEndOfBlockExt(bb, inp, v)
+      ssaDefReachesEndOfBlockExt0(bb, inp, v)
     |
       phi instanceof PhiNode or
       phi instanceof PhiReadNode
@@ -695,7 +975,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
     ssaDefReachesReadWithinBlock(v, def, bb, i)
     or
     ssaRef(bb, i, v, SsaActualRead()) and
-    ssaDefReachesEndOfBlockExt(getABasicBlockPredecessor(bb), def, v) and
+    ssaDefReachesEndOfBlockExt0(getABasicBlockPredecessor(bb), def, v) and
     not ssaDefReachesReadWithinBlock(v, _, bb, i)
   }
 
@@ -704,13 +984,9 @@ module Make<LocationSig Location, InputSig<Location> Input> {
    *
    * Same as `ssaDefReachesReadExt`, but ignores phi-reads.
    */
-  pragma[nomagic]
   predicate ssaDefReachesRead(SourceVariable v, Definition def, BasicBlock bb, int i) {
-    ssaDefReachesReadWithinBlock(v, def, bb, i)
-    or
-    ssaRef(bb, i, v, SsaActualRead()) and
-    ssaDefReachesEndOfBlock(getABasicBlockPredecessor(bb), def, v) and
-    not exists(Definition other | ssaDefReachesReadWithinBlock(v, other, bb, i))
+    SsaDefReachesNew::ssaDefReachesRead(v, def, bb, i) and
+    variableRead(bb, i, v, _)
   }
 
   /**
@@ -844,10 +1120,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
    * `def`. Since `def` is uncertain, the value from the preceding definition might
    * still be valid.
    */
-  pragma[nomagic]
-  predicate uncertainWriteDefinitionInput(UncertainWriteDefinition def, Definition inp) {
-    lastRefRedef(inp, _, _, def)
-  }
+  predicate uncertainWriteDefinitionInput = SsaDefReachesNew::uncertainWriteDefinitionInput/2;
 
   /** Holds if `bb` is a control-flow exit point. */
   private predicate exitBlock(BasicBlock bb) { not exists(getABasicBlockSuccessor(bb)) }