From 5c7b3ac98c8267bdbe0972fe4b4b1f5da953c936 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 30 Jun 2026 09:25:34 -0700
Subject: [PATCH 01/20] go

---
 src/ir/abstract.h                        |  18 +++
 src/ir/constraint.cpp                    |  52 +++++++
 src/ir/constraint.h                      |  23 +--
 src/support/inplace_vector.h             |  62 +++++++-
 test/gtest/inplace_vector.cpp            |  42 ++++++
 test/lit/passes/constraint-analysis.wast | 176 +++++++++++++++++++++++
 6 files changed, 361 insertions(+), 12 deletions(-)

diff --git a/src/ir/abstract.h b/src/ir/abstract.h
index 97b449f967b..44124381876 100644
--- a/src/ir/abstract.h
+++ b/src/ir/abstract.h
@@ -331,6 +331,24 @@ inline Op negateRelational(Op op) {
   }
 }
 
+inline bool isRelationalSymmetric(Op op) { return op == Eq || op == Ne; }
+
+inline bool isRelationalAntisymmetric(Op op) {
+  switch (op) {
+    case LtS:
+    case LtU:
+    case LeS:
+    case LeU:
+    case GtS:
+    case GtU:
+    case GeS:
+    case GeU:
+      return true;
+    default:
+      return false;
+  }
+}
+
 } // namespace wasm::Abstract
 
 #endif // wasm_ir_abstract_h
diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index d3ca5edacdf..44c42ff7058 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -250,6 +250,31 @@ LocalConstraint::parseCondition(Expression* curr) {
   return parse(curr);
 };
 
+void BasicBlockConstraintMap::set(Index index, const Constraint& c) {
+  assert(!unreachable);
+  eraseStaleRefs(index);
+  map[index].set(c);
+
+  // If the constraint refers to another local, add it there too.
+  if (auto* otherIndex = std::get_if<Index>(&c.term)) {
+    // Build a flipped constraint, referring to index.
+    Constraint otherC{c.op, index};
+    if (Abstract::isRelationalAntiSymmetric(otherC.op)) {
+      otherC.op = Abstract::negateRelational(otherC.op);
+    } else {
+      // All we support for now are symmetric and antisymmetric operations.
+      assert(Abstract::isRelationalSymmetric(c.op));
+    }
+    map[*otherIndex].approximateAnd(otherC);
+  }
+}
+
+void BasicBlockConstraintMap::setProvesNothing(Index index) {
+  assert(!unreachable);
+  eraseStaleRefs(index);
+  map.erase(index);
+}
+
 void BasicBlockConstraintMap::approximateOr(
   const BasicBlockConstraintMap& other) {
   // If one is unreachable, it adds nothing to the other.
@@ -295,6 +320,33 @@ void BasicBlockConstraintMap::approximateAnd(Index index, const Constraint& c) {
   map[index] = std::move(combined);
 }
 
+void BasicBlockConstraintMap::eraseStaleRefs(Index index) {
+  auto iter = refs.find(index);
+  if (iter == refs.end()) {
+    return;
+  }
+
+  auto& refIndexes = iter->second;
+
+  for (auto refIndex : refIndexes) {
+    if (auto iter = map.find(refIndex); iter != map.end()) {
+      auto& refConstraints = iter->second;
+      std::erase_if(refConstraints, [&](const auto& c) {
+        if (auto* i = std::get_if<Index>(&c.term)) {
+          if (*i == index) {
+            return true;
+          }
+        }
+        return false;
+      });
+      if (refConstraints.empty()) {
+        // This became trivial.
+        map.erase(iter);
+      }
+    }
+  }
+}
+
 std::ostream& operator<<(std::ostream& o, const Constraint& c) {
   o << "Constraint{" << int(c.op) << ", ";
   if (auto* cc = std::get_if<Literal>(&c.term)) {
diff --git a/src/ir/constraint.h b/src/ir/constraint.h
index 27022d10604..52220f8cab0 100644
--- a/src/ir/constraint.h
+++ b/src/ir/constraint.h
@@ -205,6 +205,10 @@ struct LocalConstraint {
 //
 // As a result, the map only contains interesting things, where we can prove
 // something (but not everything).
+//
+// Cross-local constraints (like x == y) are duplicated, that is, they appear in
+// the constraints for both x and y. This makes things simple by having all
+// constraints related to a local in the same place.
 struct BasicBlockConstraintMap {
   // Blocks begin unreachable, like AndedConstraintSet.
   bool unreachable = true;
@@ -215,15 +219,10 @@ struct BasicBlockConstraintMap {
   }
 
   // Apply a constraint to a local.
-  void set(Index index, const Constraint& c) {
-    assert(!unreachable);
-    map[index].set(c);
-  }
+  void set(Index index, const Constraint& c);
 
-  void setProvesNothing(Index index) {
-    assert(!unreachable);
-    map.erase(index);
-  }
+  // Mark a local as unknown and able to prove nothing.
+  void setProvesNothing(Index index);
 
   // Get the constraints for a local.
   AndedConstraintSet get(Index index) const {
@@ -250,6 +249,14 @@ struct BasicBlockConstraintMap {
 
 private:
   std::unordered_map<Index, AndedConstraintSet> map;
+
+  // Maps an index to the locals that have constraints referring to it. When a
+  // local is modified, we need to wipe all those constraints, which become
+  // stale.
+  std::unordered_map<Index, std::unordered_set<Index>> refs;
+
+  // Given an index, erase constraints referring to it.
+  void eraseStaleRefs(Index index);
 };
 
 std::ostream& operator<<(std::ostream& o, const Constraint& c);
diff --git a/src/support/inplace_vector.h b/src/support/inplace_vector.h
index 21826ea737d..21af95a2589 100644
--- a/src/support/inplace_vector.h
+++ b/src/support/inplace_vector.h
@@ -24,8 +24,11 @@
 #ifndef wasm_support_inplace_vector_h
 #define wasm_support_inplace_vector_h
 
+#include <algorithm>
 #include <array>
 #include <cassert>
+#include <iterator>
+#include <type_traits>
 #include <vector>
 
 #include "support/parent_index_iterator.h"
@@ -137,6 +140,7 @@ template<typename T, size_t N> class inplace_vector {
     Iterator(const Iterator& other) = default;
 
     T& operator*() { return (*this->parent)[this->index]; }
+    T* operator->() { return &(*this->parent)[this->index]; }
   };
 
   struct ConstIterator
@@ -151,6 +155,7 @@ template<typename T, size_t N> class inplace_vector {
     ConstIterator(const ConstIterator& other) = default;
 
     const T& operator*() const { return (*this->parent)[this->index]; }
+    const T* operator->() const { return &(*this->parent)[this->index]; }
   };
 
   Iterator begin() { return Iterator(this, 0); }
@@ -158,13 +163,62 @@ template<typename T, size_t N> class inplace_vector {
   ConstIterator begin() const { return ConstIterator(this, 0); }
   ConstIterator end() const { return ConstIterator(this, size()); }
 
-  void erase(Iterator a, Iterator b) {
-    // Atm we only support erasing at the end, which is very efficient.
-    assert(b == end());
-    resize(a.index);
+  Iterator erase(ConstIterator first, ConstIterator last) {
+    assert(first.index <= last.index);
+    assert(last.index <= usedFixed);
+    size_t numToErase = last.index - first.index;
+    if (numToErase > 0) {
+      std::move(fixed.begin() + last.index,
+                fixed.begin() + usedFixed,
+                fixed.begin() + first.index);
+      usedFixed -= numToErase;
+    }
+    return Iterator(this, first.index);
+  }
+
+  Iterator erase(Iterator first, Iterator last) {
+    return erase(ConstIterator(this, first.index),
+                 ConstIterator(this, last.index));
   }
+
+  Iterator erase(ConstIterator pos) { return erase(pos, pos + 1); }
+
+  Iterator erase(Iterator pos) { return erase(pos, pos + 1); }
 };
 
+namespace detail {
+
+template<typename T> struct is_inplace_vector_or_derived {
+private:
+  template<typename U, size_t N>
+  static std::true_type test(const inplace_vector<U, N>*);
+  static std::false_type test(...);
+
+public:
+  static constexpr bool value = decltype(test(std::declval<T*>()))::value;
+};
+
+} // namespace detail
+
+template<typename Vector, typename Pred>
+  requires detail::is_inplace_vector_or_derived<Vector>::value
+size_t erase_if(Vector& c, Pred pred) {
+  auto it = std::remove_if(c.begin(), c.end(), pred);
+  auto r = std::distance(it, c.end());
+  c.erase(it, c.end());
+  return r;
+}
+
 } // namespace wasm
 
+namespace std {
+
+template<typename Vector, typename Pred>
+  requires wasm::detail::is_inplace_vector_or_derived<Vector>::value
+size_t erase_if(Vector& c, Pred pred) {
+  return wasm::erase_if(c, pred);
+}
+
+} // namespace std
+
 #endif // wasm_support_inplace_vector_h
diff --git a/test/gtest/inplace_vector.cpp b/test/gtest/inplace_vector.cpp
index 34c1a3d3e1b..0480bc9f79f 100644
--- a/test/gtest/inplace_vector.cpp
+++ b/test/gtest/inplace_vector.cpp
@@ -42,3 +42,45 @@ TEST_F(InplaceVectorTest, I) {
 
   EXPECT_EQ(normal, std::vector<int>({10, 20, 30}));
 }
+
+TEST_F(InplaceVectorTest, Erase) {
+  inplace_vector<int, 5> vec{10, 20, 30, 40, 50};
+
+  // Erase single element in the middle (30 at index 2)
+  auto it = vec.erase(vec.begin() + 2);
+  EXPECT_EQ(*it, 40);
+  EXPECT_EQ(vec.size(), 4u);
+  EXPECT_EQ(vec[0], 10);
+  EXPECT_EQ(vec[1], 20);
+  EXPECT_EQ(vec[2], 40);
+  EXPECT_EQ(vec[3], 50);
+
+  // Erase range at beginning [10, 20]
+  it = vec.erase(vec.begin(), vec.begin() + 2);
+  EXPECT_EQ(*it, 40);
+  EXPECT_EQ(vec.size(), 2u);
+  EXPECT_EQ(vec[0], 40);
+  EXPECT_EQ(vec[1], 50);
+
+  // Erase at end
+  it = vec.erase(vec.begin() + 1, vec.end());
+  EXPECT_EQ(it, vec.end());
+  EXPECT_EQ(vec.size(), 1u);
+  EXPECT_EQ(vec[0], 40);
+}
+
+TEST_F(InplaceVectorTest, EraseIf) {
+  // Test std::erase_if on inplace_vector
+  inplace_vector<int, 5> vec{1, 2, 3, 4, 5};
+  size_t erased = std::erase_if(vec, [](int x) { return x % 2 == 0; });
+  EXPECT_EQ(erased, 2u);
+  EXPECT_EQ(vec.size(), 3u);
+  EXPECT_EQ(vec[0], 1);
+  EXPECT_EQ(vec[1], 3);
+  EXPECT_EQ(vec[2], 5);
+
+  // Erase remaining elements
+  erased = std::erase_if(vec, [](int x) { return x > 0; });
+  EXPECT_EQ(erased, 3u);
+  EXPECT_TRUE(vec.empty());
+}
diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index 5417c9ee8f6..1ea749091e6 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -1651,4 +1651,180 @@
       )
     )
   )
+
+  ;; CHECK:      (func $local-changes (type $4) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
+  ;; CHECK-NEXT:  (if
+  ;; CHECK-NEXT:   (i32.eq
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (local.get $y)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (then
+  ;; CHECK-NEXT:    (if
+  ;; CHECK-NEXT:     (i32.eq
+  ;; CHECK-NEXT:      (local.get $x)
+  ;; CHECK-NEXT:      (local.get $z)
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:     (then
+  ;; CHECK-NEXT:      (drop
+  ;; CHECK-NEXT:       (i32.const 1)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:      (drop
+  ;; CHECK-NEXT:       (i32.eq
+  ;; CHECK-NEXT:        (local.get $y)
+  ;; CHECK-NEXT:        (local.get $x)
+  ;; CHECK-NEXT:       )
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:      (drop
+  ;; CHECK-NEXT:       (i32.const 1)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:      (drop
+  ;; CHECK-NEXT:       (i32.eq
+  ;; CHECK-NEXT:        (local.get $z)
+  ;; CHECK-NEXT:        (local.get $x)
+  ;; CHECK-NEXT:       )
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:      (local.set $y
+  ;; CHECK-NEXT:       (local.get $w)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:      (drop
+  ;; CHECK-NEXT:       (i32.const 1)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:      (drop
+  ;; CHECK-NEXT:       (i32.eq
+  ;; CHECK-NEXT:        (local.get $y)
+  ;; CHECK-NEXT:        (local.get $x)
+  ;; CHECK-NEXT:       )
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:      (drop
+  ;; CHECK-NEXT:       (i32.const 1)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:      (drop
+  ;; CHECK-NEXT:       (i32.eq
+  ;; CHECK-NEXT:        (local.get $z)
+  ;; CHECK-NEXT:        (local.get $x)
+  ;; CHECK-NEXT:       )
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $local-changes (type $4) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
+  ;; OPTIN-NEXT:  (if
+  ;; OPTIN-NEXT:   (i32.eq
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (local.get $y)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (then
+  ;; OPTIN-NEXT:    (if
+  ;; OPTIN-NEXT:     (i32.eq
+  ;; OPTIN-NEXT:      (local.get $x)
+  ;; OPTIN-NEXT:      (local.get $z)
+  ;; OPTIN-NEXT:     )
+  ;; OPTIN-NEXT:     (then
+  ;; OPTIN-NEXT:      (drop
+  ;; OPTIN-NEXT:       (i32.const 1)
+  ;; OPTIN-NEXT:      )
+  ;; OPTIN-NEXT:      (drop
+  ;; OPTIN-NEXT:       (i32.const 1)
+  ;; OPTIN-NEXT:      )
+  ;; OPTIN-NEXT:      (drop
+  ;; OPTIN-NEXT:       (i32.const 1)
+  ;; OPTIN-NEXT:      )
+  ;; OPTIN-NEXT:      (drop
+  ;; OPTIN-NEXT:       (i32.const 1)
+  ;; OPTIN-NEXT:      )
+  ;; OPTIN-NEXT:      (local.set $y
+  ;; OPTIN-NEXT:       (local.get $w)
+  ;; OPTIN-NEXT:      )
+  ;; OPTIN-NEXT:      (drop
+  ;; OPTIN-NEXT:       (i32.const 1)
+  ;; OPTIN-NEXT:      )
+  ;; OPTIN-NEXT:      (drop
+  ;; OPTIN-NEXT:       (i32.const 1)
+  ;; OPTIN-NEXT:      )
+  ;; OPTIN-NEXT:      (drop
+  ;; OPTIN-NEXT:       (i32.const 1)
+  ;; OPTIN-NEXT:      )
+  ;; OPTIN-NEXT:      (drop
+  ;; OPTIN-NEXT:       (i32.const 1)
+  ;; OPTIN-NEXT:      )
+  ;; OPTIN-NEXT:     )
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $local-changes (param $x i32) (param $y i32) (param $z i32) (param $w i32)
+    (if
+      (i32.eq
+        (local.get $x)
+        (local.get $y)
+      )
+      (then
+        (if
+          (i32.eq
+            (local.get $x)
+            (local.get $z)
+          )
+          (then
+            ;; x == y and x == z here.
+            (drop
+              (i32.eq
+                (local.get $x)
+                (local.get $y)
+              )
+            )
+            (drop
+              (i32.eq
+                (local.get $y)
+                (local.get $x)
+              )
+            )
+            (drop
+              (i32.eq
+                (local.get $x)
+                (local.get $z)
+              )
+            )
+            (drop
+              (i32.eq
+                (local.get $z)
+                (local.get $x)
+              )
+            )
+            ;; TODO: y == z
+
+            ;; Modify y. x is still equal to z.
+            (local.set $y
+              (local.get $w)
+            )
+            (drop
+              (i32.eq
+                (local.get $x)
+                (local.get $y)
+              )
+            )
+            (drop
+              (i32.eq
+                (local.get $y)
+                (local.get $x)
+              )
+            )
+            (drop
+              (i32.eq
+                (local.get $x)
+                (local.get $z)
+              )
+            )
+            (drop
+              (i32.eq
+                (local.get $z)
+                (local.get $x)
+              )
+            )
+          )
+        )
+      )
+    )
+  )
 )

From 5314388c57d0e152989c53a0441e737815d7fa0b Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 30 Jun 2026 09:40:22 -0700
Subject: [PATCH 02/20] go

---
 src/ir/constraint.cpp | 36 ++++++++++++++++++++++++------------
 src/ir/constraint.h   | 10 +++++++++-
 2 files changed, 33 insertions(+), 13 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 44c42ff7058..4a103da8985 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -256,16 +256,8 @@ void BasicBlockConstraintMap::set(Index index, const Constraint& c) {
   map[index].set(c);
 
   // If the constraint refers to another local, add it there too.
-  if (auto* otherIndex = std::get_if<Index>(&c.term)) {
-    // Build a flipped constraint, referring to index.
-    Constraint otherC{c.op, index};
-    if (Abstract::isRelationalAntiSymmetric(otherC.op)) {
-      otherC.op = Abstract::negateRelational(otherC.op);
-    } else {
-      // All we support for now are symmetric and antisymmetric operations.
-      assert(Abstract::isRelationalSymmetric(c.op));
-    }
-    map[*otherIndex].approximateAnd(otherC);
+  if (std::holds_alternative<Index>(c.term)) {
+    approximateAndInternal(c, true);
   }
 }
 
@@ -301,9 +293,23 @@ void BasicBlockConstraintMap::approximateOr(
   });
 }
 
-void BasicBlockConstraintMap::approximateAnd(Index index, const Constraint& c) {
+void BasicBlockConstraintMap::approximateAndInternal(Index index, const Constraint& c, bool flip) {
+  Constraint actual = c;
+  if (flip) {
+    // Build a flipped constraint, referring to index.
+    auto otherIndex = std::get<Index>(&actual.term);
+    actual.term = index;
+    index = otherIndex;
+    if (Abstract::isRelationalAntisymmetric(actual.op)) {
+      actual.op = Abstract::negateRelational(actual.op);
+    } else {
+      // All we support for now are symmetric and antisymmetric operations.
+      assert(Abstract::isRelationalSymmetric(actual.op));
+    }
+  }
+
   auto combined = get(index);
-  combined.approximateAnd(c);
+  combined.approximateAnd(actual);
 
   if (combined.provesEverything()) {
     // We just proved we are in unreachable code.
@@ -318,6 +324,12 @@ void BasicBlockConstraintMap::approximateAnd(Index index, const Constraint& c) {
 
   // Otherwise, this is an interesting state; set it.
   map[index] = std::move(combined);
+
+  // If this is not the flipped version, and it refers to a local, add the
+  // flipped one too.
+  if (!flip && std::holds_alternative<Index>(actual.term)) {
+    approximateAndInternal(actual, true);
+  }
 }
 
 void BasicBlockConstraintMap::eraseStaleRefs(Index index) {
diff --git a/src/ir/constraint.h b/src/ir/constraint.h
index 52220f8cab0..0a741d3c7f1 100644
--- a/src/ir/constraint.h
+++ b/src/ir/constraint.h
@@ -238,7 +238,9 @@ struct BasicBlockConstraintMap {
   void approximateOr(const BasicBlockConstraintMap& other);
 
   // Perform an AND as above, on a particular index.
-  void approximateAnd(Index index, const Constraint& c);
+  void approximateAnd(Index index, const Constraint& c) {
+    approximateAndInternal(index, c);
+  }
 
   bool operator!=(const BasicBlockConstraintMap& other) {
     return unreachable != other.unreachable || map != other.map;
@@ -257,6 +259,12 @@ struct BasicBlockConstraintMap {
 
   // Given an index, erase constraints referring to it.
   void eraseStaleRefs(Index index);
+
+  // Internal version, with a flag to flip the constraint. Whenever we apply
+  // e.g. x == y, we also apply y == x to y, to maintain the invariant described
+  // above. When flip is true, we flip the constraint and apply it to the other
+  // index (y == x) in this example.
+  void approximateAndInternal(Index index, const Constraint& c, bool flip = false);
 };
 
 std::ostream& operator<<(std::ostream& o, const Constraint& c);

From 75e8ea3e744aa58bb17dbb282054e2019f37a7af Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 30 Jun 2026 09:41:35 -0700
Subject: [PATCH 03/20] go

---
 src/ir/constraint.cpp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 4a103da8985..952d12d0f8b 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -257,7 +257,7 @@ void BasicBlockConstraintMap::set(Index index, const Constraint& c) {
 
   // If the constraint refers to another local, add it there too.
   if (std::holds_alternative<Index>(c.term)) {
-    approximateAndInternal(c, true);
+    approximateAndInternal(index, c, true);
   }
 }
 
@@ -297,8 +297,8 @@ void BasicBlockConstraintMap::approximateAndInternal(Index index, const Constrai
   Constraint actual = c;
   if (flip) {
     // Build a flipped constraint, referring to index.
-    auto otherIndex = std::get<Index>(&actual.term);
-    actual.term = index;
+    auto otherIndex = std::get<Index>(actual.term);
+    actual.term = Term{index};
     index = otherIndex;
     if (Abstract::isRelationalAntisymmetric(actual.op)) {
       actual.op = Abstract::negateRelational(actual.op);
@@ -328,7 +328,7 @@ void BasicBlockConstraintMap::approximateAndInternal(Index index, const Constrai
   // If this is not the flipped version, and it refers to a local, add the
   // flipped one too.
   if (!flip && std::holds_alternative<Index>(actual.term)) {
-    approximateAndInternal(actual, true);
+    approximateAndInternal(index, actual, true);
   }
 }
 

From 204ae5118d87114f077771bf09cd2677039f0770 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 30 Jun 2026 09:49:38 -0700
Subject: [PATCH 04/20] work

---
 src/passes/ConstraintAnalysis.cpp | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/passes/ConstraintAnalysis.cpp b/src/passes/ConstraintAnalysis.cpp
index a6e06760220..39a5b7d171b 100644
--- a/src/passes/ConstraintAnalysis.cpp
+++ b/src/passes/ConstraintAnalysis.cpp
@@ -301,13 +301,23 @@ struct ConstraintAnalysis
   void applyToConstraints(Expression* curr,
                           BasicBlockConstraintMap& constraints) {
     if (auto* set = curr->dynCast<LocalSet>()) {
+std::cout << "apply " << *curr << "\n";
       if (Properties::isSingleConstantExpression(set->value)) {
-        // We know this one constraint.
+        // Apply a constraint to this value.
         auto value = Properties::getLiteral(set->value);
+std::cout << constraints << "\n";
         constraints.set(set->index, Constraint{Abstract::Eq, {value}});
+std::cout << " ==>\n" << constraints << "\n";
+      } else if (auto* get = set->value->dynCast<LocalGet>()) {
+        // Apply a constraint to this local..
+std::cout << constraints << "\n";
+        constraints.set(set->index, Constraint{Abstract::Eq, {get->index}});
+std::cout << " =1=>\n" << constraints << "\n";
       } else {
         // We know and can prove nothing.
+std::cout << constraints << "\n";
         constraints.setProvesNothing(set->index);
+std::cout << " =2=>\n" << constraints << "\n";
       }
     }
   }

From 06c45911a0bae21313e22b4004d356f1f351d0ad Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 30 Jun 2026 09:56:20 -0700
Subject: [PATCH 05/20] work

---
 src/ir/constraint.cpp             | 12 ++++++++++++
 src/ir/constraint.h               |  3 +++
 src/passes/ConstraintAnalysis.cpp |  7 -------
 3 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 952d12d0f8b..18d3d0e8d4d 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -254,6 +254,7 @@ void BasicBlockConstraintMap::set(Index index, const Constraint& c) {
   assert(!unreachable);
   eraseStaleRefs(index);
   map[index].set(c);
+  noteRefs(index, c);
 
   // If the constraint refers to another local, add it there too.
   if (std::holds_alternative<Index>(c.term)) {
@@ -308,6 +309,11 @@ void BasicBlockConstraintMap::approximateAndInternal(Index index, const Constrai
     }
   }
 
+  // Add a ref of what we are adding. Note that the approximation below may end
+  // up not actually adding this, or adding only part of this, but it is safe to
+  // always add a ref (at the cost of minor wasted work).
+  noteRefs(index, actual);
+
   auto combined = get(index);
   combined.approximateAnd(actual);
 
@@ -332,6 +338,12 @@ void BasicBlockConstraintMap::approximateAndInternal(Index index, const Constrai
   }
 }
 
+void BasicBlockConstraintMap::noteRefs(Index index, const Constraint& c) {
+  if (auto* i = std::get_if<Index>(&c.term)) {
+    refs[*i].insert(index);
+  }
+}
+
 void BasicBlockConstraintMap::eraseStaleRefs(Index index) {
   auto iter = refs.find(index);
   if (iter == refs.end()) {
diff --git a/src/ir/constraint.h b/src/ir/constraint.h
index 0a741d3c7f1..54cebbeddfc 100644
--- a/src/ir/constraint.h
+++ b/src/ir/constraint.h
@@ -257,6 +257,9 @@ struct BasicBlockConstraintMap {
   // stale.
   std::unordered_map<Index, std::unordered_set<Index>> refs;
 
+  // Given a constraint on a local, note refs.
+  void noteRefs(Index index, const Constraint& c);
+
   // Given an index, erase constraints referring to it.
   void eraseStaleRefs(Index index);
 
diff --git a/src/passes/ConstraintAnalysis.cpp b/src/passes/ConstraintAnalysis.cpp
index 39a5b7d171b..257f0fd91bd 100644
--- a/src/passes/ConstraintAnalysis.cpp
+++ b/src/passes/ConstraintAnalysis.cpp
@@ -301,23 +301,16 @@ struct ConstraintAnalysis
   void applyToConstraints(Expression* curr,
                           BasicBlockConstraintMap& constraints) {
     if (auto* set = curr->dynCast<LocalSet>()) {
-std::cout << "apply " << *curr << "\n";
       if (Properties::isSingleConstantExpression(set->value)) {
         // Apply a constraint to this value.
         auto value = Properties::getLiteral(set->value);
-std::cout << constraints << "\n";
         constraints.set(set->index, Constraint{Abstract::Eq, {value}});
-std::cout << " ==>\n" << constraints << "\n";
       } else if (auto* get = set->value->dynCast<LocalGet>()) {
         // Apply a constraint to this local..
-std::cout << constraints << "\n";
         constraints.set(set->index, Constraint{Abstract::Eq, {get->index}});
-std::cout << " =1=>\n" << constraints << "\n";
       } else {
         // We know and can prove nothing.
-std::cout << constraints << "\n";
         constraints.setProvesNothing(set->index);
-std::cout << " =2=>\n" << constraints << "\n";
       }
     }
   }

From fd96dbc368a51df3c83d3a090c993f8496209089 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 30 Jun 2026 09:56:58 -0700
Subject: [PATCH 06/20] work

---
 src/ir/constraint.cpp | 4 +++-
 src/ir/constraint.h   | 3 ++-
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 18d3d0e8d4d..e1eeb8357a3 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -294,7 +294,9 @@ void BasicBlockConstraintMap::approximateOr(
   });
 }
 
-void BasicBlockConstraintMap::approximateAndInternal(Index index, const Constraint& c, bool flip) {
+void BasicBlockConstraintMap::approximateAndInternal(Index index,
+                                                     const Constraint& c,
+                                                     bool flip) {
   Constraint actual = c;
   if (flip) {
     // Build a flipped constraint, referring to index.
diff --git a/src/ir/constraint.h b/src/ir/constraint.h
index 54cebbeddfc..295f69f50b5 100644
--- a/src/ir/constraint.h
+++ b/src/ir/constraint.h
@@ -267,7 +267,8 @@ struct BasicBlockConstraintMap {
   // e.g. x == y, we also apply y == x to y, to maintain the invariant described
   // above. When flip is true, we flip the constraint and apply it to the other
   // index (y == x) in this example.
-  void approximateAndInternal(Index index, const Constraint& c, bool flip = false);
+  void
+  approximateAndInternal(Index index, const Constraint& c, bool flip = false);
 };
 
 std::ostream& operator<<(std::ostream& o, const Constraint& c);

From c597f52931efe899e5199592bff2161fb6e93b0c Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 30 Jun 2026 10:22:09 -0700
Subject: [PATCH 07/20] work

---
 test/lit/passes/constraint-analysis.wast | 54 ++++++++++++++++++------
 1 file changed, 40 insertions(+), 14 deletions(-)

diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index 1ea749091e6..efbfcd451e6 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -1669,25 +1669,22 @@
   ;; CHECK-NEXT:       (i32.const 1)
   ;; CHECK-NEXT:      )
   ;; CHECK-NEXT:      (drop
-  ;; CHECK-NEXT:       (i32.eq
-  ;; CHECK-NEXT:        (local.get $y)
-  ;; CHECK-NEXT:        (local.get $x)
-  ;; CHECK-NEXT:       )
+  ;; CHECK-NEXT:       (i32.const 1)
   ;; CHECK-NEXT:      )
   ;; CHECK-NEXT:      (drop
   ;; CHECK-NEXT:       (i32.const 1)
   ;; CHECK-NEXT:      )
   ;; CHECK-NEXT:      (drop
-  ;; CHECK-NEXT:       (i32.eq
-  ;; CHECK-NEXT:        (local.get $z)
-  ;; CHECK-NEXT:        (local.get $x)
-  ;; CHECK-NEXT:       )
+  ;; CHECK-NEXT:       (i32.const 1)
   ;; CHECK-NEXT:      )
   ;; CHECK-NEXT:      (local.set $y
   ;; CHECK-NEXT:       (local.get $w)
   ;; CHECK-NEXT:      )
   ;; CHECK-NEXT:      (drop
-  ;; CHECK-NEXT:       (i32.const 1)
+  ;; CHECK-NEXT:       (i32.eq
+  ;; CHECK-NEXT:        (local.get $x)
+  ;; CHECK-NEXT:        (local.get $y)
+  ;; CHECK-NEXT:       )
   ;; CHECK-NEXT:      )
   ;; CHECK-NEXT:      (drop
   ;; CHECK-NEXT:       (i32.eq
@@ -1699,10 +1696,13 @@
   ;; CHECK-NEXT:       (i32.const 1)
   ;; CHECK-NEXT:      )
   ;; CHECK-NEXT:      (drop
-  ;; CHECK-NEXT:       (i32.eq
-  ;; CHECK-NEXT:        (local.get $z)
-  ;; CHECK-NEXT:        (local.get $x)
-  ;; CHECK-NEXT:       )
+  ;; CHECK-NEXT:       (i32.const 1)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:      (drop
+  ;; CHECK-NEXT:       (i32.const 1)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:      (drop
+  ;; CHECK-NEXT:       (i32.const 1)
   ;; CHECK-NEXT:      )
   ;; CHECK-NEXT:     )
   ;; CHECK-NEXT:    )
@@ -1738,6 +1738,18 @@
   ;; OPTIN-NEXT:       (local.get $w)
   ;; OPTIN-NEXT:      )
   ;; OPTIN-NEXT:      (drop
+  ;; OPTIN-NEXT:       (i32.eq
+  ;; OPTIN-NEXT:        (local.get $x)
+  ;; OPTIN-NEXT:        (local.get $y)
+  ;; OPTIN-NEXT:       )
+  ;; OPTIN-NEXT:      )
+  ;; OPTIN-NEXT:      (drop
+  ;; OPTIN-NEXT:       (i32.eq
+  ;; OPTIN-NEXT:        (local.get $x)
+  ;; OPTIN-NEXT:        (local.get $y)
+  ;; OPTIN-NEXT:       )
+  ;; OPTIN-NEXT:      )
+  ;; OPTIN-NEXT:      (drop
   ;; OPTIN-NEXT:       (i32.const 1)
   ;; OPTIN-NEXT:      )
   ;; OPTIN-NEXT:      (drop
@@ -1794,7 +1806,8 @@
             )
             ;; TODO: y == z
 
-            ;; Modify y. x is still equal to z.
+            ;; Modify y to the value of w. x is still equal to z, but no longer
+            ;; to y.
             (local.set $y
               (local.get $w)
             )
@@ -1822,6 +1835,19 @@
                 (local.get $x)
               )
             )
+            ;; But y == w.
+            (drop
+              (i32.eq
+                (local.get $y)
+                (local.get $w)
+              )
+            )
+            (drop
+              (i32.eq
+                (local.get $w)
+                (local.get $y)
+              )
+            )
           )
         )
       )

From f660b234cbe7f40a9b95a9409babd212dd97b6de Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 30 Jun 2026 10:27:11 -0700
Subject: [PATCH 08/20] work

---
 test/lit/passes/constraint-analysis.wast | 155 ++++++++++++++++++++++-
 1 file changed, 152 insertions(+), 3 deletions(-)

diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index efbfcd451e6..2822db6c762 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -1652,7 +1652,155 @@
     )
   )
 
-  ;; CHECK:      (func $local-changes (type $4) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
+  ;; CHECK:      (func $local-changes (type $4) (param $x i32) (param $y i32) (param $z i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (local.get $y)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.eq
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (local.get $z)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.eq
+  ;; CHECK-NEXT:    (local.get $z)
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (local.get $z)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.eq
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (local.get $y)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.eq
+  ;; CHECK-NEXT:    (local.get $y)
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $local-changes (type $4) (param $x i32) (param $y i32) (param $z i32)
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (local.get $y)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.eq
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (local.get $z)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.eq
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (local.get $z)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (local.get $z)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.eq
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (local.get $y)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.eq
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (local.get $y)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $local-changes (param $x i32) (param $y i32) (param $z i32)
+    (local.set $x
+      (local.get $y)
+    )
+    ;; x == y but not z.
+    (drop
+      (i32.eq
+        (local.get $x)
+        (local.get $y)
+      )
+    )
+    (drop
+      (i32.eq
+        (local.get $y)
+        (local.get $x)
+      )
+    )
+    (drop
+      (i32.eq
+        (local.get $x)
+        (local.get $z)
+      )
+    )
+    (drop
+      (i32.eq
+        (local.get $z)
+        (local.get $x)
+      )
+    )
+
+    ;; Set x to z. Now x == z but we can prove nothing about x and y.
+    (local.set $x
+      (local.get $z)
+    )
+    (drop
+      (i32.eq
+        (local.get $x)
+        (local.get $y)
+      )
+    )
+    (drop
+      (i32.eq
+        (local.get $y)
+        (local.get $x)
+      )
+    )
+    (drop
+      (i32.eq
+        (local.get $x)
+        (local.get $z)
+      )
+    )
+    (drop
+      (i32.eq
+        (local.get $z)
+        (local.get $x)
+      )
+    )
+  )
+
+  ;; 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)
@@ -1709,7 +1857,7 @@
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $local-changes (type $4) (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)
@@ -1766,7 +1914,8 @@
   ;; OPTIN-NEXT:   )
   ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT: )
-  (func $local-changes (param $x i32) (param $y i32) (param $z i32) (param $w i32)
+  (func $local-changes-if (param $x i32) (param $y i32) (param $z i32) (param $w i32)
+    ;; Local changes after if conditions set up constraints.
     (if
       (i32.eq
         (local.get $x)

From f2b8ce9d6ea5a36c659d57f5cb755181abb89106 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 30 Jun 2026 10:28:50 -0700
Subject: [PATCH 09/20] work

---
 test/lit/passes/constraint-analysis.wast | 169 ++++++++++++++++++++++-
 1 file changed, 165 insertions(+), 4 deletions(-)

diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index 2822db6c762..b0d195bca9a 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 $3) (param $x i32) (param $y i32)
+  ;; CHECK:      (func $conditional-binary-nesting (type $4) (param $x i32) (param $y i32)
   ;; CHECK-NEXT:  (if
   ;; CHECK-NEXT:   (i32.eq
   ;; CHECK-NEXT:    (local.get $x)
@@ -1038,7 +1038,7 @@
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $conditional-binary-nesting (type $3) (param $x i32) (param $y i32)
+  ;; OPTIN:      (func $conditional-binary-nesting (type $4) (param $x i32) (param $y i32)
   ;; OPTIN-NEXT:  (if
   ;; OPTIN-NEXT:   (i32.eq
   ;; OPTIN-NEXT:    (local.get $x)
@@ -1652,7 +1652,7 @@
     )
   )
 
-  ;; CHECK:      (func $local-changes (type $4) (param $x i32) (param $y i32) (param $z i32)
+  ;; 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)
   ;; CHECK-NEXT:  )
@@ -1696,7 +1696,7 @@
   ;; CHECK-NEXT:   (i32.const 1)
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $local-changes (type $4) (param $x i32) (param $y i32) (param $z i32)
+  ;; OPTIN:      (func $local-changes (type $3) (param $x i32) (param $y i32) (param $z i32)
   ;; OPTIN-NEXT:  (local.set $x
   ;; OPTIN-NEXT:   (local.get $y)
   ;; OPTIN-NEXT:  )
@@ -1800,6 +1800,167 @@
     )
   )
 
+  ;; CHECK:      (func $local-changes-2 (type $3) (param $x i32) (param $y i32) (param $z i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (local.get $y)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.eq
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (local.get $z)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.eq
+  ;; CHECK-NEXT:    (local.get $z)
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (local.set $y
+  ;; CHECK-NEXT:   (local.get $z)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.eq
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (local.get $y)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.eq
+  ;; CHECK-NEXT:    (local.get $y)
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.eq
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (local.get $z)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.eq
+  ;; CHECK-NEXT:    (local.get $z)
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $local-changes-2 (type $3) (param $x i32) (param $y i32) (param $z i32)
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (local.get $y)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.eq
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (local.get $z)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.eq
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (local.get $z)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (local.set $y
+  ;; OPTIN-NEXT:   (local.get $z)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.eq
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (local.get $y)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.eq
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (local.get $y)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.eq
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (local.get $z)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.eq
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (local.get $z)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $local-changes-2 (param $x i32) (param $y i32) (param $z i32)
+    ;; As above, but the set in the middle is on y, not x.
+    (local.set $x
+      (local.get $y)
+    )
+    ;; x == y but not z, as above.
+    (drop
+      (i32.eq
+        (local.get $x)
+        (local.get $y)
+      )
+    )
+    (drop
+      (i32.eq
+        (local.get $y)
+        (local.get $x)
+      )
+    )
+    (drop
+      (i32.eq
+        (local.get $x)
+        (local.get $z)
+      )
+    )
+    (drop
+      (i32.eq
+        (local.get $z)
+        (local.get $x)
+      )
+    )
+
+    (local.set $y    ;; this changed
+      (local.get $z)
+    )
+    ;; We can prove nothing here.
+    (drop
+      (i32.eq
+        (local.get $x)
+        (local.get $y)
+      )
+    )
+    (drop
+      (i32.eq
+        (local.get $y)
+        (local.get $x)
+      )
+    )
+    (drop
+      (i32.eq
+        (local.get $x)
+        (local.get $z)
+      )
+    )
+    (drop
+      (i32.eq
+        (local.get $z)
+        (local.get $x)
+      )
+    )
+  )
+
   ;; 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

From 6c78762b6f689ea18e594bf2cc4634106d45f6b2 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 30 Jun 2026 10:30:11 -0700
Subject: [PATCH 10/20] work

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

diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index b0d195bca9a..8e69064d816 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -1695,6 +1695,18 @@
   ;; CHECK-NEXT:  (drop
   ;; CHECK-NEXT:   (i32.const 1)
   ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.eq
+  ;; CHECK-NEXT:    (local.get $y)
+  ;; CHECK-NEXT:    (local.get $z)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.eq
+  ;; CHECK-NEXT:    (local.get $z)
+  ;; CHECK-NEXT:    (local.get $y)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
   ;; OPTIN:      (func $local-changes (type $3) (param $x i32) (param $y i32) (param $z i32)
   ;; OPTIN-NEXT:  (local.set $x
@@ -1739,6 +1751,18 @@
   ;; OPTIN-NEXT:  (drop
   ;; OPTIN-NEXT:   (i32.const 1)
   ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.eq
+  ;; OPTIN-NEXT:    (local.get $y)
+  ;; OPTIN-NEXT:    (local.get $z)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.eq
+  ;; OPTIN-NEXT:    (local.get $y)
+  ;; OPTIN-NEXT:    (local.get $z)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT: )
   (func $local-changes (param $x i32) (param $y i32) (param $z i32)
     (local.set $x
@@ -1798,6 +1822,20 @@
         (local.get $x)
       )
     )
+
+    ;; No idea about y vs z.
+    (drop
+      (i32.eq
+        (local.get $y)
+        (local.get $z)
+      )
+    )
+    (drop
+      (i32.eq
+        (local.get $z)
+        (local.get $y)
+      )
+    )
   )
 
   ;; CHECK:      (func $local-changes-2 (type $3) (param $x i32) (param $y i32) (param $z i32)
@@ -1849,6 +1887,12 @@
   ;; CHECK-NEXT:    (local.get $x)
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
   ;; OPTIN:      (func $local-changes-2 (type $3) (param $x i32) (param $y i32) (param $z i32)
   ;; OPTIN-NEXT:  (local.set $x
@@ -1899,6 +1943,12 @@
   ;; OPTIN-NEXT:    (local.get $z)
   ;; OPTIN-NEXT:   )
   ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT: )
   (func $local-changes-2 (param $x i32) (param $y i32) (param $z i32)
     ;; As above, but the set in the middle is on y, not x.
@@ -1959,6 +2009,20 @@
         (local.get $x)
       )
     )
+
+    ;; But y == z.
+    (drop
+      (i32.eq
+        (local.get $y)
+        (local.get $z)
+      )
+    )
+    (drop
+      (i32.eq
+        (local.get $z)
+        (local.get $y)
+      )
+    )
   )
 
   ;; CHECK:      (func $local-changes-if (type $5) (param $x i32) (param $y i32) (param $z i32) (param $w i32)

From b5786f8f968804e050872e5d0141ee7081541f50 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 30 Jun 2026 10:45:03 -0700
Subject: [PATCH 11/20] work

---
 src/support/inplace_vector.h | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/support/inplace_vector.h b/src/support/inplace_vector.h
index 21af95a2589..09b8d3abf15 100644
--- a/src/support/inplace_vector.h
+++ b/src/support/inplace_vector.h
@@ -137,7 +137,6 @@ template<typename T, size_t N> class inplace_vector {
     Iterator(inplace_vector<T, N>* parent, size_t index)
       : wasm::ParentIndexIterator<inplace_vector<T, N>*, Iterator>{parent,
                                                                    index} {}
-    Iterator(const Iterator& other) = default;
 
     T& operator*() { return (*this->parent)[this->index]; }
     T* operator->() { return &(*this->parent)[this->index]; }

From 69cc1b15a91903ff986ae25ef715a04d00490b89 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 30 Jun 2026 10:47:16 -0700
Subject: [PATCH 12/20] work

---
 src/ir/constraint.h | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/ir/constraint.h b/src/ir/constraint.h
index 295f69f50b5..397685d7f9e 100644
--- a/src/ir/constraint.h
+++ b/src/ir/constraint.h
@@ -242,6 +242,10 @@ struct BasicBlockConstraintMap {
     approximateAndInternal(index, c);
   }
 
+  // TODO: Add proves() here, which could do things like: if asked x == y, we
+  // can answer False if we see x == c1, y == c2, and the constants c1, c2
+  // differ.
+
   bool operator!=(const BasicBlockConstraintMap& other) {
     return unreachable != other.unreachable || map != other.map;
   }

From 2fc836957fb82e5db6e84e9d22daa44646a0710c Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 30 Jun 2026 10:51:24 -0700
Subject: [PATCH 13/20] work

---
 src/ir/constraint.h | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/ir/constraint.h b/src/ir/constraint.h
index 397685d7f9e..f98fc56fa94 100644
--- a/src/ir/constraint.h
+++ b/src/ir/constraint.h
@@ -259,6 +259,11 @@ struct BasicBlockConstraintMap {
   // Maps an index to the locals that have constraints referring to it. When a
   // local is modified, we need to wipe all those constraints, which become
   // stale.
+  //
+  // It is ok (but unoptimal in efficiency) if we have stale refs here, e.g. due
+  // to approximation removing a constraint. Whenever there is a reference,
+  // however, it must be noted here, so that when things get stale we can remove
+  // them.
   std::unordered_map<Index, std::unordered_set<Index>> refs;
 
   // Given a constraint on a local, note refs.

From f74e978c3094137fb43626c44c19b6f23f71f1ea Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 30 Jun 2026 12:00:58 -0700
Subject: [PATCH 14/20] work

---
 src/ir/constraint.cpp                    |  10 +-
 test/lit/passes/constraint-analysis.wast | 231 ++++++++++++++++++++++-
 2 files changed, 228 insertions(+), 13 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index e1eeb8357a3..326cdbaef71 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -311,11 +311,6 @@ void BasicBlockConstraintMap::approximateAndInternal(Index index,
     }
   }
 
-  // Add a ref of what we are adding. Note that the approximation below may end
-  // up not actually adding this, or adding only part of this, but it is safe to
-  // always add a ref (at the cost of minor wasted work).
-  noteRefs(index, actual);
-
   auto combined = get(index);
   combined.approximateAnd(actual);
 
@@ -333,6 +328,11 @@ void BasicBlockConstraintMap::approximateAndInternal(Index index,
   // Otherwise, this is an interesting state; set it.
   map[index] = std::move(combined);
 
+  // Add a ref of what we are adding. Note that the approximation above may end
+  // up not actually adding this, or adding only part of this, but it is safe to
+  // always add a ref (at the cost of minor wasted work).
+  noteRefs(index, actual);
+
   // If this is not the flipped version, and it refers to a local, add the
   // flipped one too.
   if (!flip && std::holds_alternative<Index>(actual.term)) {
diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index 8e69064d816..2f04cb12b58 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -1510,7 +1510,7 @@
     )
   )
 
-  ;; CHECK:      (func $br_on_null (type $2) (param $param anyref)
+  ;; CHECK:      (func $br_on_null (type $3) (param $param anyref)
   ;; CHECK-NEXT:  (block $block
   ;; CHECK-NEXT:   (drop
   ;; CHECK-NEXT:    (ref.is_null
@@ -1531,7 +1531,7 @@
   ;; CHECK-NEXT:   (i32.const 1)
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $br_on_null (type $2) (param $param anyref)
+  ;; OPTIN:      (func $br_on_null (type $3) (param $param anyref)
   ;; OPTIN-NEXT:  (block $block
   ;; OPTIN-NEXT:   (drop
   ;; OPTIN-NEXT:    (ref.is_null
@@ -1581,7 +1581,7 @@
     )
   )
 
-  ;; CHECK:      (func $br_on_non_null (type $2) (param $param anyref)
+  ;; CHECK:      (func $br_on_non_null (type $3) (param $param anyref)
   ;; CHECK-NEXT:  (drop
   ;; CHECK-NEXT:   (block $block (result (ref any))
   ;; CHECK-NEXT:    (drop
@@ -1602,7 +1602,7 @@
   ;; CHECK-NEXT:   (i32.const 0)
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $br_on_non_null (type $2) (param $param anyref)
+  ;; OPTIN:      (func $br_on_non_null (type $3) (param $param anyref)
   ;; OPTIN-NEXT:  (drop
   ;; OPTIN-NEXT:   (block $block (result (ref any))
   ;; OPTIN-NEXT:    (drop
@@ -1652,7 +1652,7 @@
     )
   )
 
-  ;; CHECK:      (func $local-changes (type $3) (param $x i32) (param $y i32) (param $z i32)
+  ;; 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)
   ;; CHECK-NEXT:  )
@@ -1708,7 +1708,7 @@
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $local-changes (type $3) (param $x i32) (param $y i32) (param $z i32)
+  ;; OPTIN:      (func $local-changes (type $2) (param $x i32) (param $y i32) (param $z i32)
   ;; OPTIN-NEXT:  (local.set $x
   ;; OPTIN-NEXT:   (local.get $y)
   ;; OPTIN-NEXT:  )
@@ -1838,7 +1838,7 @@
     )
   )
 
-  ;; CHECK:      (func $local-changes-2 (type $3) (param $x i32) (param $y i32) (param $z i32)
+  ;; CHECK:      (func $local-changes-2 (type $2) (param $x i32) (param $y i32) (param $z i32)
   ;; CHECK-NEXT:  (local.set $x
   ;; CHECK-NEXT:   (local.get $y)
   ;; CHECK-NEXT:  )
@@ -1894,7 +1894,7 @@
   ;; CHECK-NEXT:   (i32.const 1)
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $local-changes-2 (type $3) (param $x i32) (param $y i32) (param $z i32)
+  ;; OPTIN:      (func $local-changes-2 (type $2) (param $x i32) (param $y i32) (param $z i32)
   ;; OPTIN-NEXT:  (local.set $x
   ;; OPTIN-NEXT:   (local.get $y)
   ;; OPTIN-NEXT:  )
@@ -2227,4 +2227,219 @@
       )
     )
   )
+
+  ;; CHECK:      (func $local-changes-ne (type $2) (param $x i32) (param $y i32) (param $z i32)
+  ;; CHECK-NEXT:  (if
+  ;; CHECK-NEXT:   (i32.ne
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (local.get $y)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (then
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.ne
+  ;; CHECK-NEXT:      (local.get $x)
+  ;; CHECK-NEXT:      (local.get $z)
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.ne
+  ;; CHECK-NEXT:      (local.get $z)
+  ;; CHECK-NEXT:      (local.get $x)
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (local.set $x
+  ;; CHECK-NEXT:     (local.get $z)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.ne
+  ;; CHECK-NEXT:      (local.get $x)
+  ;; CHECK-NEXT:      (local.get $y)
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.ne
+  ;; CHECK-NEXT:      (local.get $y)
+  ;; CHECK-NEXT:      (local.get $x)
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.ne
+  ;; CHECK-NEXT:      (local.get $x)
+  ;; CHECK-NEXT:      (local.get $z)
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.ne
+  ;; CHECK-NEXT:      (local.get $z)
+  ;; CHECK-NEXT:      (local.get $x)
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.ne
+  ;; CHECK-NEXT:      (local.get $y)
+  ;; CHECK-NEXT:      (local.get $z)
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.ne
+  ;; CHECK-NEXT:      (local.get $z)
+  ;; CHECK-NEXT:      (local.get $y)
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $local-changes-ne (type $2) (param $x i32) (param $y i32) (param $z i32)
+  ;; OPTIN-NEXT:  (if
+  ;; OPTIN-NEXT:   (i32.ne
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (local.get $y)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (then
+  ;; OPTIN-NEXT:    (drop
+  ;; OPTIN-NEXT:     (i32.const 1)
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:    (drop
+  ;; OPTIN-NEXT:     (i32.const 1)
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:    (drop
+  ;; OPTIN-NEXT:     (i32.ne
+  ;; OPTIN-NEXT:      (local.get $x)
+  ;; OPTIN-NEXT:      (local.get $z)
+  ;; OPTIN-NEXT:     )
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:    (drop
+  ;; OPTIN-NEXT:     (i32.ne
+  ;; OPTIN-NEXT:      (local.get $x)
+  ;; OPTIN-NEXT:      (local.get $z)
+  ;; OPTIN-NEXT:     )
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:    (local.set $x
+  ;; OPTIN-NEXT:     (local.get $z)
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:    (drop
+  ;; OPTIN-NEXT:     (i32.ne
+  ;; OPTIN-NEXT:      (local.get $x)
+  ;; OPTIN-NEXT:      (local.get $y)
+  ;; OPTIN-NEXT:     )
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:    (drop
+  ;; OPTIN-NEXT:     (i32.ne
+  ;; OPTIN-NEXT:      (local.get $x)
+  ;; OPTIN-NEXT:      (local.get $y)
+  ;; OPTIN-NEXT:     )
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:    (drop
+  ;; OPTIN-NEXT:     (i32.ne
+  ;; OPTIN-NEXT:      (local.get $x)
+  ;; OPTIN-NEXT:      (local.get $z)
+  ;; OPTIN-NEXT:     )
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:    (drop
+  ;; OPTIN-NEXT:     (i32.ne
+  ;; OPTIN-NEXT:      (local.get $x)
+  ;; OPTIN-NEXT:      (local.get $z)
+  ;; OPTIN-NEXT:     )
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:    (drop
+  ;; OPTIN-NEXT:     (i32.ne
+  ;; OPTIN-NEXT:      (local.get $y)
+  ;; OPTIN-NEXT:      (local.get $z)
+  ;; OPTIN-NEXT:     )
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:    (drop
+  ;; OPTIN-NEXT:     (i32.ne
+  ;; OPTIN-NEXT:      (local.get $y)
+  ;; OPTIN-NEXT:      (local.get $z)
+  ;; OPTIN-NEXT:     )
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $local-changes-ne (param $x i32) (param $y i32) (param $z i32)
+    ;; Similar to above, but testing != rather than ==
+    (if
+      (i32.ne
+        (local.get $x)
+        (local.get $y)
+      )
+      (then
+        ;; x == y is false, and we know nothing about z.
+        (drop
+          (i32.ne
+            (local.get $x)
+            (local.get $y)
+          )
+        )
+        (drop
+          (i32.ne
+            (local.get $y)
+            (local.get $x)
+          )
+        )
+        (drop
+          (i32.ne
+            (local.get $x)
+            (local.get $z)
+          )
+        )
+        (drop
+          (i32.ne
+            (local.get $z)
+            (local.get $x)
+          )
+        )
+
+        ;; Set x to z. Now x != z is false, but we can prove nothing about
+        ;; x and y.
+        (local.set $x
+          (local.get $z)
+        )
+        (drop
+          (i32.ne
+            (local.get $x)
+            (local.get $y)
+          )
+        )
+        (drop
+          (i32.ne
+            (local.get $y)
+            (local.get $x)
+          )
+        )
+        (drop
+          (i32.ne
+            (local.get $x)
+            (local.get $z)
+          )
+        )
+        (drop
+          (i32.ne
+            (local.get $z)
+            (local.get $x)
+          )
+        )
+
+        ;; No idea about y vs z.
+        (drop
+          (i32.ne
+            (local.get $y)
+            (local.get $z)
+          )
+        )
+        (drop
+          (i32.ne
+            (local.get $z)
+            (local.get $y)
+          )
+        )
+      )
+    )
+  )
 )

From 4f50ee33e1ba693539fa2521f3fab7ce7c893dc2 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 30 Jun 2026 12:51:22 -0700
Subject: [PATCH 15/20] work

---
 src/ir/constraint.cpp                    |  5 ++
 src/ir/constraint.h                      |  2 +-
 test/lit/passes/constraint-analysis.wast | 74 +++++-------------------
 3 files changed, 22 insertions(+), 59 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 326cdbaef71..1a5307068fa 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -64,6 +64,11 @@ Result provesPair(const Constraint& a, const Constraint& b) {
     return True;
   }
 
+  // A thing always implies its negation is false.
+  if (a == b.negate()) {
+    return False;
+  }
+
   // Comparisons of two constants.
   auto* aConstant = std::get_if<Literal>(&a.term);
   auto* bConstant = std::get_if<Literal>(&b.term);
diff --git a/src/ir/constraint.h b/src/ir/constraint.h
index f98fc56fa94..edaa308ca96 100644
--- a/src/ir/constraint.h
+++ b/src/ir/constraint.h
@@ -45,7 +45,7 @@ struct Constraint {
 
   bool operator==(const Constraint&) const = default;
 
-  Constraint negate() {
+  Constraint negate() const {
     return Constraint{Abstract::negateRelational(op), term};
   }
 };
diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index 2f04cb12b58..ce5d59afa7b 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -2236,7 +2236,7 @@
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:   (then
   ;; CHECK-NEXT:    (drop
-  ;; CHECK-NEXT:     (i32.const 1)
+  ;; CHECK-NEXT:     (i32.const 0)
   ;; CHECK-NEXT:    )
   ;; CHECK-NEXT:    (drop
   ;; CHECK-NEXT:     (i32.const 1)
@@ -2247,49 +2247,34 @@
   ;; CHECK-NEXT:      (local.get $z)
   ;; CHECK-NEXT:     )
   ;; CHECK-NEXT:    )
-  ;; CHECK-NEXT:    (drop
-  ;; CHECK-NEXT:     (i32.ne
-  ;; CHECK-NEXT:      (local.get $z)
-  ;; CHECK-NEXT:      (local.get $x)
-  ;; CHECK-NEXT:     )
-  ;; CHECK-NEXT:    )
   ;; CHECK-NEXT:    (local.set $x
   ;; CHECK-NEXT:     (local.get $z)
   ;; CHECK-NEXT:    )
   ;; CHECK-NEXT:    (drop
-  ;; CHECK-NEXT:     (i32.ne
+  ;; CHECK-NEXT:     (i32.eq
   ;; CHECK-NEXT:      (local.get $x)
   ;; CHECK-NEXT:      (local.get $y)
   ;; CHECK-NEXT:     )
   ;; CHECK-NEXT:    )
   ;; CHECK-NEXT:    (drop
   ;; CHECK-NEXT:     (i32.ne
-  ;; CHECK-NEXT:      (local.get $y)
   ;; CHECK-NEXT:      (local.get $x)
+  ;; CHECK-NEXT:      (local.get $y)
   ;; CHECK-NEXT:     )
   ;; CHECK-NEXT:    )
   ;; CHECK-NEXT:    (drop
-  ;; CHECK-NEXT:     (i32.ne
-  ;; CHECK-NEXT:      (local.get $x)
-  ;; CHECK-NEXT:      (local.get $z)
-  ;; CHECK-NEXT:     )
-  ;; CHECK-NEXT:    )
-  ;; CHECK-NEXT:    (drop
-  ;; CHECK-NEXT:     (i32.ne
-  ;; CHECK-NEXT:      (local.get $z)
-  ;; CHECK-NEXT:      (local.get $x)
-  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:     (i32.const 0)
   ;; CHECK-NEXT:    )
   ;; CHECK-NEXT:    (drop
-  ;; CHECK-NEXT:     (i32.ne
+  ;; CHECK-NEXT:     (i32.eq
   ;; CHECK-NEXT:      (local.get $y)
   ;; CHECK-NEXT:      (local.get $z)
   ;; CHECK-NEXT:     )
   ;; CHECK-NEXT:    )
   ;; CHECK-NEXT:    (drop
   ;; CHECK-NEXT:     (i32.ne
-  ;; CHECK-NEXT:      (local.get $z)
   ;; CHECK-NEXT:      (local.get $y)
+  ;; CHECK-NEXT:      (local.get $z)
   ;; CHECK-NEXT:     )
   ;; CHECK-NEXT:    )
   ;; CHECK-NEXT:   )
@@ -2303,7 +2288,7 @@
   ;; OPTIN-NEXT:   )
   ;; OPTIN-NEXT:   (then
   ;; OPTIN-NEXT:    (drop
-  ;; OPTIN-NEXT:     (i32.const 1)
+  ;; OPTIN-NEXT:     (i32.const 0)
   ;; OPTIN-NEXT:    )
   ;; OPTIN-NEXT:    (drop
   ;; OPTIN-NEXT:     (i32.const 1)
@@ -2314,17 +2299,11 @@
   ;; OPTIN-NEXT:      (local.get $z)
   ;; OPTIN-NEXT:     )
   ;; OPTIN-NEXT:    )
-  ;; OPTIN-NEXT:    (drop
-  ;; OPTIN-NEXT:     (i32.ne
-  ;; OPTIN-NEXT:      (local.get $x)
-  ;; OPTIN-NEXT:      (local.get $z)
-  ;; OPTIN-NEXT:     )
-  ;; OPTIN-NEXT:    )
   ;; OPTIN-NEXT:    (local.set $x
   ;; OPTIN-NEXT:     (local.get $z)
   ;; OPTIN-NEXT:    )
   ;; OPTIN-NEXT:    (drop
-  ;; OPTIN-NEXT:     (i32.ne
+  ;; OPTIN-NEXT:     (i32.eq
   ;; OPTIN-NEXT:      (local.get $x)
   ;; OPTIN-NEXT:      (local.get $y)
   ;; OPTIN-NEXT:     )
@@ -2336,19 +2315,10 @@
   ;; OPTIN-NEXT:     )
   ;; OPTIN-NEXT:    )
   ;; OPTIN-NEXT:    (drop
-  ;; OPTIN-NEXT:     (i32.ne
-  ;; OPTIN-NEXT:      (local.get $x)
-  ;; OPTIN-NEXT:      (local.get $z)
-  ;; OPTIN-NEXT:     )
-  ;; OPTIN-NEXT:    )
-  ;; OPTIN-NEXT:    (drop
-  ;; OPTIN-NEXT:     (i32.ne
-  ;; OPTIN-NEXT:      (local.get $x)
-  ;; OPTIN-NEXT:      (local.get $z)
-  ;; OPTIN-NEXT:     )
+  ;; OPTIN-NEXT:     (i32.const 0)
   ;; OPTIN-NEXT:    )
   ;; OPTIN-NEXT:    (drop
-  ;; OPTIN-NEXT:     (i32.ne
+  ;; OPTIN-NEXT:     (i32.eq
   ;; OPTIN-NEXT:      (local.get $y)
   ;; OPTIN-NEXT:      (local.get $z)
   ;; OPTIN-NEXT:     )
@@ -2372,15 +2342,15 @@
       (then
         ;; x == y is false, and we know nothing about z.
         (drop
-          (i32.ne
+          (i32.eq
             (local.get $x)
             (local.get $y)
           )
         )
         (drop
           (i32.ne
-            (local.get $y)
             (local.get $x)
+            (local.get $y)
           )
         )
         (drop
@@ -2389,12 +2359,6 @@
             (local.get $z)
           )
         )
-        (drop
-          (i32.ne
-            (local.get $z)
-            (local.get $x)
-          )
-        )
 
         ;; Set x to z. Now x != z is false, but we can prove nothing about
         ;; x and y.
@@ -2402,15 +2366,15 @@
           (local.get $z)
         )
         (drop
-          (i32.ne
+          (i32.eq
             (local.get $x)
             (local.get $y)
           )
         )
         (drop
           (i32.ne
-            (local.get $y)
             (local.get $x)
+            (local.get $y)
           )
         )
         (drop
@@ -2419,24 +2383,18 @@
             (local.get $z)
           )
         )
-        (drop
-          (i32.ne
-            (local.get $z)
-            (local.get $x)
-          )
-        )
 
         ;; No idea about y vs z.
         (drop
-          (i32.ne
+          (i32.eq
             (local.get $y)
             (local.get $z)
           )
         )
         (drop
           (i32.ne
-            (local.get $z)
             (local.get $y)
+            (local.get $z)
           )
         )
       )

From e2d04970131e39a2e420c2f0f2225e271617b69b Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 30 Jun 2026 12:56:20 -0700
Subject: [PATCH 16/20] work

---
 src/ir/constraint.h | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/ir/constraint.h b/src/ir/constraint.h
index edaa308ca96..e55ba20bfd8 100644
--- a/src/ir/constraint.h
+++ b/src/ir/constraint.h
@@ -227,7 +227,10 @@ struct BasicBlockConstraintMap {
   // Get the constraints for a local.
   AndedConstraintSet get(Index index) const {
     if (auto iter = map.find(index); iter != map.end()) {
-      return iter->second;
+      auto& constraints = iter->second;
+      // If we can prove nothing, we should have removed it from the map.
+      assert(!constraints.provesNothing());
+      return constraints;
     }
     return AndedConstraintSet::makeProvesNothing();
   }

From 8cc8c5f932d2ee250314cdc66f750cbe9cb23cd9 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 30 Jun 2026 12:57:22 -0700
Subject: [PATCH 17/20] work

---
 src/ir/constraint.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ir/constraint.h b/src/ir/constraint.h
index e55ba20bfd8..f485c46abd1 100644
--- a/src/ir/constraint.h
+++ b/src/ir/constraint.h
@@ -278,7 +278,7 @@ struct BasicBlockConstraintMap {
   // Internal version, with a flag to flip the constraint. Whenever we apply
   // e.g. x == y, we also apply y == x to y, to maintain the invariant described
   // above. When flip is true, we flip the constraint and apply it to the other
-  // index (y == x) in this example.
+  // index (y == x, in this example).
   void
   approximateAndInternal(Index index, const Constraint& c, bool flip = false);
 };

From 62a496fcd288c05ddd3dbd1c10fd04418d025b94 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 30 Jun 2026 12:57:35 -0700
Subject: [PATCH 18/20] work

---
 src/passes/ConstraintAnalysis.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/passes/ConstraintAnalysis.cpp b/src/passes/ConstraintAnalysis.cpp
index 257f0fd91bd..5c2fe99b875 100644
--- a/src/passes/ConstraintAnalysis.cpp
+++ b/src/passes/ConstraintAnalysis.cpp
@@ -306,7 +306,7 @@ struct ConstraintAnalysis
         auto value = Properties::getLiteral(set->value);
         constraints.set(set->index, Constraint{Abstract::Eq, {value}});
       } else if (auto* get = set->value->dynCast<LocalGet>()) {
-        // Apply a constraint to this local..
+        // Apply a constraint to this local.
         constraints.set(set->index, Constraint{Abstract::Eq, {get->index}});
       } else {
         // We know and can prove nothing.

From 32b873be2106a7d1675d534ba6067025692aa0ac Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Wed, 1 Jul 2026 08:12:52 -0700
Subject: [PATCH 19/20] add a flip helper

---
 src/ir/constraint.cpp | 26 ++++++++++++++++----------
 src/ir/constraint.h   |  4 ++++
 2 files changed, 20 insertions(+), 10 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 1a5307068fa..a1be14c6bf0 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -255,6 +255,18 @@ LocalConstraint::parseCondition(Expression* curr) {
   return parse(curr);
 };
 
+void LocalConstraint::flip() {
+  auto other = std::get<Index>(constraint.term);
+  constraint.term = Term{local};
+  local = other;
+  if (Abstract::isRelationalAntisymmetric(constraint.op)) {
+    constraint.op = Abstract::negateRelational(constraint.op);
+  } else {
+    // All we support for now are symmetric and antisymmetric operations.
+    assert(Abstract::isRelationalSymmetric(constraint.op));
+  }
+}
+
 void BasicBlockConstraintMap::set(Index index, const Constraint& c) {
   assert(!unreachable);
   eraseStaleRefs(index);
@@ -304,16 +316,10 @@ void BasicBlockConstraintMap::approximateAndInternal(Index index,
                                                      bool flip) {
   Constraint actual = c;
   if (flip) {
-    // Build a flipped constraint, referring to index.
-    auto otherIndex = std::get<Index>(actual.term);
-    actual.term = Term{index};
-    index = otherIndex;
-    if (Abstract::isRelationalAntisymmetric(actual.op)) {
-      actual.op = Abstract::negateRelational(actual.op);
-    } else {
-      // All we support for now are symmetric and antisymmetric operations.
-      assert(Abstract::isRelationalSymmetric(actual.op));
-    }
+    LocalConstraint flipped{index, c};
+    flipped.flip();
+    index = flipped.local;
+    actual = flipped.constraint;
   }
 
   auto combined = get(index);
diff --git a/src/ir/constraint.h b/src/ir/constraint.h
index f485c46abd1..6903fb66a5f 100644
--- a/src/ir/constraint.h
+++ b/src/ir/constraint.h
@@ -186,6 +186,10 @@ struct LocalConstraint {
   // Parse in a condition context, i.e., where (local.get $x) is the same as
   // $x != 0 (e.g., in an if condition, or a br_on ref).
   static std::optional<LocalConstraint> parseCondition(Expression* curr);
+
+  // Reverse the constraint. The constraint's term must, of course, be another
+  // local.
+  void flip();
 };
 
 // A map of locals and their constraints, representing the state at a basic

From 123c31b476c540b30dc32d9b0f3193f2df994935 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Wed, 1 Jul 2026 08:16:40 -0700
Subject: [PATCH 20/20] add suggested assert, and another

---
 src/ir/constraint.h | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/ir/constraint.h b/src/ir/constraint.h
index 6903fb66a5f..31a5dd04fed 100644
--- a/src/ir/constraint.h
+++ b/src/ir/constraint.h
@@ -230,10 +230,15 @@ struct BasicBlockConstraintMap {
 
   // Get the constraints for a local.
   AndedConstraintSet get(Index index) const {
+    // We should not be called in unreachable code.
+    assert(!unreachable);
+
     if (auto iter = map.find(index); iter != map.end()) {
       auto& constraints = iter->second;
       // If we can prove nothing, we should have removed it from the map.
       assert(!constraints.provesNothing());
+      // If we can prove everything, we should be entirely unreachable.
+      assert(!constraints.provesEverything());
       return constraints;
     }
     return AndedConstraintSet::makeProvesNothing();