From 843feed11cf04092b6d3f6a68bc066f0126676f8 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 9 Jul 2026 10:36:11 -0700
Subject: [PATCH 01/12] start

---
 src/ir/constraint.cpp                    | 10 ++++++-
 test/lit/passes/constraint-analysis.wast | 38 ++++++++++++++++++++++++
 2 files changed, 47 insertions(+), 1 deletion(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 5e8e3a0129c..fec7ada8e27 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -234,7 +234,15 @@ std::optional<LocalConstraint> LocalConstraint::parse(Expression* curr) {
 
   if (auto* binary = curr->dynCast<Binary>()) {
     // The operation must be one we recognize.
-    for (auto op : {Abstract::Eq, Abstract::Ne}) {
+    for (auto op : {Abstract::Eq, Abstract::Ne, Abstract::LtS,
+Abstract::LtU,
+Abstract::LeS,
+Abstract::LeU,
+Abstract::GtS,
+Abstract::GtU,
+Abstract::GeS,
+Abstract::GeU
+}) {
       if (Abstract::getBinary(binary->type, op) == binary->op) {
         return parseBinaryArguments(op, binary->left, binary->right);
       }
diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index ce5d59afa7b..59c0f7d91ff 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -1652,6 +1652,44 @@
     )
   )
 
+  (func $inequalities-lt_u (param $param i32)
+    ;; The simple case where an inequality is seen again, in exact form.
+    (if
+      (i32.lt_u
+        (local.get $x)
+        (i32.const 10)
+      )
+      (then
+        (drop
+          (i32.lt_u
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+        (drop
+          (i32.ge_u
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+      )
+      (else
+        (drop
+          (i32.lt_u
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+        (drop
+          (i32.ge_u
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+      )
+    )
+  )
+
   ;; CHECK:      (func $local-changes (type $2) (param $x i32) (param $y i32) (param $z i32)
   ;; CHECK-NEXT:  (local.set $x
   ;; CHECK-NEXT:   (local.get $y)

From c5cbb3666486618a03ebef59ba378ae7769df29c Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 9 Jul 2026 10:36:22 -0700
Subject: [PATCH 02/12] form

---
 src/ir/constraint.cpp | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index fec7ada8e27..95d55d68997 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -234,15 +234,16 @@ std::optional<LocalConstraint> LocalConstraint::parse(Expression* curr) {
 
   if (auto* binary = curr->dynCast<Binary>()) {
     // The operation must be one we recognize.
-    for (auto op : {Abstract::Eq, Abstract::Ne, Abstract::LtS,
-Abstract::LtU,
-Abstract::LeS,
-Abstract::LeU,
-Abstract::GtS,
-Abstract::GtU,
-Abstract::GeS,
-Abstract::GeU
-}) {
+    for (auto op : {Abstract::Eq,
+                    Abstract::Ne,
+                    Abstract::LtS,
+                    Abstract::LtU,
+                    Abstract::LeS,
+                    Abstract::LeU,
+                    Abstract::GtS,
+                    Abstract::GtU,
+                    Abstract::GeS,
+                    Abstract::GeU}) {
       if (Abstract::getBinary(binary->type, op) == binary->op) {
         return parseBinaryArguments(op, binary->left, binary->right);
       }

From 9432fe328a3889cfc0407b7b509175266be552fc Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 9 Jul 2026 10:37:15 -0700
Subject: [PATCH 03/12] test

---
 test/lit/passes/constraint-analysis.wast | 42 +++++++++++++++++++++++-
 1 file changed, 41 insertions(+), 1 deletion(-)

diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index 59c0f7d91ff..76ab9d65217 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -1652,7 +1652,45 @@
     )
   )
 
-  (func $inequalities-lt_u (param $param i32)
+  ;; CHECK:      (func $inequalities-lt_u (type $0) (param $x i32)
+  ;; CHECK-NEXT:  (if
+  ;; CHECK-NEXT:   (i32.lt_u
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (i32.const 10)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (then
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (else
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $inequalities-lt_u (type $0) (param $x i32)
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.lt_u
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 10)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.ge_u
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 10)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $inequalities-lt_u (param $x i32)
     ;; The simple case where an inequality is seen again, in exact form.
     (if
       (i32.lt_u
@@ -1660,6 +1698,7 @@
         (i32.const 10)
       )
       (then
+        ;; We can infer 1, 0 here.
         (drop
           (i32.lt_u
             (local.get $x)
@@ -1674,6 +1713,7 @@
         )
       )
       (else
+        ;; We can infer 0, 1 here.
         (drop
           (i32.lt_u
             (local.get $x)

From b248ab5ea2007939e92446429eb407a7a3034fe2 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 9 Jul 2026 10:42:03 -0700
Subject: [PATCH 04/12] test

---
 test/lit/passes/constraint-analysis.wast | 525 +++++++++++++++++++++++
 1 file changed, 525 insertions(+)

diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index 76ab9d65217..b0ed5dcc6c7 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -1730,6 +1730,531 @@
     )
   )
 
+  ;; CHECK:      (func $inequalities-lt_s (type $0) (param $x i32)
+  ;; CHECK-NEXT:  (if
+  ;; CHECK-NEXT:   (i32.lt_s
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (i32.const 10)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (then
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (else
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $inequalities-lt_s (type $0) (param $x i32)
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.lt_s
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 10)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.ge_s
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 10)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $inequalities-lt_s (param $x i32)
+    (if
+      (i32.lt_s
+        (local.get $x)
+        (i32.const 10)
+      )
+      (then
+        (drop
+          (i32.lt_s
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+        (drop
+          (i32.ge_s
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+      )
+      (else
+        (drop
+          (i32.lt_s
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+        (drop
+          (i32.ge_s
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+      )
+    )
+  )
+
+  ;; CHECK:      (func $inequalities-le_u (type $0) (param $x i32)
+  ;; CHECK-NEXT:  (if
+  ;; CHECK-NEXT:   (i32.le_u
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (i32.const 10)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (then
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (else
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $inequalities-le_u (type $0) (param $x i32)
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.le_u
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 10)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.gt_u
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 10)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $inequalities-le_u (param $x i32)
+    (if
+      (i32.le_u
+        (local.get $x)
+        (i32.const 10)
+      )
+      (then
+        (drop
+          (i32.le_u
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+        (drop
+          (i32.gt_u
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+      )
+      (else
+        (drop
+          (i32.le_u
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+        (drop
+          (i32.gt_u
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+      )
+    )
+  )
+
+  ;; CHECK:      (func $inequalities-le_s (type $0) (param $x i32)
+  ;; CHECK-NEXT:  (if
+  ;; CHECK-NEXT:   (i32.le_s
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (i32.const 10)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (then
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (else
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $inequalities-le_s (type $0) (param $x i32)
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.le_s
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 10)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.gt_s
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 10)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $inequalities-le_s (param $x i32)
+    (if
+      (i32.le_s
+        (local.get $x)
+        (i32.const 10)
+      )
+      (then
+        (drop
+          (i32.le_s
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+        (drop
+          (i32.gt_s
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+      )
+      (else
+        (drop
+          (i32.le_s
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+        (drop
+          (i32.gt_s
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+      )
+    )
+  )
+
+  ;; CHECK:      (func $inequalities-gt_u (type $0) (param $x i32)
+  ;; CHECK-NEXT:  (if
+  ;; CHECK-NEXT:   (i32.gt_u
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (i32.const 10)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (then
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (else
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $inequalities-gt_u (type $0) (param $x i32)
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.gt_u
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 10)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.le_u
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 10)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $inequalities-gt_u (param $x i32)
+    (if
+      (i32.gt_u
+        (local.get $x)
+        (i32.const 10)
+      )
+      (then
+        (drop
+          (i32.gt_u
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+        (drop
+          (i32.le_u
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+      )
+      (else
+        (drop
+          (i32.gt_u
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+        (drop
+          (i32.le_u
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+      )
+    )
+  )
+
+  ;; CHECK:      (func $inequalities-gt_s (type $0) (param $x i32)
+  ;; CHECK-NEXT:  (if
+  ;; CHECK-NEXT:   (i32.gt_s
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (i32.const 10)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (then
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (else
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $inequalities-gt_s (type $0) (param $x i32)
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.gt_s
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 10)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.le_s
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 10)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $inequalities-gt_s (param $x i32)
+    (if
+      (i32.gt_s
+        (local.get $x)
+        (i32.const 10)
+      )
+      (then
+        (drop
+          (i32.gt_s
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+        (drop
+          (i32.le_s
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+      )
+      (else
+        (drop
+          (i32.gt_s
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+        (drop
+          (i32.le_s
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+      )
+    )
+  )
+
+  ;; CHECK:      (func $inequalities-ge_u (type $0) (param $x i32)
+  ;; CHECK-NEXT:  (if
+  ;; CHECK-NEXT:   (i32.ge_u
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (i32.const 10)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (then
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (else
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $inequalities-ge_u (type $0) (param $x i32)
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.ge_u
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 10)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.lt_u
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 10)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $inequalities-ge_u (param $x i32)
+    (if
+      (i32.ge_u
+        (local.get $x)
+        (i32.const 10)
+      )
+      (then
+        (drop
+          (i32.ge_u
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+        (drop
+          (i32.lt_u
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+      )
+      (else
+        (drop
+          (i32.ge_u
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+        (drop
+          (i32.lt_u
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+      )
+    )
+  )
+
+  ;; CHECK:      (func $inequalities-ge_s (type $0) (param $x i32)
+  ;; CHECK-NEXT:  (if
+  ;; CHECK-NEXT:   (i32.ge_s
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (i32.const 10)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (then
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (else
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $inequalities-ge_s (type $0) (param $x i32)
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.ge_s
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 10)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.lt_s
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 10)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $inequalities-ge_s (param $x i32)
+    (if
+      (i32.ge_s
+        (local.get $x)
+        (i32.const 10)
+      )
+      (then
+        (drop
+          (i32.ge_s
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+        (drop
+          (i32.lt_s
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+      )
+      (else
+        (drop
+          (i32.ge_s
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+        (drop
+          (i32.lt_s
+            (local.get $x)
+            (i32.const 10)
+          )
+        )
+      )
+    )
+  )
+
   ;; CHECK:      (func $local-changes (type $2) (param $x i32) (param $y i32) (param $z i32)
   ;; CHECK-NEXT:  (local.set $x
   ;; CHECK-NEXT:   (local.get $y)

From 047a97c6b9f66372903684b1df4418f3d0e4cd11 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 9 Jul 2026 11:26:33 -0700
Subject: [PATCH 05/12] test

---
 test/lit/passes/constraint-analysis.wast | 68 ++++++++++++++++++++++++
 1 file changed, 68 insertions(+)

diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index b0ed5dcc6c7..a920e76f95d 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -9,6 +9,8 @@
 ;; RUN: wasm-opt %s --optimize-instructions --constraint-analysis -all -S -o - | filecheck %s --check-prefix=OPTIN
 
 (module
+  (type $array (array (mut i32)))
+
   ;; CHECK:      (func $simple (type $1)
   ;; CHECK-NEXT:  (local $x i32)
   ;; CHECK-NEXT:  (local.set $x
@@ -2255,6 +2257,72 @@
     )
   )
 
+
+  (func $array-sum (param (ref $array)) (result i32)
+    ;; Somewhat-realistic code that sums up an array, using a software/userspace
+    ;; bounds check that can be removed.
+    (local $index i32)
+    (local $total i32)
+    (local $len i32)
+    (local $curr i32)
+    ;; Loop only if len > 0.
+    (if
+      (i32.gt_s
+        (local.tee $len
+          (array.len
+            (local.get $param)
+          )
+        )
+        (i32.const 0)
+      )
+      (then
+        (loop $label
+          ;; Increment for the next iteration, storing the current index in curr.
+          (local.set $index
+            (i32.add
+             (local.tee $curr
+               (local.get $index)
+              )
+              (i32.const 1)
+            )
+          )
+          ;; Software bounds check: if curr >= len, then the current index is invalid
+          ;; to read from the array.
+          ;;
+          ;; At the top of the loop, index == 0 or index < len. Those constraints
+          ;; were copied for curr. But we need len > 0 to make sense of it..?
+          (if
+            (i32.ge_s
+              (local.get $curr)
+              (local.get $len)
+            )
+            (then
+              (unreachable)
+            )
+          )
+          ;; Read the array and add to the total.
+          (local.set $total
+            (i32.add
+              (array.get $array
+                (local.get $param)
+                (local.get $curr)
+              )
+              (local.get $total)
+            )
+          )
+          ;; Keep looping if we did not reach the end of the array.
+          (br_if $label
+            (i32.lt_s
+              (local.get $index)
+              (local.get $len)
+            )
+          )
+        )
+      )
+    )
+    (local.get $total)
+  )
+
   ;; CHECK:      (func $local-changes (type $2) (param $x i32) (param $y i32) (param $z i32)
   ;; CHECK-NEXT:  (local.set $x
   ;; CHECK-NEXT:   (local.get $y)

From 7127778da0d0b4a52e02774a5f1d723496f38d54 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 9 Jul 2026 11:29:17 -0700
Subject: [PATCH 06/12] test

---
 test/lit/passes/constraint-analysis.wast | 132 ++++++++++++++++++++---
 1 file changed, 117 insertions(+), 15 deletions(-)

diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index a920e76f95d..14779d2075c 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -9,6 +9,8 @@
 ;; RUN: wasm-opt %s --optimize-instructions --constraint-analysis -all -S -o - | filecheck %s --check-prefix=OPTIN
 
 (module
+  ;; CHECK:      (type $array (array (mut i32)))
+  ;; OPTIN:      (type $array (array (mut i32)))
   (type $array (array (mut i32)))
 
   ;; CHECK:      (func $simple (type $1)
@@ -1010,7 +1012,7 @@
     )
   )
 
-  ;; CHECK:      (func $conditional-binary-nesting (type $4) (param $x i32) (param $y i32)
+  ;; CHECK:      (func $conditional-binary-nesting (type $5) (param $x i32) (param $y i32)
   ;; CHECK-NEXT:  (if
   ;; CHECK-NEXT:   (i32.eq
   ;; CHECK-NEXT:    (local.get $x)
@@ -1040,7 +1042,7 @@
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $conditional-binary-nesting (type $4) (param $x i32) (param $y i32)
+  ;; OPTIN:      (func $conditional-binary-nesting (type $5) (param $x i32) (param $y i32)
   ;; OPTIN-NEXT:  (if
   ;; OPTIN-NEXT:   (i32.eq
   ;; OPTIN-NEXT:    (local.get $x)
@@ -1512,7 +1514,7 @@
     )
   )
 
-  ;; CHECK:      (func $br_on_null (type $3) (param $param anyref)
+  ;; CHECK:      (func $br_on_null (type $4) (param $param anyref)
   ;; CHECK-NEXT:  (block $block
   ;; CHECK-NEXT:   (drop
   ;; CHECK-NEXT:    (ref.is_null
@@ -1533,7 +1535,7 @@
   ;; CHECK-NEXT:   (i32.const 1)
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $br_on_null (type $3) (param $param anyref)
+  ;; OPTIN:      (func $br_on_null (type $4) (param $param anyref)
   ;; OPTIN-NEXT:  (block $block
   ;; OPTIN-NEXT:   (drop
   ;; OPTIN-NEXT:    (ref.is_null
@@ -1583,7 +1585,7 @@
     )
   )
 
-  ;; CHECK:      (func $br_on_non_null (type $3) (param $param anyref)
+  ;; CHECK:      (func $br_on_non_null (type $4) (param $param anyref)
   ;; CHECK-NEXT:  (drop
   ;; CHECK-NEXT:   (block $block (result (ref any))
   ;; CHECK-NEXT:    (drop
@@ -1604,7 +1606,7 @@
   ;; CHECK-NEXT:   (i32.const 0)
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $br_on_non_null (type $3) (param $param anyref)
+  ;; OPTIN:      (func $br_on_non_null (type $4) (param $param anyref)
   ;; OPTIN-NEXT:  (drop
   ;; OPTIN-NEXT:   (block $block (result (ref any))
   ;; OPTIN-NEXT:    (drop
@@ -2258,7 +2260,110 @@
   )
 
 
-  (func $array-sum (param (ref $array)) (result i32)
+  ;; CHECK:      (func $array-sum (type $6) (param $param (ref $array)) (result i32)
+  ;; CHECK-NEXT:  (local $index i32)
+  ;; CHECK-NEXT:  (local $total i32)
+  ;; CHECK-NEXT:  (local $len i32)
+  ;; CHECK-NEXT:  (local $curr i32)
+  ;; CHECK-NEXT:  (if
+  ;; CHECK-NEXT:   (i32.gt_u
+  ;; CHECK-NEXT:    (local.tee $len
+  ;; CHECK-NEXT:     (array.len
+  ;; CHECK-NEXT:      (local.get $param)
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (i32.const 0)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (then
+  ;; CHECK-NEXT:    (loop $label
+  ;; CHECK-NEXT:     (local.set $index
+  ;; CHECK-NEXT:      (i32.add
+  ;; CHECK-NEXT:       (local.tee $curr
+  ;; CHECK-NEXT:        (local.get $index)
+  ;; CHECK-NEXT:       )
+  ;; CHECK-NEXT:       (i32.const 1)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:     (if
+  ;; CHECK-NEXT:      (i32.ge_u
+  ;; CHECK-NEXT:       (local.get $curr)
+  ;; CHECK-NEXT:       (local.get $len)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:      (then
+  ;; CHECK-NEXT:       (unreachable)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:     (local.set $total
+  ;; CHECK-NEXT:      (i32.add
+  ;; CHECK-NEXT:       (array.get $array
+  ;; CHECK-NEXT:        (local.get $param)
+  ;; CHECK-NEXT:        (local.get $curr)
+  ;; CHECK-NEXT:       )
+  ;; CHECK-NEXT:       (local.get $total)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:     (br_if $label
+  ;; CHECK-NEXT:      (i32.lt_u
+  ;; CHECK-NEXT:       (local.get $index)
+  ;; CHECK-NEXT:       (local.get $len)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (local.get $total)
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $array-sum (type $6) (param $param (ref $array)) (result i32)
+  ;; OPTIN-NEXT:  (local $index i32)
+  ;; OPTIN-NEXT:  (local $total i32)
+  ;; OPTIN-NEXT:  (local $len i32)
+  ;; OPTIN-NEXT:  (local $curr i32)
+  ;; OPTIN-NEXT:  (if
+  ;; OPTIN-NEXT:   (local.tee $len
+  ;; OPTIN-NEXT:    (array.len
+  ;; OPTIN-NEXT:     (local.get $param)
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (then
+  ;; OPTIN-NEXT:    (loop $label
+  ;; OPTIN-NEXT:     (local.set $index
+  ;; OPTIN-NEXT:      (i32.add
+  ;; OPTIN-NEXT:       (local.tee $curr
+  ;; OPTIN-NEXT:        (local.get $index)
+  ;; OPTIN-NEXT:       )
+  ;; OPTIN-NEXT:       (i32.const 1)
+  ;; OPTIN-NEXT:      )
+  ;; OPTIN-NEXT:     )
+  ;; OPTIN-NEXT:     (if
+  ;; OPTIN-NEXT:      (i32.le_u
+  ;; OPTIN-NEXT:       (local.get $len)
+  ;; OPTIN-NEXT:       (local.get $curr)
+  ;; OPTIN-NEXT:      )
+  ;; OPTIN-NEXT:      (then
+  ;; OPTIN-NEXT:       (unreachable)
+  ;; OPTIN-NEXT:      )
+  ;; OPTIN-NEXT:     )
+  ;; OPTIN-NEXT:     (local.set $total
+  ;; OPTIN-NEXT:      (i32.add
+  ;; OPTIN-NEXT:       (local.get $total)
+  ;; OPTIN-NEXT:       (array.get $array
+  ;; OPTIN-NEXT:        (local.get $param)
+  ;; OPTIN-NEXT:        (local.get $curr)
+  ;; OPTIN-NEXT:       )
+  ;; OPTIN-NEXT:      )
+  ;; OPTIN-NEXT:     )
+  ;; OPTIN-NEXT:     (br_if $label
+  ;; OPTIN-NEXT:      (i32.lt_u
+  ;; OPTIN-NEXT:       (local.get $index)
+  ;; OPTIN-NEXT:       (local.get $len)
+  ;; OPTIN-NEXT:      )
+  ;; OPTIN-NEXT:     )
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (local.get $total)
+  ;; OPTIN-NEXT: )
+  (func $array-sum (param $param (ref $array)) (result i32)
     ;; Somewhat-realistic code that sums up an array, using a software/userspace
     ;; bounds check that can be removed.
     (local $index i32)
@@ -2267,7 +2372,7 @@
     (local $curr i32)
     ;; Loop only if len > 0.
     (if
-      (i32.gt_s
+      (i32.gt_u
         (local.tee $len
           (array.len
             (local.get $param)
@@ -2288,11 +2393,8 @@
           )
           ;; Software bounds check: if curr >= len, then the current index is invalid
           ;; to read from the array.
-          ;;
-          ;; At the top of the loop, index == 0 or index < len. Those constraints
-          ;; were copied for curr. But we need len > 0 to make sense of it..?
           (if
-            (i32.ge_s
+            (i32.ge_u
               (local.get $curr)
               (local.get $len)
             )
@@ -2312,7 +2414,7 @@
           )
           ;; Keep looping if we did not reach the end of the array.
           (br_if $label
-            (i32.lt_s
+            (i32.lt_u
               (local.get $index)
               (local.get $len)
             )
@@ -2696,7 +2798,7 @@
     )
   )
 
-  ;; CHECK:      (func $local-changes-if (type $5) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
+  ;; CHECK:      (func $local-changes-if (type $7) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
   ;; CHECK-NEXT:  (if
   ;; CHECK-NEXT:   (i32.eq
   ;; CHECK-NEXT:    (local.get $x)
@@ -2753,7 +2855,7 @@
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $local-changes-if (type $5) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
+  ;; OPTIN:      (func $local-changes-if (type $7) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
   ;; OPTIN-NEXT:  (if
   ;; OPTIN-NEXT:   (i32.eq
   ;; OPTIN-NEXT:    (local.get $x)

From 05af48dda9c117728b6f8994383011cf0bab488a Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 9 Jul 2026 11:39:18 -0700
Subject: [PATCH 07/12] test

---
 src/ir/CMakeLists.txt |  1 +
 src/ir/abstract.cpp   | 61 +++++++++++++++++++++++++++++++++++++++++++
 src/ir/abstract.h     |  2 ++
 src/ir/constraint.cpp |  6 ++++-
 4 files changed, 69 insertions(+), 1 deletion(-)
 create mode 100644 src/ir/abstract.cpp

diff --git a/src/ir/CMakeLists.txt b/src/ir/CMakeLists.txt
index 5521529cd91..4bedfc886ec 100644
--- a/src/ir/CMakeLists.txt
+++ b/src/ir/CMakeLists.txt
@@ -1,5 +1,6 @@
 FILE(GLOB ir_HEADERS *.h)
 set(ir_SOURCES
+  abstract.cpp
   ExpressionAnalyzer.cpp
   ExpressionManipulator.cpp
   constraint.cpp
diff --git a/src/ir/abstract.cpp b/src/ir/abstract.cpp
new file mode 100644
index 00000000000..c1f368c7a3f
--- /dev/null
+++ b/src/ir/abstract.cpp
@@ -0,0 +1,61 @@
+/*
+ * Copyright 2026 WebAssembly Community Group participants
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#include "ir/abstract.h"
+#include "wasm.h"
+
+namespace wasm::Abstract {
+
+std::ostream& operator<<(std::ostream& o, Op op) {
+  #define HANDLE(x) case x: return o << #x;
+  switch (op) {
+    HANDLE(Abs)
+    HANDLE(Neg)
+    HANDLE(Popcnt)
+    HANDLE(Add)
+    HANDLE(Sub)
+    HANDLE(Mul)
+    HANDLE(DivU)
+    HANDLE(DivS)
+    HANDLE(RemU)
+    HANDLE(RemS)
+    HANDLE(Shl)
+    HANDLE(ShrU)
+    HANDLE(ShrS)
+    HANDLE(RotL)
+    HANDLE(RotR)
+    HANDLE(And)
+    HANDLE(Or)
+    HANDLE(Xor)
+    HANDLE(CopySign)
+    HANDLE(EqZ)
+    HANDLE(Eq)
+    HANDLE(Ne)
+    HANDLE(LtS)
+    HANDLE(LtU)
+    HANDLE(LeS)
+    HANDLE(LeU)
+    HANDLE(GtS)
+    HANDLE(GtU)
+    HANDLE(GeS)
+    HANDLE(GeU)
+    default:
+      WASM_UNREACHABLE("bad abstract op");
+  }
+}
+
+} // namespace wasm::Abstract
+
diff --git a/src/ir/abstract.h b/src/ir/abstract.h
index 44124381876..33a297efb5f 100644
--- a/src/ir/abstract.h
+++ b/src/ir/abstract.h
@@ -349,6 +349,8 @@ inline bool isRelationalAntisymmetric(Op op) {
   }
 }
 
+std::ostream& operator<<(std::ostream& o, Op op);
+
 } // namespace wasm::Abstract
 
 #endif // wasm_ir_abstract_h
diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 95d55d68997..560f8ae908c 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -166,6 +166,8 @@ void AndedConstraintSet::approximateOr(const AndedConstraintSet& other) {
     return;
   }
 
+std::cout << "OR " << *this << " with " << other << '\n';
+
   // If this is already implied by current constraints, then it is redundant.
   // E.g. if we are { x = 10 } and other is { x >= 0 } then all we need is
   // { x >= 0 } as the result of the OR.
@@ -182,6 +184,7 @@ void AndedConstraintSet::approximateOr(const AndedConstraintSet& other) {
   // Otherwise, we don't know how to nicely OR these things, and expand to the
   // trivial set of no constraints.
   clear();
+std::cout << "  sadd OR\n";
 }
 
 std::optional<LocalConstraint> LocalConstraint::parse(Expression* curr) {
@@ -314,6 +317,7 @@ void BasicBlockConstraintMap::approximateOr(
   // We only need to loop on our locals, as any local that is missing in us is
   // one that would end up proving nothing (and get removed).
   for (auto& [local, constraints] : map) {
+std::cout << "or local " << local << '\n';
     constraints.approximateOr(other.get(local));
   }
 
@@ -400,7 +404,7 @@ void BasicBlockConstraintMap::eraseStaleRefs(Index index) {
 }
 
 std::ostream& operator<<(std::ostream& o, const Constraint& c) {
-  o << "Constraint{" << int(c.op) << ", ";
+  o << "Constraint{" << c.op << ", ";
   if (auto* cc = std::get_if<Literal>(&c.term)) {
     o << *cc;
   } else if (auto* i = std::get_if<Index>(&c.term)) {

From f99c0ed19e46e61fdfcde1ad18b0aa290d24411e Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 9 Jul 2026 15:18:42 -0700
Subject: [PATCH 08/12] undo

---
 test/lit/passes/constraint-analysis.wast | 170 -----------------------
 1 file changed, 170 deletions(-)

diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index 0314f13d72d..0162161d3be 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -9,10 +9,6 @@
 ;; RUN: wasm-opt %s --optimize-instructions --constraint-analysis -all -S -o - | filecheck %s --check-prefix=OPTIN
 
 (module
-  ;; CHECK:      (type $array (array (mut i32)))
-  ;; OPTIN:      (type $array (array (mut i32)))
-  (type $array (array (mut i32)))
-
   ;; CHECK:      (func $simple (type $1)
   ;; CHECK-NEXT:  (local $x i32)
   ;; CHECK-NEXT:  (local.set $x
@@ -2259,172 +2255,6 @@
     )
   )
 
-
-  ;; CHECK:      (func $array-sum (type $6) (param $param (ref $array)) (result i32)
-  ;; CHECK-NEXT:  (local $index i32)
-  ;; CHECK-NEXT:  (local $total i32)
-  ;; CHECK-NEXT:  (local $len i32)
-  ;; CHECK-NEXT:  (local $curr i32)
-  ;; CHECK-NEXT:  (if
-  ;; CHECK-NEXT:   (i32.gt_u
-  ;; CHECK-NEXT:    (local.tee $len
-  ;; CHECK-NEXT:     (array.len
-  ;; CHECK-NEXT:      (local.get $param)
-  ;; CHECK-NEXT:     )
-  ;; CHECK-NEXT:    )
-  ;; CHECK-NEXT:    (i32.const 0)
-  ;; CHECK-NEXT:   )
-  ;; CHECK-NEXT:   (then
-  ;; CHECK-NEXT:    (loop $label
-  ;; CHECK-NEXT:     (local.set $index
-  ;; CHECK-NEXT:      (i32.add
-  ;; CHECK-NEXT:       (local.tee $curr
-  ;; CHECK-NEXT:        (local.get $index)
-  ;; CHECK-NEXT:       )
-  ;; CHECK-NEXT:       (i32.const 1)
-  ;; CHECK-NEXT:      )
-  ;; CHECK-NEXT:     )
-  ;; CHECK-NEXT:     (if
-  ;; CHECK-NEXT:      (i32.ge_u
-  ;; CHECK-NEXT:       (local.get $curr)
-  ;; CHECK-NEXT:       (local.get $len)
-  ;; CHECK-NEXT:      )
-  ;; CHECK-NEXT:      (then
-  ;; CHECK-NEXT:       (unreachable)
-  ;; CHECK-NEXT:      )
-  ;; CHECK-NEXT:     )
-  ;; CHECK-NEXT:     (local.set $total
-  ;; CHECK-NEXT:      (i32.add
-  ;; CHECK-NEXT:       (array.get $array
-  ;; CHECK-NEXT:        (local.get $param)
-  ;; CHECK-NEXT:        (local.get $curr)
-  ;; CHECK-NEXT:       )
-  ;; CHECK-NEXT:       (local.get $total)
-  ;; CHECK-NEXT:      )
-  ;; CHECK-NEXT:     )
-  ;; CHECK-NEXT:     (br_if $label
-  ;; CHECK-NEXT:      (i32.lt_u
-  ;; CHECK-NEXT:       (local.get $index)
-  ;; CHECK-NEXT:       (local.get $len)
-  ;; CHECK-NEXT:      )
-  ;; CHECK-NEXT:     )
-  ;; CHECK-NEXT:    )
-  ;; CHECK-NEXT:   )
-  ;; CHECK-NEXT:  )
-  ;; CHECK-NEXT:  (local.get $total)
-  ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $array-sum (type $6) (param $param (ref $array)) (result i32)
-  ;; OPTIN-NEXT:  (local $index i32)
-  ;; OPTIN-NEXT:  (local $total i32)
-  ;; OPTIN-NEXT:  (local $len i32)
-  ;; OPTIN-NEXT:  (local $curr i32)
-  ;; OPTIN-NEXT:  (if
-  ;; OPTIN-NEXT:   (local.tee $len
-  ;; OPTIN-NEXT:    (array.len
-  ;; OPTIN-NEXT:     (local.get $param)
-  ;; OPTIN-NEXT:    )
-  ;; OPTIN-NEXT:   )
-  ;; OPTIN-NEXT:   (then
-  ;; OPTIN-NEXT:    (loop $label
-  ;; OPTIN-NEXT:     (local.set $index
-  ;; OPTIN-NEXT:      (i32.add
-  ;; OPTIN-NEXT:       (local.tee $curr
-  ;; OPTIN-NEXT:        (local.get $index)
-  ;; OPTIN-NEXT:       )
-  ;; OPTIN-NEXT:       (i32.const 1)
-  ;; OPTIN-NEXT:      )
-  ;; OPTIN-NEXT:     )
-  ;; OPTIN-NEXT:     (if
-  ;; OPTIN-NEXT:      (i32.le_u
-  ;; OPTIN-NEXT:       (local.get $len)
-  ;; OPTIN-NEXT:       (local.get $curr)
-  ;; OPTIN-NEXT:      )
-  ;; OPTIN-NEXT:      (then
-  ;; OPTIN-NEXT:       (unreachable)
-  ;; OPTIN-NEXT:      )
-  ;; OPTIN-NEXT:     )
-  ;; OPTIN-NEXT:     (local.set $total
-  ;; OPTIN-NEXT:      (i32.add
-  ;; OPTIN-NEXT:       (local.get $total)
-  ;; OPTIN-NEXT:       (array.get $array
-  ;; OPTIN-NEXT:        (local.get $param)
-  ;; OPTIN-NEXT:        (local.get $curr)
-  ;; OPTIN-NEXT:       )
-  ;; OPTIN-NEXT:      )
-  ;; OPTIN-NEXT:     )
-  ;; OPTIN-NEXT:     (br_if $label
-  ;; OPTIN-NEXT:      (i32.lt_u
-  ;; OPTIN-NEXT:       (local.get $index)
-  ;; OPTIN-NEXT:       (local.get $len)
-  ;; OPTIN-NEXT:      )
-  ;; OPTIN-NEXT:     )
-  ;; OPTIN-NEXT:    )
-  ;; OPTIN-NEXT:   )
-  ;; OPTIN-NEXT:  )
-  ;; OPTIN-NEXT:  (local.get $total)
-  ;; OPTIN-NEXT: )
-  (func $array-sum (param $param (ref $array)) (result i32)
-    ;; Somewhat-realistic code that sums up an array, using a software/userspace
-    ;; bounds check that can be removed.
-    (local $index i32)
-    (local $total i32)
-    (local $len i32)
-    (local $curr i32)
-    ;; Loop only if len > 0.
-    (if
-      (i32.gt_u
-        (local.tee $len
-          (array.len
-            (local.get $param)
-          )
-        )
-        (i32.const 0)
-      )
-      (then
-        (loop $label
-          ;; Increment for the next iteration, storing the current index in curr.
-          (local.set $index
-            (i32.add
-             (local.tee $curr
-               (local.get $index)
-              )
-              (i32.const 1)
-            )
-          )
-          ;; Software bounds check: if curr >= len, then the current index is invalid
-          ;; to read from the array.
-          (if
-            (i32.ge_u
-              (local.get $curr)
-              (local.get $len)
-            )
-            (then
-              (unreachable)
-            )
-          )
-          ;; Read the array and add to the total.
-          (local.set $total
-            (i32.add
-              (array.get $array
-                (local.get $param)
-                (local.get $curr)
-              )
-              (local.get $total)
-            )
-          )
-          ;; Keep looping if we did not reach the end of the array.
-          (br_if $label
-            (i32.lt_u
-              (local.get $index)
-              (local.get $len)
-            )
-          )
-        )
-      )
-    )
-    (local.get $total)
-  )
-
   ;; CHECK:      (func $local-changes (type $3) (param $x i32) (param $y i32) (param $z i32)
   ;; CHECK-NEXT:  (local.set $x
   ;; CHECK-NEXT:   (local.get $y)

From cea10d2ffa18b34d1cfce92f92fe2467e3ff838b Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 9 Jul 2026 15:23:24 -0700
Subject: [PATCH 09/12] test

---
 src/ir/constraint.cpp                    | 4 ----
 test/lit/passes/constraint-analysis.wast | 6 +++---
 2 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 4ac62614741..8a192bbd6de 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -166,8 +166,6 @@ void AndedConstraintSet::approximateOr(const AndedConstraintSet& other) {
     return;
   }
 
-std::cout << "OR " << *this << " with " << other << '\n';
-
   // If this is already implied by current constraints, then it is redundant.
   // E.g. if we are { x = 10 } and other is { x >= 0 } then all we need is
   // { x >= 0 } as the result of the OR.
@@ -184,7 +182,6 @@ std::cout << "OR " << *this << " with " << other << '\n';
   // Otherwise, we don't know how to nicely OR these things, and expand to the
   // trivial set of no constraints.
   clear();
-std::cout << "  sadd OR\n";
 }
 
 std::optional<LocalConstraint> LocalConstraint::parse(Expression* curr) {
@@ -321,7 +318,6 @@ void BasicBlockConstraintMap::approximateOr(
   // We only need to loop on our locals, as any local that is missing in us is
   // one that would end up proving nothing (and get removed).
   for (auto& [local, constraints] : map) {
-std::cout << "or local " << local << '\n';
     constraints.approximateOr(other.get(local));
   }
 
diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index 0162161d3be..32ea4621d2f 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -1008,7 +1008,7 @@
     )
   )
 
-  ;; CHECK:      (func $conditional-binary-nesting (type $5) (param $x i32) (param $y i32)
+  ;; CHECK:      (func $conditional-binary-nesting (type $2) (param $x i32) (param $y i32)
   ;; CHECK-NEXT:  (if
   ;; CHECK-NEXT:   (i32.eq
   ;; CHECK-NEXT:    (local.get $x)
@@ -2628,7 +2628,7 @@
     )
   )
 
-  ;; CHECK:      (func $local-changes-if (type $7) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
+  ;; CHECK:      (func $local-changes-if (type $5) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
   ;; CHECK-NEXT:  (if
   ;; CHECK-NEXT:   (i32.eq
   ;; CHECK-NEXT:    (local.get $x)
@@ -2685,7 +2685,7 @@
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $local-changes-if (type $7) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
+  ;; OPTIN:      (func $local-changes-if (type $5) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
   ;; OPTIN-NEXT:  (if
   ;; OPTIN-NEXT:   (i32.eq
   ;; OPTIN-NEXT:    (local.get $x)

From 4b8acf45390a4a058c29e39f7be2aa5e7ffdeedb Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 9 Jul 2026 15:25:05 -0700
Subject: [PATCH 10/12] format

---
 src/ir/abstract.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/ir/abstract.cpp b/src/ir/abstract.cpp
index c1f368c7a3f..5c95bffbcdb 100644
--- a/src/ir/abstract.cpp
+++ b/src/ir/abstract.cpp
@@ -20,7 +20,9 @@
 namespace wasm::Abstract {
 
 std::ostream& operator<<(std::ostream& o, Op op) {
-  #define HANDLE(x) case x: return o << #x;
+#define HANDLE(x)                                                              \
+  case x:                                                                      \
+    return o << #x;
   switch (op) {
     HANDLE(Abs)
     HANDLE(Neg)
@@ -58,4 +60,3 @@ std::ostream& operator<<(std::ostream& o, Op op) {
 }
 
 } // namespace wasm::Abstract
-

From c37502490ecb73be9fb3e25f534f019cac8934b1 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 9 Jul 2026 15:25:16 -0700
Subject: [PATCH 11/12] format

---
 src/ir/abstract.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/ir/abstract.cpp b/src/ir/abstract.cpp
index 5c95bffbcdb..54180ad785f 100644
--- a/src/ir/abstract.cpp
+++ b/src/ir/abstract.cpp
@@ -20,9 +20,11 @@
 namespace wasm::Abstract {
 
 std::ostream& operator<<(std::ostream& o, Op op) {
+
 #define HANDLE(x)                                                              \
   case x:                                                                      \
     return o << #x;
+
   switch (op) {
     HANDLE(Abs)
     HANDLE(Neg)

From 6c021c5e9af6b3872e3b03197149ce9856e0b97c Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 9 Jul 2026 16:23:55 -0700
Subject: [PATCH 12/12] add software bounds check test

---
 test/lit/passes/constraint-analysis.wast | 164 ++++++++++++++++++++++-
 1 file changed, 158 insertions(+), 6 deletions(-)

diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index 32ea4621d2f..5b51766a9a8 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -9,6 +9,10 @@
 ;; RUN: wasm-opt %s --optimize-instructions --constraint-analysis -all -S -o - | filecheck %s --check-prefix=OPTIN
 
 (module
+  ;; CHECK:      (type $array (array (mut i32)))
+  ;; OPTIN:      (type $array (array (mut i32)))
+  (type $array (array (mut i32)))
+
   ;; CHECK:      (func $simple (type $1)
   ;; CHECK-NEXT:  (local $x i32)
   ;; CHECK-NEXT:  (local.set $x
@@ -1510,7 +1514,7 @@
     )
   )
 
-  ;; CHECK:      (func $br_on_null (type $4) (param $param anyref)
+  ;; CHECK:      (func $br_on_null (type $5) (param $param anyref)
   ;; CHECK-NEXT:  (block $block
   ;; CHECK-NEXT:   (drop
   ;; CHECK-NEXT:    (ref.is_null
@@ -1531,7 +1535,7 @@
   ;; CHECK-NEXT:   (i32.const 1)
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $br_on_null (type $4) (param $param anyref)
+  ;; OPTIN:      (func $br_on_null (type $5) (param $param anyref)
   ;; OPTIN-NEXT:  (block $block
   ;; OPTIN-NEXT:   (drop
   ;; OPTIN-NEXT:    (ref.is_null
@@ -1581,7 +1585,7 @@
     )
   )
 
-  ;; CHECK:      (func $br_on_non_null (type $4) (param $param anyref)
+  ;; CHECK:      (func $br_on_non_null (type $5) (param $param anyref)
   ;; CHECK-NEXT:  (drop
   ;; CHECK-NEXT:   (block $block (result (ref any))
   ;; CHECK-NEXT:    (drop
@@ -1602,7 +1606,7 @@
   ;; CHECK-NEXT:   (i32.const 0)
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $br_on_non_null (type $4) (param $param anyref)
+  ;; OPTIN:      (func $br_on_non_null (type $5) (param $param anyref)
   ;; OPTIN-NEXT:  (drop
   ;; OPTIN-NEXT:   (block $block (result (ref any))
   ;; OPTIN-NEXT:    (drop
@@ -2628,7 +2632,7 @@
     )
   )
 
-  ;; CHECK:      (func $local-changes-if (type $5) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
+  ;; CHECK:      (func $local-changes-if (type $6) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
   ;; CHECK-NEXT:  (if
   ;; CHECK-NEXT:   (i32.eq
   ;; CHECK-NEXT:    (local.get $x)
@@ -2685,7 +2689,7 @@
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $local-changes-if (type $5) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
+  ;; OPTIN:      (func $local-changes-if (type $6) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
   ;; OPTIN-NEXT:  (if
   ;; OPTIN-NEXT:   (i32.eq
   ;; OPTIN-NEXT:    (local.get $x)
@@ -3320,4 +3324,152 @@
       )
     )
   )
+
+  ;; CHECK:      (func $simple-array-sum (type $7) (param $param (ref $array)) (result i32)
+  ;; CHECK-NEXT:  (local $index i32)
+  ;; CHECK-NEXT:  (local $sum i32)
+  ;; CHECK-NEXT:  (local $len i32)
+  ;; CHECK-NEXT:  (local.set $len
+  ;; CHECK-NEXT:   (array.len
+  ;; CHECK-NEXT:    (local.get $param)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (loop $loop
+  ;; CHECK-NEXT:   (if
+  ;; CHECK-NEXT:    (i32.ge_u
+  ;; CHECK-NEXT:     (local.get $index)
+  ;; CHECK-NEXT:     (local.get $len)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (then
+  ;; CHECK-NEXT:     (return
+  ;; CHECK-NEXT:      (local.get $sum)
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (if
+  ;; CHECK-NEXT:    (i32.const 0)
+  ;; CHECK-NEXT:    (then
+  ;; CHECK-NEXT:     (unreachable)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (local.set $sum
+  ;; CHECK-NEXT:    (i32.add
+  ;; CHECK-NEXT:     (local.get $sum)
+  ;; CHECK-NEXT:     (array.get $array
+  ;; CHECK-NEXT:      (local.get $param)
+  ;; CHECK-NEXT:      (local.get $index)
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (local.set $index
+  ;; CHECK-NEXT:    (i32.add
+  ;; CHECK-NEXT:     (local.get $index)
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (br $loop)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $simple-array-sum (type $7) (param $param (ref $array)) (result i32)
+  ;; OPTIN-NEXT:  (local $index i32)
+  ;; OPTIN-NEXT:  (local $sum i32)
+  ;; OPTIN-NEXT:  (local $len i32)
+  ;; OPTIN-NEXT:  (local.set $len
+  ;; OPTIN-NEXT:   (array.len
+  ;; OPTIN-NEXT:    (local.get $param)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (loop $loop
+  ;; OPTIN-NEXT:   (if
+  ;; OPTIN-NEXT:    (i32.ge_u
+  ;; OPTIN-NEXT:     (local.get $index)
+  ;; OPTIN-NEXT:     (local.get $len)
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:    (then
+  ;; OPTIN-NEXT:     (return
+  ;; OPTIN-NEXT:      (local.get $sum)
+  ;; OPTIN-NEXT:     )
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (if
+  ;; OPTIN-NEXT:    (i32.const 0)
+  ;; OPTIN-NEXT:    (then
+  ;; OPTIN-NEXT:     (unreachable)
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (local.set $sum
+  ;; OPTIN-NEXT:    (i32.add
+  ;; OPTIN-NEXT:     (array.get $array
+  ;; OPTIN-NEXT:      (local.get $param)
+  ;; OPTIN-NEXT:      (local.get $index)
+  ;; OPTIN-NEXT:     )
+  ;; OPTIN-NEXT:     (local.get $sum)
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (local.set $index
+  ;; OPTIN-NEXT:    (i32.add
+  ;; OPTIN-NEXT:     (local.get $index)
+  ;; OPTIN-NEXT:     (i32.const 1)
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (br $loop)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $simple-array-sum (param $param (ref $array)) (result i32)
+    ;; A simple but realistic software bounds check that we can remove.
+    (local $index i32)
+    (local $sum i32)
+    (local $len i32)
+    ;; Stash the length in a local.
+    (local.set $len
+      (array.len
+        (local.get $param)
+      )
+    )
+    ;; Loop over the array.
+    (loop $loop
+      ;; If we reached the end of the array, return the sum.
+      (if
+        (i32.ge_u
+          (local.get $index)
+          (local.get $len)
+        )
+        (then
+          (return
+            (local.get $sum)
+          )
+        )
+      )
+      ;; Software bounds check, right before the actual access. After we
+      ;; optimize, the condition here becomes zero, so it will be removed later.
+      (if
+        (i32.ge_u
+          (local.get $index)
+          (local.get $len)
+        )
+        (then
+          (unreachable)
+        )
+      )
+      ;; Read the array and add to the sum.
+      (local.set $sum
+        (i32.add
+          (local.get $sum)
+          (array.get $array
+            (local.get $param)
+            (local.get $index)
+          )
+        )
+      )
+      ;; Increment.
+      (local.set $index
+        (i32.add
+          (local.get $index)
+          (i32.const 1)
+        )
+      )
+      ;; Keep looping.
+      (br $loop)
+    )
+  )
 )