diff --git a/CHANGELOG.md b/CHANGELOG.md
index f0506d20f0d..b4278e9f51c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -15,6 +15,8 @@ full changeset diff at the end of each section.
 Current Trunk
 -------------
 
+- Add a new `--constraint-analysis` pass which propagates logical facts along
+  branches. (#9010)
 - Replace the `BINARYEN_ROOT` environment variable (used by developers who are
   doing out-of-tree builds of binaryen) with `BINARYEN_BIN` (#9023)
 
diff --git a/scripts/fuzz_opt.py b/scripts/fuzz_opt.py
index 267f268c523..77652a53971 100755
--- a/scripts/fuzz_opt.py
+++ b/scripts/fuzz_opt.py
@@ -2691,6 +2691,7 @@ def write_commands(commands, filename):
     ("--code-pushing",),
     ("--code-folding",),
     ("--const-hoisting",),
+    ("--constraint-analysis",),
     ("--dae",),
     ("--dae-optimizing",),
     ("--dae2",),
diff --git a/src/passes/ConstraintAnalysis.cpp b/src/passes/ConstraintAnalysis.cpp
index a914cf37feb..324e2ef0312 100644
--- a/src/passes/ConstraintAnalysis.cpp
+++ b/src/passes/ConstraintAnalysis.cpp
@@ -517,14 +517,12 @@ struct ConstraintAnalysis
   // incremented and loop again, leading to [0, 2] and so forth, only stopping
   // when it reaches the loop bound, which may be very high. We don't want to
   // spend significant time on such constant operations, as other passes will
-  // propagate them anyhow, so we verify that we don't apply such x = y + 1
-  // operations too many times.
-#ifndef NDEBUG
-  static const Index MaxBinaryActions = 5;
+  // propagate them anyhow, so we stop before applying such x = y + 1
+  // operations a ridiculous number of times, by widening to a worst case.
+  static const Index MaxBinaryActions = 20;
 
   // How many times we processed each Binary action.
   std::unordered_map<Binary*, Index> binaryActionCounts;
-#endif
 
   // Given an expression, apply it to the constraints. For example, a local.set
   // sets the value for that local.
@@ -536,12 +534,13 @@ struct ConstraintAnalysis
         return;
       }
 
-#ifndef NDEBUG
       // See above on binary action counting limits.
       if (auto* binary = set->value->dynCast<Binary>()) {
-        assert(binaryActionCounts[binary]++ <= MaxBinaryActions);
+        if (binaryActionCounts[binary]++ >= MaxBinaryActions) {
+          constraints.setProvesNothing(set->index);
+          return;
+        }
       }
-#endif
 
       // Look at the fallthrough. It is valid to do so, because our constraints
       // only track two things, constants and locals. For a constant, it does
diff --git a/src/passes/pass.cpp b/src/passes/pass.cpp
index 34bc0c7dd40..f178772290a 100644
--- a/src/passes/pass.cpp
+++ b/src/passes/pass.cpp
@@ -740,7 +740,7 @@ void PassRunner::addDefaultFunctionOptimizationPasses() {
     "remove-unused-brs"); // coalesce-locals opens opportunities
   addIfNoDWARFIssues(
     "remove-unused-names");           // remove-unused-brs opens opportunities
-  addIfNoDWARFIssues("merge-blocks"); // clean up remove-unused-brs new blocks
+  addIfNoDWARFIssues("merge-blocks"); // clean up new blocks from last passes
   // late propagation
   if (options.optimizeLevel >= 3 || options.shrinkLevel >= 2) {
     addIfNoDWARFIssues("precompute-propagate");
diff --git a/test/lit/passes/constraint-analysis-loops.wast b/test/lit/passes/constraint-analysis-loops.wast
index 9e503b01e95..a865c5b8651 100644
--- a/test/lit/passes/constraint-analysis-loops.wast
+++ b/test/lit/passes/constraint-analysis-loops.wast
@@ -64,6 +64,51 @@
     )
   )
 
+  ;; CHECK:      (func $infinite-loop-with-branch (type $0)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (loop $loop
+  ;; CHECK-NEXT:   (if
+  ;; CHECK-NEXT:    (i32.gt_s
+  ;; CHECK-NEXT:     (local.get $x)
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (then
+  ;; CHECK-NEXT:     (nop)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (local.set $x
+  ;; CHECK-NEXT:    (i32.add
+  ;; CHECK-NEXT:     (local.get $x)
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (br $loop)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  (func $infinite-loop-with-branch
+    (local $x i32)
+    ;; An infinite loop that *looks* like it might not be infinite. We have a
+    ;; branch with a loop-like condition, but it is just a nop.
+    (loop $loop
+      (if
+        (i32.gt_s
+          (local.get $x)
+          (i32.const 0)
+       )
+       (then
+         (nop)
+       )
+      )
+      (local.set $x
+        (i32.add
+          (local.get $x)
+          (i32.const 1)
+        )
+      )
+      (br $loop)
+    )
+  )
+
   ;; CHECK:      (func $bound (type $0)
   ;; CHECK-NEXT:  (local $x i32)
   ;; CHECK-NEXT:  (loop $loop
@@ -665,7 +710,7 @@
             (br $out)
           )
         )
-        ;; x > 0 && x <= 100 here (but we need loops mode to get both).
+        ;; x > 0 && x <= 100 here.
         (drop
           (i32.gt_u
             (local.get $x)