From 9e3540e7b64013fdb32b558a33cda72279c750bf Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Mon, 24 Aug 2026 10:01:19 -0700
Subject: [PATCH 01/30] test

---
 test/gtest/constraint.cpp | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 47039f1ac0b..2112b3b677b 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -1042,3 +1042,30 @@ TEST(ConstraintTest, EmptySpanContradiction) {
   AndedConstraintSet impossible{gtsMax32};
   checkOr(valid, impossible, valid);
 }
+
+TEST(ConstraintTest, SignedUnsigned) {
+  // x == 5 proves x < 10, signed or unsigned.
+  Constraint eq5{Eq, {Literal(int32_t(5))}};
+  Constraint lts10{LtS, {Literal(int32_t(10))}};
+  Constraint ltu10{LtU, {Literal(int32_t(10))}};
+  EXPECT_EQ(AndedConstraintSet{eq5}.proves(lts10), True);
+  EXPECT_EQ(AndedConstraintSet{eq5}.proves(ltu10), True);
+
+  // x == 5 proves x < -10 signed is false, but unsigned is true (since -10 is
+  // a very large positive number).
+  Constraint lts_minus10{LtS, {Literal(int32_t(-10))}};
+  Constraint ltu_minus10{LtU, {Literal(int32_t(-10))}};
+  EXPECT_EQ(AndedConstraintSet{eq5}.proves(lts_minus10), False);
+  EXPECT_EQ(AndedConstraintSet{eq5}.proves(ltu_minus10), True);
+}
+
+TEST(ConstraintTest, SignedUnsignedMix) {
+  // x < 10, signed and the same but unsigned, have some overlap (0 to 10) but
+  // the signed version has more possible values.
+  Constraint lts10{LtS, {Literal(int32_t(10))}};
+  Constraint ltu10{LtU, {Literal(int32_t(10))}};
+  // x might be negative, which would not prove x < 10 unsigned.
+  EXPECT_EQ(AndedConstraintSet{lts10}.proves(ltu10), Unknown);
+  // x is definitely in [0, 10], so x < 10 signed is also true.
+  EXPECT_EQ(AndedConstraintSet{ltu10}.proves(lts10), True);
+}

From a32c080ac8f8fa8e7590f6842f9593bfab6bec6b Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Mon, 24 Aug 2026 10:04:47 -0700
Subject: [PATCH 02/30] test

---
 test/gtest/constraint.cpp | 58 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 58 insertions(+)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 2112b3b677b..fceeebcc59c 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -1068,4 +1068,62 @@ TEST(ConstraintTest, SignedUnsignedMix) {
   EXPECT_EQ(AndedConstraintSet{lts10}.proves(ltu10), Unknown);
   // x is definitely in [0, 10], so x < 10 signed is also true.
   EXPECT_EQ(AndedConstraintSet{ltu10}.proves(lts10), True);
+
+  // Now with -10 instead of 10.
+  Constraint lts_minus10{LtS, {Literal(int32_t(-10))}};
+  Constraint ltu_minus10{LtU, {Literal(int32_t(-10))}};
+  // x < -10 signed means all the numbers with the high/sign bit set, except for
+  // -1 to -10 (which are the very highest in unsigned terms).
+  EXPECT_EQ(AndedConstraintSet{lts_minus10}.proves(ltu_minus10), Unknown);
+
 }
+
+/*
+(module $a.wasm
+ (func $scalbn (param $0 i32)
+  (local $1 f64)
+  (local.set $1
+   (f64.const 1)
+  )
+  (block $block
+   (br_if $block
+    (i32.ge_s
+     (local.get $0)
+     (i32.const 1024)
+    )
+   )
+   ;; Here we know  $0 <_s 1024. This includes all numbers with the sign bit,
+   ;; which implies the following *unsigned* inequality is true, as it
+   ;; includes only ones with the high bit set.
+   (drop
+    (i32.gt_u
+     (local.get $0)
+     (i32.const -1992)
+    )
+   )
+  )
+ )
+
+ (func $scalbn2 (param $0 i32)
+  (local $1 f64)
+  (local.set $1
+   (f64.const 1)
+  )
+  (block $block
+   (br_if $block
+    (i32.gt_s
+     (local.get $0)
+     (i32.const -1023)
+    )
+   )
+   ;; Here we know  $0 <=_s -1023
+   (drop
+    (i32.gt_u
+     (local.get $0)
+     (i32.const -1992)
+    )
+   )
+  )
+ )
+)*/
+

From 8783222a393ce3cc33626ef7449d64061a47c27a Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Mon, 24 Aug 2026 12:44:08 -0700
Subject: [PATCH 03/30] test

---
 test/gtest/constraint.cpp | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index fceeebcc59c..260a5b48865 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -1073,9 +1073,18 @@ TEST(ConstraintTest, SignedUnsignedMix) {
   Constraint lts_minus10{LtS, {Literal(int32_t(-10))}};
   Constraint ltu_minus10{LtU, {Literal(int32_t(-10))}};
   // x < -10 signed means all the numbers with the high/sign bit set, except for
-  // -1 to -10 (which are the very highest in unsigned terms).
-  EXPECT_EQ(AndedConstraintSet{lts_minus10}.proves(ltu_minus10), Unknown);
+  // -1 to -10 (which are the very highest in unsigned terms), that is,
+  // [1, large number] in the unsigned representation of bits. x < -10
+  // *un*signed is similar, but *does* include 0, so the unsigned one does not
+  // prove the signed.
+  EXPECT_EQ(AndedConstraintSet{lts_minus10}.proves(ltu_minus10), True);
+  EXPECT_EQ(AndedConstraintSet{ltu_minus10}.proves(lts_minus10), Unknown);
 
+  // gt rather than lt for all the above
+
+  // -20 vs -10, not -10/-10
+
+  // mixtures of gt_s lt_u (not just signed/unsigned but gt/lt)
 }
 
 /*

From 4a43de9a925d111c5a292f81fa79cbe5d845cc43 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 09:24:24 -0700
Subject: [PATCH 04/30] test

---
 test/gtest/constraint.cpp | 24 +++++++++++++++++++++---
 1 file changed, 21 insertions(+), 3 deletions(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 260a5b48865..8fa9970c0e7 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -1059,7 +1059,7 @@ TEST(ConstraintTest, SignedUnsigned) {
   EXPECT_EQ(AndedConstraintSet{eq5}.proves(ltu_minus10), True);
 }
 
-TEST(ConstraintTest, SignedUnsignedMix) {
+TEST(ConstraintTest, SignedUnsignedLessMix) {
   // x < 10, signed and the same but unsigned, have some overlap (0 to 10) but
   // the signed version has more possible values.
   Constraint lts10{LtS, {Literal(int32_t(10))}};
@@ -1080,9 +1080,27 @@ TEST(ConstraintTest, SignedUnsignedMix) {
   EXPECT_EQ(AndedConstraintSet{lts_minus10}.proves(ltu_minus10), True);
   EXPECT_EQ(AndedConstraintSet{ltu_minus10}.proves(lts_minus10), Unknown);
 
-  // gt rather than lt for all the above
+  // x < -10 signed means all numbers with the high bit set, except for the very
+  // highest. This rules out x < 10 unsigned.
+  EXPECT_EQ(AndedConstraintSet{lts_minus10}.proves(ltu10), False);
+  // x < 10 signed means all numbers with the sign bit, and 0..10. This has
+  // partial overlap with x < -10 unsigned.
+  EXPECT_EQ(AndedConstraintSet{lts10}.proves(ltu_minus10), Unknown);
+
+  // Flip cases of the above pair.
+  EXPECT_EQ(AndedConstraintSet{ltu_minus10}.proves(lts10), Unknown);
+  EXPECT_EQ(AndedConstraintSet{ltu10}.proves(lts_minus10), False);
+}
 
-  // -20 vs -10, not -10/-10
+TEST(ConstraintTest, SignedUnsignedMoreMix) {
+  // x > 10, signed and the same but unsigned. The signed version does not
+  // include numbers with the highest bit set.
+  Constraint gts10{GtS, {Literal(int32_t(10))}};
+  Constraint gtu10{GtU, {Literal(int32_t(10))}};
+  EXPECT_EQ(AndedConstraintSet{gts10}.proves(gtu10), True);
+  EXPECT_EQ(AndedConstraintSet{gtu10}.proves(gts10), Unknown);
+
+  // gt rather than lt for all the above
 
   // mixtures of gt_s lt_u (not just signed/unsigned but gt/lt)
 }

From 8616b1113d8716d316c6104b7f913f362ce9794f Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 09:27:39 -0700
Subject: [PATCH 05/30] test

---
 test/gtest/constraint.cpp | 65 +++++++++------------------------------
 1 file changed, 14 insertions(+), 51 deletions(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 8fa9970c0e7..15c04efebd8 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -1100,57 +1100,20 @@ TEST(ConstraintTest, SignedUnsignedMoreMix) {
   EXPECT_EQ(AndedConstraintSet{gts10}.proves(gtu10), True);
   EXPECT_EQ(AndedConstraintSet{gtu10}.proves(gts10), Unknown);
 
-  // gt rather than lt for all the above
-
-  // mixtures of gt_s lt_u (not just signed/unsigned but gt/lt)
+  // TODO: add negative cases
 }
 
-/*
-(module $a.wasm
- (func $scalbn (param $0 i32)
-  (local $1 f64)
-  (local.set $1
-   (f64.const 1)
-  )
-  (block $block
-   (br_if $block
-    (i32.ge_s
-     (local.get $0)
-     (i32.const 1024)
-    )
-   )
-   ;; Here we know  $0 <_s 1024. This includes all numbers with the sign bit,
-   ;; which implies the following *unsigned* inequality is true, as it
-   ;; includes only ones with the high bit set.
-   (drop
-    (i32.gt_u
-     (local.get $0)
-     (i32.const -1992)
-    )
-   )
-  )
- )
-
- (func $scalbn2 (param $0 i32)
-  (local $1 f64)
-  (local.set $1
-   (f64.const 1)
-  )
-  (block $block
-   (br_if $block
-    (i32.gt_s
-     (local.get $0)
-     (i32.const -1023)
-    )
-   )
-   ;; Here we know  $0 <=_s -1023
-   (drop
-    (i32.gt_u
-     (local.get $0)
-     (i32.const -1992)
-    )
-   )
-  )
- )
-)*/
+TEST(ConstraintTest, SignedUnsignedLessAndMoreMix) {
+  // Use > and < together.
+  Constraint lts10{LtS, {Literal(int32_t(10))}};
+  Constraint ltu10{LtU, {Literal(int32_t(10))}};
+  Constraint gts10{GtS, {Literal(int32_t(10))}};
+  Constraint gtu10{GtU, {Literal(int32_t(10))}};
+
+  EXPECT_EQ(AndedConstraintSet{lts10}.proves(gtu10), Unknown);
+  EXPECT_EQ(AndedConstraintSet{ltu10}.proves(gts10), False);
+  EXPECT_EQ(AndedConstraintSet{gts10}.proves(ltu10), False);
+  EXPECT_EQ(AndedConstraintSet{gtu10}.proves(lts10), Unknown);
 
+  // TODO: add negative cases
+}

From 9e3b412e9ef7987c2e98e2a8ad9cba38b243f31b Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 09:46:48 -0700
Subject: [PATCH 06/30] test

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

diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index 6f04d3c882a..a2781211435 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -4733,4 +4733,100 @@
       )
     )
   )
+
+  ;; CHECK:      (func $sign-unsigned-less-more-mix (type $0) (param $0 i32)
+  ;; CHECK-NEXT:  (block $block
+  ;; CHECK-NEXT:   (br_if $block
+  ;; CHECK-NEXT:    (i32.ge_s
+  ;; CHECK-NEXT:     (local.get $0)
+  ;; CHECK-NEXT:     (i32.const 1024)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (drop
+  ;; CHECK-NEXT:    (i32.const 0)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $sign-unsigned-less-more-mix (type $0) (param $0 i32)
+  ;; OPTIN-NEXT:  (block $block
+  ;; OPTIN-NEXT:   (br_if $block
+  ;; OPTIN-NEXT:    (i32.ge_s
+  ;; OPTIN-NEXT:     (local.get $0)
+  ;; OPTIN-NEXT:     (i32.const 1024)
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (drop
+  ;; OPTIN-NEXT:    (i32.const 0)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $sign-unsigned-less-more-mix (param $0 i32)
+    (block $block
+      (br_if $block
+        (i32.ge_s
+          (local.get $0)
+          (i32.const 1024)
+        )
+      )
+      ;; Here we know  $0 <_s 1024. This includes all numbers with the sign bit,
+      ;; which implies the following *unsigned* inequality is true, as it
+      ;; includes only ones with the high bit set.
+      ;; XXX FIXME the result is wrong atm
+      (drop
+        (i32.gt_u
+          (local.get $0)
+          (i32.const -1992)
+        )
+      )
+    )
+  )
+
+  ;; CHECK:      (func $sign-unsigned-less-more-mix-2 (type $0) (param $0 i32)
+  ;; CHECK-NEXT:  (block $block
+  ;; CHECK-NEXT:   (br_if $block
+  ;; CHECK-NEXT:    (i32.gt_s
+  ;; CHECK-NEXT:     (local.get $0)
+  ;; CHECK-NEXT:     (i32.const -1023)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (drop
+  ;; CHECK-NEXT:    (i32.const 0)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $sign-unsigned-less-more-mix-2 (type $0) (param $0 i32)
+  ;; OPTIN-NEXT:  (block $block
+  ;; OPTIN-NEXT:   (br_if $block
+  ;; OPTIN-NEXT:    (i32.gt_s
+  ;; OPTIN-NEXT:     (local.get $0)
+  ;; OPTIN-NEXT:     (i32.const -1023)
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (drop
+  ;; OPTIN-NEXT:    (i32.const 0)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $sign-unsigned-less-more-mix-2 (param $0 i32)
+    ;; Similar to the above, but the 1024 was replaced by -1023.
+    (block $block
+      (br_if $block
+        (i32.gt_s
+          (local.get $0)
+         (i32.const -1023) ;; this changed
+        )
+      )
+      ;; Here we know  $0 <=_s -1023. This includes most numbers with the sign
+      ;; bit set, except for the lowest in absolute value. That implies the
+      ;; following *unsigned* inequality might or might not true, so we optimize
+      ;; nothing.
+      ;; XXX FIXME the result is wrong atm
+      (drop
+        (i32.gt_u
+          (local.get $0)
+          (i32.const -1992)
+        )
+      )
+    )
+  )
 )

From f4e96115d81a3c75632e84d99100dc9ebcfe9a36 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 10:10:02 -0700
Subject: [PATCH 07/30] test

---
 src/support/iu64.h  | 152 --------------------------
 src/support/span.h  |  61 +++++++++++
 test/gtest/iu64.cpp | 258 --------------------------------------------
 3 files changed, 61 insertions(+), 410 deletions(-)
 delete mode 100644 src/support/iu64.h
 delete mode 100644 test/gtest/iu64.cpp

diff --git a/src/support/iu64.h b/src/support/iu64.h
deleted file mode 100644
index b91666560c8..00000000000
--- a/src/support/iu64.h
+++ /dev/null
@@ -1,152 +0,0 @@
-/*
- * 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.
- */
-
-#ifndef wasm_support_i65_h
-#define wasm_support_i65_h
-
-#include <cstdint>
-#include <iostream>
-#include <limits>
-
-namespace wasm {
-
-// An integer capable of representing numbers in the combined range of 32 and
-// 64-bit integers, both signed and unsigned. That is, in the range
-//
-//  std::numeric_limits<int64_t>::min() .. std::numeric_limits<uint64_t>::max()
-//
-// This is basically an i64 combined with a u64 in terms of range, hence "IU64".
-struct IU64 {
-  // A 64-bit payload with an extra 65th sign bit.
-  uint64_t value = 0;
-  bool negative = false;
-
-  constexpr IU64() = default;
-
-  // Unsigned values are simple.
-  constexpr IU64(uint32_t x) : value(x) {}
-  constexpr IU64(uint64_t x) : value(x) {}
-
-  // Signed values need to be checked for being negative.
-  constexpr IU64(int32_t x) {
-    if (x >= 0) {
-      value = x;
-    } else {
-      negative = true;
-      value = -int64_t(x);
-    }
-  }
-  constexpr IU64(int64_t x) {
-    if (x >= 0) {
-      value = x;
-    } else {
-      negative = true;
-
-      // One does not simply negate MIN_INT64.
-      if (x == std::numeric_limits<int64_t>::min()) {
-        value = uint64_t(1) << 63;
-      } else {
-        value = -int64_t(x);
-      }
-    }
-  }
-
-  constexpr bool operator==(const IU64& other) const {
-    return value == other.value && negative == other.negative;
-  }
-  constexpr bool operator!=(const IU64& other) const {
-    return !(*this == other);
-  }
-
-  constexpr bool operator<(const IU64& other) const {
-    if (negative) {
-      if (other.negative) {
-        // Both negative; we are smaller if absolute value is larger.
-        return value > other.value;
-      } else {
-        // Only we are negative, so we are smaller.
-        return true;
-      }
-    } else {
-      if (other.negative) {
-        // Only the other is negative, so we are larger.
-        return false;
-      } else {
-        // Both positive; we are smaller if absolute value is smaller.
-        return value < other.value;
-      }
-    }
-  }
-  constexpr bool operator<=(const IU64& other) const {
-    return *this < other || *this == other;
-  }
-  constexpr bool operator>(const IU64& other) const {
-    return !(*this <= other);
-  }
-  constexpr bool operator>=(const IU64& other) const {
-    return !(*this < other);
-  }
-};
-
-inline std::ostream& operator<<(std::ostream& os, const IU64& x) {
-  if (x.negative) {
-    os << '-';
-  }
-  return os << x.value;
-}
-
-} // namespace wasm
-
-namespace std {
-
-template<> class numeric_limits<wasm::IU64> {
-public:
-  static constexpr bool is_specialized = true;
-  static constexpr bool is_signed = true;
-  static constexpr bool is_integer = true;
-  static constexpr bool is_exact = true;
-  static constexpr bool has_infinity = false;
-  static constexpr bool has_quiet_NaN = false;
-  static constexpr bool has_signaling_NaN = false;
-  static constexpr float_denorm_style has_denorm = denorm_absent;
-  static constexpr bool has_denorm_loss = false;
-  static constexpr float_round_style round_style = round_toward_zero;
-  static constexpr bool is_iec559 = false;
-  static constexpr bool is_bounded = true;
-  static constexpr bool is_modulo = false;
-  static constexpr int digits = 65;
-  static constexpr int digits10 = 19;
-  static constexpr int max_digits10 = 0;
-  static constexpr int radix = 2;
-  static constexpr int min_exponent = 0;
-  static constexpr int min_exponent10 = 0;
-  static constexpr int max_exponent = 0;
-  static constexpr int max_exponent10 = 0;
-  static constexpr bool traps = false;
-  static constexpr bool tinyness_before = false;
-
-  static constexpr wasm::IU64 min() noexcept {
-    return wasm::IU64(std::numeric_limits<int64_t>::min());
-  }
-  static constexpr wasm::IU64 lowest() noexcept { return min(); }
-  static constexpr wasm::IU64 max() noexcept {
-    return wasm::IU64(std::numeric_limits<uint64_t>::max());
-  }
-};
-
-} // namespace std
-
-#endif // wasm_support_i65_h
diff --git a/src/support/span.h b/src/support/span.h
index 05cdbce65a9..50575228282 100644
--- a/src/support/span.h
+++ b/src/support/span.h
@@ -22,6 +22,8 @@
 #include <iostream>
 #include <limits>
 
+#include "support/inplace_vector.h"
+
 namespace wasm {
 
 // A span of values.
@@ -87,6 +89,65 @@ template<typename T> struct Span {
   bool operator!=(const Span& other) const { return !(*this == other); }
 };
 
+// A union of spans
+template<typename T, size_t N> struct Spans {
+  inplace_vector<Span<T>, N> spans;
+
+  static constexpr T Min = std::numeric_limits<T>::lowest();
+  static constexpr T Max = std::numeric_limits<T>::max();
+
+  T min = Min;
+  T max = Max;
+
+  constexpr Spans() = default;
+  Spans(std::initializer_list<Span<T>> init) {
+    for (auto& span : init) {
+      spans.push_back(span);
+    }
+  }
+
+  Spans<T, N> intersection(const Spans<T, N>& other) const {
+    // (s1 U s2) ^ (s3 U s4) == (s1 ^ (s3 U s4)) U (s2 ^ (s3 U s4)) etc.
+    Spans<T, N> ret;
+    for (auto& span : *this) {
+      // Starting from span, intersect it with other's spans, and unify those.
+      // This must end up a single span, as we assume other's spans are
+      // disjoint. XXX
+      auto curr = Span<T>::empty();
+      for (auto& otherSpan : other) {
+        curr
+    if (isEmpty() || other.isEmpty()) {
+      return empty();
+    }
+    return Span<T>{std::max(min, other.min), std::min(max, other.max)};
+  }
+
+  // Checks whether two spans have any overlap at all.
+  bool hasOverlap(const Spans<T, N>& other) const {
+    return !intersection(other).isEmpty();
+  }
+
+  // Check whether we contain another span (possibly being equal).
+  bool contains(const Spans<T, N>& other) const {
+    return intersection(other) == other;
+  }
+
+  bool operator==(const Spans<T, N>& other) const {
+    if (isEmpty()) {
+      return other.isEmpty();
+    }
+    return !other.isEmpty() && min == other.min && max == other.max;
+  }
+  bool operator!=(const Spans<T, N>& other) const { return !(*this == other); }
+
+};
+
+// A useful set of 2 spans that can contain any integer value. 2 spans is enough
+// to contain spans for any inequality, signed or unsigned: we represent numbers
+// as unsigned internally, and so e.g. signed x < 10 ends up as two disjoint
+// spans, [0..10] and [2^32..MAX_INT].
+using Spans2 = Spans<uint64_t, 2>;
+
 template<typename T>
 inline std::ostream& operator<<(std::ostream& os, const Span<T>& span) {
   if (span.isEmpty()) {
diff --git a/test/gtest/iu64.cpp b/test/gtest/iu64.cpp
deleted file mode 100644
index 1f812e9f8a3..00000000000
--- a/test/gtest/iu64.cpp
+++ /dev/null
@@ -1,258 +0,0 @@
-/*
- * 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 <cstdint>
-#include <limits>
-#include <sstream>
-#include <vector>
-
-#include "support/iu64.h"
-#include "gtest/gtest.h"
-
-using namespace wasm;
-
-TEST(IU64Test, DefaultConstruct) {
-  IU64 x;
-  EXPECT_EQ(x.value, 0u);
-  EXPECT_FALSE(x.negative);
-  EXPECT_EQ(x, IU64(0));
-}
-
-TEST(IU64Test, ConstructFromUnsigned32) {
-  uint32_t zero = 0;
-  uint32_t one = 1;
-  uint32_t mid = 12345678;
-  uint32_t maxU32 = std::numeric_limits<uint32_t>::max();
-
-  IU64 iZero(zero);
-  EXPECT_EQ(iZero.value, 0u);
-  EXPECT_FALSE(iZero.negative);
-
-  IU64 iOne(one);
-  EXPECT_EQ(iOne.value, 1u);
-  EXPECT_FALSE(iOne.negative);
-
-  IU64 iMid(mid);
-  EXPECT_EQ(iMid.value, mid);
-  EXPECT_FALSE(iMid.negative);
-
-  IU64 iMax(maxU32);
-  EXPECT_EQ(iMax.value, uint64_t(maxU32));
-  EXPECT_FALSE(iMax.negative);
-}
-
-TEST(IU64Test, ConstructFromSigned32) {
-  int32_t zero = 0;
-  int32_t one = 1;
-  int32_t maxI32 = std::numeric_limits<int32_t>::max();
-  int32_t negOne = -1;
-  int32_t negMid = -12345678;
-  int32_t minI32 = std::numeric_limits<int32_t>::min();
-
-  IU64 iZero(zero);
-  EXPECT_EQ(iZero.value, 0u);
-  EXPECT_FALSE(iZero.negative);
-
-  IU64 iOne(one);
-  EXPECT_EQ(iOne.value, 1u);
-  EXPECT_FALSE(iOne.negative);
-
-  IU64 iMax(maxI32);
-  EXPECT_EQ(iMax.value, uint64_t(maxI32));
-  EXPECT_FALSE(iMax.negative);
-
-  IU64 iNegOne(negOne);
-  EXPECT_EQ(iNegOne.value, 1u);
-  EXPECT_TRUE(iNegOne.negative);
-
-  IU64 iNegMid(negMid);
-  EXPECT_EQ(iNegMid.value, 12345678u);
-  EXPECT_TRUE(iNegMid.negative);
-
-  IU64 iMin(minI32);
-  EXPECT_EQ(iMin.value, 2147483648ULL);
-  EXPECT_TRUE(iMin.negative);
-}
-
-TEST(IU64Test, ConstructFromUnsigned64) {
-  uint64_t zero = 0;
-  uint64_t one = 1;
-  uint64_t maxU32 = std::numeric_limits<uint32_t>::max();
-  uint64_t maxI64 = std::numeric_limits<int64_t>::max();
-  uint64_t highBitOnly = uint64_t(1) << 63;
-  uint64_t maxU64 = std::numeric_limits<uint64_t>::max();
-
-  IU64 iZero(zero);
-  EXPECT_EQ(iZero.value, 0u);
-  EXPECT_FALSE(iZero.negative);
-
-  IU64 iOne(one);
-  EXPECT_EQ(iOne.value, 1u);
-  EXPECT_FALSE(iOne.negative);
-
-  IU64 iMaxU32(maxU32);
-  EXPECT_EQ(iMaxU32.value, maxU32);
-  EXPECT_FALSE(iMaxU32.negative);
-
-  IU64 iMaxI64(maxI64);
-  EXPECT_EQ(iMaxI64.value, maxI64);
-  EXPECT_FALSE(iMaxI64.negative);
-
-  IU64 iHighBit(highBitOnly);
-  EXPECT_EQ(iHighBit.value, highBitOnly);
-  EXPECT_FALSE(iHighBit.negative);
-
-  IU64 iMaxU64(maxU64);
-  EXPECT_EQ(iMaxU64.value, maxU64);
-  EXPECT_FALSE(iMaxU64.negative);
-}
-
-TEST(IU64Test, ConstructFromSigned64) {
-  int64_t zero = 0;
-  int64_t one = 1;
-  int64_t maxI64 = std::numeric_limits<int64_t>::max();
-  int64_t negOne = -1;
-  int64_t minI64 = std::numeric_limits<int64_t>::min();
-  int64_t minI64PlusOne = std::numeric_limits<int64_t>::min() + 1;
-
-  IU64 iZero(zero);
-  EXPECT_EQ(iZero.value, 0u);
-  EXPECT_FALSE(iZero.negative);
-
-  IU64 iOne(one);
-  EXPECT_EQ(iOne.value, 1u);
-  EXPECT_FALSE(iOne.negative);
-
-  IU64 iMax(maxI64);
-  EXPECT_EQ(iMax.value, uint64_t(maxI64));
-  EXPECT_FALSE(iMax.negative);
-
-  IU64 iNegOne(negOne);
-  EXPECT_EQ(iNegOne.value, 1u);
-  EXPECT_TRUE(iNegOne.negative);
-
-  IU64 iMin(minI64);
-  EXPECT_EQ(iMin.value, uint64_t(1) << 63);
-  EXPECT_TRUE(iMin.negative);
-
-  IU64 iMinPlusOne(minI64PlusOne);
-  EXPECT_EQ(iMinPlusOne.value, uint64_t(std::numeric_limits<int64_t>::max()));
-  EXPECT_TRUE(iMinPlusOne.negative);
-}
-
-TEST(IU64Test, EqualityAndInequality) {
-  EXPECT_EQ(IU64(int32_t(0)), IU64(uint32_t(0)));
-  EXPECT_EQ(IU64(int32_t(0)), IU64(int64_t(0)));
-  EXPECT_EQ(IU64(int32_t(0)), IU64(uint64_t(0)));
-
-  EXPECT_EQ(IU64(int32_t(42)), IU64(uint32_t(42)));
-  EXPECT_EQ(IU64(int32_t(42)), IU64(int64_t(42)));
-  EXPECT_EQ(IU64(int32_t(42)), IU64(uint64_t(42)));
-
-  EXPECT_EQ(IU64(int32_t(-42)), IU64(int64_t(-42)));
-  EXPECT_EQ(IU64(std::numeric_limits<int32_t>::min()),
-            IU64(int64_t(std::numeric_limits<int32_t>::min())));
-
-  EXPECT_NE(IU64(int32_t(1)), IU64(int32_t(-1)));
-  EXPECT_NE(IU64(uint64_t(0xffffffffffffffffULL)), IU64(int64_t(-1)));
-  EXPECT_NE(IU64(std::numeric_limits<int64_t>::min()), IU64(uint64_t(1) << 63));
-}
-
-TEST(IU64Test, TotalOrdering) {
-  std::vector<IU64> sortedValues = {
-    IU64(std::numeric_limits<int64_t>::min()),
-    IU64(std::numeric_limits<int64_t>::min() + 1),
-    IU64(int64_t(-0x100000000LL)),
-    IU64(std::numeric_limits<int32_t>::min()),
-    IU64(int32_t(-12345)),
-    IU64(int64_t(-2)),
-    IU64(int64_t(-1)),
-    IU64(0),
-    IU64(1),
-    IU64(2),
-    IU64(int32_t(12345)),
-    IU64(std::numeric_limits<int32_t>::max()),
-    IU64(uint64_t(std::numeric_limits<int32_t>::max()) + 1),
-    IU64(std::numeric_limits<uint32_t>::max()),
-    IU64(uint64_t(std::numeric_limits<uint32_t>::max()) + 1),
-    IU64(std::numeric_limits<int64_t>::max() - 1),
-    IU64(std::numeric_limits<int64_t>::max()),
-    IU64(uint64_t(std::numeric_limits<int64_t>::max()) + 1),
-    IU64(std::numeric_limits<uint64_t>::max() - 1),
-    IU64(std::numeric_limits<uint64_t>::max()),
-  };
-
-  for (size_t i = 0; i < sortedValues.size(); ++i) {
-    for (size_t j = 0; j < sortedValues.size(); ++j) {
-      const auto& a = sortedValues[i];
-      const auto& b = sortedValues[j];
-
-      if (i < j) {
-        EXPECT_LT(a, b);
-        EXPECT_LE(a, b);
-        EXPECT_GT(b, a);
-        EXPECT_GE(b, a);
-        EXPECT_NE(a, b);
-        EXPECT_FALSE(a == b);
-        EXPECT_FALSE(b < a);
-      } else if (i == j) {
-        EXPECT_EQ(a, b);
-        EXPECT_LE(a, b);
-        EXPECT_GE(a, b);
-        EXPECT_FALSE(a < b);
-        EXPECT_FALSE(a > b);
-        EXPECT_FALSE(a != b);
-      } else {
-        EXPECT_GT(a, b);
-        EXPECT_GE(a, b);
-        EXPECT_LT(b, a);
-        EXPECT_LE(b, a);
-        EXPECT_NE(a, b);
-        EXPECT_FALSE(a == b);
-        EXPECT_FALSE(a < b);
-      }
-    }
-  }
-}
-
-TEST(IU64Test, NumericLimits) {
-  EXPECT_TRUE(std::numeric_limits<IU64>::is_specialized);
-  EXPECT_TRUE(std::numeric_limits<IU64>::is_signed);
-  EXPECT_TRUE(std::numeric_limits<IU64>::is_integer);
-
-  EXPECT_EQ(std::numeric_limits<IU64>::min(),
-            IU64(std::numeric_limits<int64_t>::min()));
-  EXPECT_EQ(std::numeric_limits<IU64>::lowest(),
-            IU64(std::numeric_limits<int64_t>::min()));
-  EXPECT_EQ(std::numeric_limits<IU64>::max(),
-            IU64(std::numeric_limits<uint64_t>::max()));
-}
-
-TEST(IU64Test, StreamOutput) {
-  auto toString = [](const IU64& x) {
-    std::ostringstream ss;
-    ss << x;
-    return ss.str();
-  };
-
-  EXPECT_EQ(toString(IU64(0)), "0");
-  EXPECT_EQ(toString(IU64(42)), "42");
-  EXPECT_EQ(toString(IU64(-42)), "-42");
-  EXPECT_EQ(toString(IU64(std::numeric_limits<int64_t>::min())),
-            "-9223372036854775808");
-  EXPECT_EQ(toString(IU64(std::numeric_limits<uint64_t>::max())),
-            "18446744073709551615");
-}

From cf37883e34e317ffbb666ac52183e25e034d7ec1 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 11:34:28 -0700
Subject: [PATCH 08/30] test

---
 src/support/span.h | 34 ++++++----------------------------
 1 file changed, 6 insertions(+), 28 deletions(-)

diff --git a/src/support/span.h b/src/support/span.h
index 50575228282..a3126cea16a 100644
--- a/src/support/span.h
+++ b/src/support/span.h
@@ -106,47 +106,25 @@ template<typename T, size_t N> struct Spans {
     }
   }
 
-  Spans<T, N> intersection(const Spans<T, N>& other) const {
-    // (s1 U s2) ^ (s3 U s4) == (s1 ^ (s3 U s4)) U (s2 ^ (s3 U s4)) etc.
-    Spans<T, N> ret;
-    for (auto& span : *this) {
-      // Starting from span, intersect it with other's spans, and unify those.
-      // This must end up a single span, as we assume other's spans are
-      // disjoint. XXX
-      auto curr = Span<T>::empty();
-      for (auto& otherSpan : other) {
-        curr
-    if (isEmpty() || other.isEmpty()) {
-      return empty();
-    }
-    return Span<T>{std::max(min, other.min), std::min(max, other.max)};
-  }
-
-  // Checks whether two spans have any overlap at all.
   bool hasOverlap(const Spans<T, N>& other) const {
-    return !intersection(other).isEmpty();
+    return std::any_of(spans.begin(), spans.end(), [](const Span<T>& span) {
+      return std::any_of(other.spans.begin(), other.spans.end(), [](const Span<T>& otherSpan) {
+        return span.hasOverlap(otherSpan);
+      }
+    });
   }
 
   // Check whether we contain another span (possibly being equal).
   bool contains(const Spans<T, N>& other) const {
     return intersection(other) == other;
   }
-
-  bool operator==(const Spans<T, N>& other) const {
-    if (isEmpty()) {
-      return other.isEmpty();
-    }
-    return !other.isEmpty() && min == other.min && max == other.max;
-  }
-  bool operator!=(const Spans<T, N>& other) const { return !(*this == other); }
-
 };
 
 // A useful set of 2 spans that can contain any integer value. 2 spans is enough
 // to contain spans for any inequality, signed or unsigned: we represent numbers
 // as unsigned internally, and so e.g. signed x < 10 ends up as two disjoint
 // spans, [0..10] and [2^32..MAX_INT].
-using Spans2 = Spans<uint64_t, 2>;
+using SpansU2 = Spans<uint64_t, 2>;
 
 template<typename T>
 inline std::ostream& operator<<(std::ostream& os, const Span<T>& span) {

From 5852247457a855e873aef996b5ca133470dfdec3 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 11:41:35 -0700
Subject: [PATCH 09/30] test

---
 src/ir/constraint.h | 17 +++++++++--------
 src/support/span.h  | 15 +++++++++++----
 2 files changed, 20 insertions(+), 12 deletions(-)

diff --git a/src/ir/constraint.h b/src/ir/constraint.h
index ced8edd0b46..b666e91bdcd 100644
--- a/src/ir/constraint.h
+++ b/src/ir/constraint.h
@@ -27,7 +27,6 @@
 
 #include "ir/abstract.h"
 #include "support/inplace_vector.h"
-#include "support/iu64.h"
 #include "support/span.h"
 #include "support/utilities.h"
 #include "wasm.h"
@@ -66,19 +65,21 @@ struct Constraint {
     return Constraint{Abstract::negateRelational(op), term};
   }
 
-  // Convert the constraint into a constant span, if possible. For example,
-  // "<= 100 (unsigned)" turns into the span [0, 100].
+  // Convert the constraint into constant spans, if possible. For example,
+  // "<= 100 (unsigned)" turns into the span [0, 100]. We use SpansU2 because
+  // that can also handle signed operations stored in the unsigned range (see
+  // span.h).
   //
   // An optional type may be passed in. If not, the type is inferred from the
   // term, when possible.
-  std::optional<Span<IU64>> getSpan(std::optional<Type> type = {}) const;
+  std::optional<SpansU2> getSpans(std::optional<Type> type = {}) const;
 
-  // Get a span we can prove. This is less precise than getSpan, which gets an
-  // *exact* span to represent the Constraint. Here we only return a span we can
-  // prove is true. For example, x < y cannot be represented exactly using a
+  // Get spans we can prove. This is less precise than getSpans, which gets
+  // *exact* spans for the Constraint. Here we only return spans that we can
+  // prove are true. For example, x < y cannot be represented exactly using a
   // span (y is not a constant), but that x is smaller than *something* proves
   // x is not MAX_INT, so we can return the span [MIN_INT, MAX_INT - 1].
-  std::optional<Span<IU64>> getProvenSpan(std::optional<Type> type = {}) const;
+  std::optional<SpansU2> getProvenSpans(std::optional<Type> type = {}) const;
 };
 
 // We limit constraints to a low number to ensure good performance even with
diff --git a/src/support/span.h b/src/support/span.h
index a3126cea16a..4b8980fe4e2 100644
--- a/src/support/span.h
+++ b/src/support/span.h
@@ -89,7 +89,7 @@ template<typename T> struct Span {
   bool operator!=(const Span& other) const { return !(*this == other); }
 };
 
-// A union of spans
+// A union of spans, which we assume are disjoint.
 template<typename T, size_t N> struct Spans {
   inplace_vector<Span<T>, N> spans;
 
@@ -107,16 +107,23 @@ template<typename T, size_t N> struct Spans {
   }
 
   bool hasOverlap(const Spans<T, N>& other) const {
+    // There is overlap if any of our spans overlaps with any of other's.
     return std::any_of(spans.begin(), spans.end(), [](const Span<T>& span) {
       return std::any_of(other.spans.begin(), other.spans.end(), [](const Span<T>& otherSpan) {
         return span.hasOverlap(otherSpan);
-      }
+      });
     });
   }
 
-  // Check whether we contain another span (possibly being equal).
   bool contains(const Spans<T, N>& other) const {
-    return intersection(other) == other;
+    // We contain other if each of their spans is contained in us.
+    return std::all_of(other.spans.begin(), other.spans.end(), [](const Span<T>& otherSpan) {
+      // Because our spans are assumed to be disjoint, exactly one of our spans
+      // must contain otherSpan.
+      return std::any_of(spans.begin(), spans.end(), [](const Span<T>& span) {
+        return span.contains(otherSpan);
+      });
+    });
   }
 };
 

From f2dfee48d1d67e966d965d09d3f19ba8819e1642 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 11:46:49 -0700
Subject: [PATCH 10/30] test

---
 src/ir/constraint.cpp | 40 ++++++++++++++++++++--------------------
 src/support/span.h    | 13 +++++++++++++
 2 files changed, 33 insertions(+), 20 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 9f3e0e12c9f..6862088485d 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -24,7 +24,7 @@ namespace wasm::constraint {
 
 namespace {
 
-std::optional<Span<IU64>>
+std::optional<SpansU2>
 getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
   using namespace Abstract;
 
@@ -61,15 +61,15 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
     switch (c.op) {
       // x < y, i.e., x is less than *something*, proves x < MAX_INT.
       case LtS:
-        return Span<IU64>{minSigned, maxSigned - 1};
+        return SpansU2{minSigned, maxSigned - 1};
       case LtU:
-        return Span<IU64>{0, maxUnsigned - 1};
+        return SpansU2{0, maxUnsigned - 1};
 
       // Similarly, x > y proves x > MIN_INT.
       case GtS:
-        return Span<IU64>{minSigned + 1, maxSigned};
+        return SpansU2{minSigned + 1, maxSigned};
       case GtU:
-        return Span<IU64>{1, maxUnsigned};
+        return SpansU2{1, maxUnsigned};
 
       default: {
       }
@@ -87,7 +87,7 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
         // 0xffffffff into a Span, as it might be either uint32_t(-1)
         // or actually negative (but a bit pattern like 0x00000001 is
         // always fine as it can only ever be "1").
-        return Span<IU64>{x, x};
+        return SpansU2{x, x};
       }
       break;
     }
@@ -95,44 +95,44 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
     case LtS:
       if (cc->getInteger() == minSigned) {
         // Less than the lowest possible number is an empty span.
-        return Span<IU64>::empty();
+        return SpansU2::empty();
       } else {
-        return Span<IU64>{minSigned, cc->getInteger() - 1};
+        return SpansU2{minSigned, cc->getInteger() - 1};
       }
       break;
     case LtU:
       if (cc->getInteger() == 0) {
         // Less than the lowest possible number is an empty span.
-        return Span<IU64>::empty();
+        return SpansU2::empty();
       } else {
-        return Span<IU64>{0, cc->getUnsigned() - 1};
+        return SpansU2{0, cc->getUnsigned() - 1};
       }
       break;
     case LeS:
-      return Span<IU64>{minSigned, cc->getInteger()};
+      return SpansU2{minSigned, cc->getInteger()};
     case LeU:
-      return Span<IU64>{0, cc->getUnsigned()};
+      return SpansU2{0, cc->getUnsigned()};
 
     case GtS:
       if (cc->getInteger() == maxSigned) {
         // Greater than the highest possible number is an empty span.
-        return Span<IU64>::empty();
+        return SpansU2::empty();
       } else {
-        return Span<IU64>{cc->getInteger() + 1, maxSigned};
+        return SpansU2{cc->getInteger() + 1, maxSigned};
       }
       break;
     case GtU:
       if (cc->getUnsigned() == maxUnsigned) {
         // Greater than the highest possible number is an empty span.
-        return Span<IU64>::empty();
+        return SpansU2::empty();
       } else {
-        return Span<IU64>{cc->getUnsigned() + 1, maxUnsigned};
+        return SpansU2{cc->getUnsigned() + 1, maxUnsigned};
       }
       break;
     case GeS:
-      return Span<IU64>{cc->getInteger(), maxSigned};
+      return SpansU2{cc->getInteger(), maxSigned};
     case GeU:
-      return Span<IU64>{cc->getUnsigned(), maxUnsigned};
+      return SpansU2{cc->getUnsigned(), maxUnsigned};
 
     default: {
     }
@@ -143,11 +143,11 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
 
 } // anonymous namespace
 
-std::optional<Span<IU64>> Constraint::getSpan(std::optional<Type> type) const {
+std::optional<SpansU2> Constraint::getSpan(std::optional<Type> type) const {
   return getSpanInternal(*this, type, true);
 }
 
-std::optional<Span<IU64>>
+std::optional<SpansU2>
 Constraint::getProvenSpan(std::optional<Type> type) const {
   return getSpanInternal(*this, type, false);
 }
diff --git a/src/support/span.h b/src/support/span.h
index 4b8980fe4e2..57c90e7dbf9 100644
--- a/src/support/span.h
+++ b/src/support/span.h
@@ -100,12 +100,25 @@ template<typename T, size_t N> struct Spans {
   T max = Max;
 
   constexpr Spans() = default;
+
+  // Initialize with Spans.
   Spans(std::initializer_list<Span<T>> init) {
+    spans.reserve(init.size());
     for (auto& span : init) {
       spans.push_back(span);
     }
   }
 
+  // Initialize with pairs of coordinates.
+  Spans(std::initializer_list<T> init) {
+    assert(init.size() % 2 == 0);
+
+    spans.reserve(init.size() / 2);
+    for (auto it = init.begin(); it != init.end(); it += 2) {
+      spans.push_back(Span<T>{*it, *(it + 1)});
+    }
+  }
+
   bool hasOverlap(const Spans<T, N>& other) const {
     // There is overlap if any of our spans overlaps with any of other's.
     return std::any_of(spans.begin(), spans.end(), [](const Span<T>& span) {

From 040bc6241d38edcdb39ae95ab1929f34ec095014 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 11:53:13 -0700
Subject: [PATCH 11/30] test

---
 src/ir/constraint.cpp | 31 ++++++++++++++++---------------
 1 file changed, 16 insertions(+), 15 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 6862088485d..06a28d8efb2 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -41,15 +41,14 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
     return {};
   }
 
-  auto minSigned = type && *type == Type::i32
-                     ? std::numeric_limits<int32_t>::min()
-                     : std::numeric_limits<int64_t>::min();
-  auto maxSigned = type && *type == Type::i32
-                     ? std::numeric_limits<int32_t>::max()
-                     : std::numeric_limits<int64_t>::max();
-  auto maxUnsigned = type && *type == Type::i32
+  // Maximum values, as represented as uint64_t's.
+  uint64_t maxUnsigned = type && *type == Type::i32
                        ? std::numeric_limits<uint32_t>::max()
                        : std::numeric_limits<uint64_t>::max();
+  uint64_t maxSigned = type && *type == Type::i32
+                     ? std::numeric_limits<int32_t>::max()
+                     : std::numeric_limits<int64_t>::max();
+  uint64_t minSigned = maxSigned + 1;
 
   if (!cc) {
     // Not comparing to a constant, so we can't infer anything exact, but might
@@ -59,15 +58,17 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
     }
 
     switch (c.op) {
-      // x < y, i.e., x is less than *something*, proves x < MAX_INT.
+      // x < y, i.e., x is less than *something*, proves x != MAX_INT.
       case LtS:
-        return SpansU2{minSigned, maxSigned - 1};
+        // In the signed case, this is a pair of spans: all to the left and all
+        // to the right of MAX_INT.
+        return SpansU2{0, maxSigned - 1, maxSigned + 1, maxUnsigned};
       case LtU:
         return SpansU2{0, maxUnsigned - 1};
 
-      // Similarly, x > y proves x > MIN_INT.
+      // Similarly, x > y proves x != MIN_INT.
       case GtS:
-        return SpansU2{minSigned + 1, maxSigned};
+        return SpansU2{0, minSigned - 1, minSigned + 1, maxUnsigned};
       case GtU:
         return SpansU2{1, maxUnsigned};
 
@@ -95,7 +96,7 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
     case LtS:
       if (cc->getInteger() == minSigned) {
         // Less than the lowest possible number is an empty span.
-        return SpansU2::empty();
+        return SpansU2{};
       } else {
         return SpansU2{minSigned, cc->getInteger() - 1};
       }
@@ -103,7 +104,7 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
     case LtU:
       if (cc->getInteger() == 0) {
         // Less than the lowest possible number is an empty span.
-        return SpansU2::empty();
+        return SpansU2{};
       } else {
         return SpansU2{0, cc->getUnsigned() - 1};
       }
@@ -116,7 +117,7 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
     case GtS:
       if (cc->getInteger() == maxSigned) {
         // Greater than the highest possible number is an empty span.
-        return SpansU2::empty();
+        return SpansU2{};
       } else {
         return SpansU2{cc->getInteger() + 1, maxSigned};
       }
@@ -124,7 +125,7 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
     case GtU:
       if (cc->getUnsigned() == maxUnsigned) {
         // Greater than the highest possible number is an empty span.
-        return SpansU2::empty();
+        return SpansU2{};
       } else {
         return SpansU2{cc->getUnsigned() + 1, maxUnsigned};
       }

From 629b5319d45cfca1f4664e5065e1b5e9252534e3 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 11:55:07 -0700
Subject: [PATCH 12/30] test

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

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 06a28d8efb2..0a7d796c3d7 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -80,17 +80,16 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
   }
 
   switch (c.op) {
-    case Eq: {
-      auto x = cc->getUnsigned();
-      if (x <= uint64_t(maxSigned)) {
-        // This is in the range of both signed and unsigned values, so there is
-        // no ambiguity. That is, we cannot convert the bit pattern
-        // 0xffffffff into a Span, as it might be either uint32_t(-1)
-        // or actually negative (but a bit pattern like 0x00000001 is
-        // always fine as it can only ever be "1").
-        return SpansU2{x, x};
+    case Eq:
+      return SpansU2{x, x};
+    case Ne:
+      if (x == 0) {
+        return SpansU2{1, maxUnsigned};
       }
-      break;
+      if (x == maxUnsigned) {
+        return SpansU2{0, maxUnsigned - 1};
+      }
+      return SpansU2{0, x - 1, x + 1, maxUnsigned};
     }
 
     case LtS:

From c39ff376868016ccb578d8a9732e811882cf86c4 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 11:56:36 -0700
Subject: [PATCH 13/30] test

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

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 0a7d796c3d7..b09dbca51b6 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -96,8 +96,8 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
       if (cc->getInteger() == minSigned) {
         // Less than the lowest possible number is an empty span.
         return SpansU2{};
-      } else {
-        return SpansU2{minSigned, cc->getInteger() - 1};
+      }
+      return SpansU2{minSigned, cc->getInteger() - 1};
       }
       break;
     case LtU:

From f22d838901924c555893b19a5b2c0cdda283426f Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 12:56:32 -0700
Subject: [PATCH 14/30] test

---
 src/ir/constraint.cpp | 48 +++++++++++++++++++++++++++++--------------
 1 file changed, 33 insertions(+), 15 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index b09dbca51b6..3ffbf9d6642 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -79,6 +79,8 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
     return {};
   }
 
+  auto x = cc->getUnsigned();
+
   switch (c.op) {
     case Eq:
       return SpansU2{x, x};
@@ -93,46 +95,62 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
     }
 
     case LtS:
-      if (cc->getInteger() == minSigned) {
+      if (x == minSigned) {
         // Less than the lowest possible number is an empty span.
         return SpansU2{};
       }
-      return SpansU2{minSigned, cc->getInteger() - 1};
+      if (x > maxSigned) {
+        // A negative number, so just a single span.
+        return SpansU2{maxSigned + 1, x - 1};
       }
-      break;
+      if (x == 0) {
+        // All negative numbers are possible.
+        return SpansU2{maxSigned + 1, maxUnsigned};
+      }
+      // A positive number, so all negative ones are possible, and some
+      // positive.
+      return SpansU2{0, x - 1, maxSigned + 1, maxUnsigned};
     case LtU:
-      if (cc->getInteger() == 0) {
+      if (x == 0) {
         // Less than the lowest possible number is an empty span.
         return SpansU2{};
-      } else {
-        return SpansU2{0, cc->getUnsigned() - 1};
       }
-      break;
+      return SpansU2{0, x - 1};
     case LeS:
-      return SpansU2{minSigned, cc->getInteger()};
+      if (x > maxSigned) {
+        // A negative number, so just a single span.
+        return SpansU2{maxSigned + 1, x};
+      }
+      if (x == maxSigned) {
+        // All numbers are possible.
+        return SpansU2{0, maxUnSigned};
+      }
+      // A non-negative number, so all negative ones are possible, and some
+      // positive.
+      return SpansU2{0, x, maxSigned + 1, maxUnsigned};
     case LeU:
-      return SpansU2{0, cc->getUnsigned()};
+      return SpansU2{0, x};
 
     case GtS:
-      if (cc->getInteger() == maxSigned) {
+      if (x == maxSigned) {
         // Greater than the highest possible number is an empty span.
         return SpansU2{};
       } else {
-        return SpansU2{cc->getInteger() + 1, maxSigned};
+        return SpansU2{x + 1, maxSigned};
       }
       break;
     case GtU:
-      if (cc->getUnsigned() == maxUnsigned) {
+      if (x == maxUnsigned) {
         // Greater than the highest possible number is an empty span.
         return SpansU2{};
       } else {
-        return SpansU2{cc->getUnsigned() + 1, maxUnsigned};
+        return SpansU2{x + 1, maxUnsigned};
       }
       break;
     case GeS:
-      return SpansU2{cc->getInteger(), maxSigned};
+      return SpansU2{x, maxSigned};
     case GeU:
-      return SpansU2{cc->getUnsigned(), maxUnsigned};
+      return SpansU2{x, maxUnsigned};
 
     default: {
     }

From fea30666f3570bedc5eedf606a25d4393dbe0c26 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 13:05:34 -0700
Subject: [PATCH 15/30] test

---
 src/ir/constraint.cpp | 23 ++++++++++++++++++-----
 1 file changed, 18 insertions(+), 5 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 3ffbf9d6642..a53136018c2 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -135,20 +135,33 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
       if (x == maxSigned) {
         // Greater than the highest possible number is an empty span.
         return SpansU2{};
-      } else {
+      }
+      if (x <= maxSigned) {
+        // A non-negative number, so just a single span.
         return SpansU2{x + 1, maxSigned};
       }
-      break;
+      if (x == maxUnsigned) {
+        // GtS negative one, so 0 and above.
+        return SpansU2{0, maxSigned};
+      }
+      // A negative number, so all positive ones are possible, and some
+      // negative.
+      return SpansU2{0, maxSigned, x + 1, maxUnsigned};
     case GtU:
       if (x == maxUnsigned) {
         // Greater than the highest possible number is an empty span.
         return SpansU2{};
-      } else {
-        return SpansU2{x + 1, maxUnsigned};
       }
+      return SpansU2{x + 1, maxUnsigned};
       break;
     case GeS:
-      return SpansU2{x, maxSigned};
+      if (x <= maxSigned) {
+        // A non-negative number, so just a single span.
+        return SpansU2{x, maxSigned};
+      }
+      // A negative number, so all positive ones are possible, and some
+      // negative.
+      return SpansU2{0, maxSigned, x, maxUnsigned};
     case GeU:
       return SpansU2{x, maxUnsigned};
 

From 9633520249c3bb4dcb6909ab164de9e9fe71129e Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 13:05:58 -0700
Subject: [PATCH 16/30] test

---
 src/ir/constraint.cpp | 10 +++++-----
 src/support/span.h    | 20 +++++++++++---------
 2 files changed, 16 insertions(+), 14 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index a53136018c2..102a550dac5 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -43,11 +43,11 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
 
   // Maximum values, as represented as uint64_t's.
   uint64_t maxUnsigned = type && *type == Type::i32
-                       ? std::numeric_limits<uint32_t>::max()
-                       : std::numeric_limits<uint64_t>::max();
+                           ? std::numeric_limits<uint32_t>::max()
+                           : std::numeric_limits<uint64_t>::max();
   uint64_t maxSigned = type && *type == Type::i32
-                     ? std::numeric_limits<int32_t>::max()
-                     : std::numeric_limits<int64_t>::max();
+                         ? std::numeric_limits<int32_t>::max()
+                         : std::numeric_limits<int64_t>::max();
   uint64_t minSigned = maxSigned + 1;
 
   if (!cc) {
@@ -167,7 +167,7 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
 
     default: {
     }
-  }
+}
 
   return {};
 }
diff --git a/src/support/span.h b/src/support/span.h
index 57c90e7dbf9..d98f612db02 100644
--- a/src/support/span.h
+++ b/src/support/span.h
@@ -122,21 +122,23 @@ template<typename T, size_t N> struct Spans {
   bool hasOverlap(const Spans<T, N>& other) const {
     // There is overlap if any of our spans overlaps with any of other's.
     return std::any_of(spans.begin(), spans.end(), [](const Span<T>& span) {
-      return std::any_of(other.spans.begin(), other.spans.end(), [](const Span<T>& otherSpan) {
-        return span.hasOverlap(otherSpan);
-      });
+      return std::any_of(
+        other.spans.begin(), other.spans.end(), [](const Span<T>& otherSpan) {
+          return span.hasOverlap(otherSpan);
+        });
     });
   }
 
   bool contains(const Spans<T, N>& other) const {
     // We contain other if each of their spans is contained in us.
-    return std::all_of(other.spans.begin(), other.spans.end(), [](const Span<T>& otherSpan) {
-      // Because our spans are assumed to be disjoint, exactly one of our spans
-      // must contain otherSpan.
-      return std::any_of(spans.begin(), spans.end(), [](const Span<T>& span) {
-        return span.contains(otherSpan);
+    return std::all_of(
+      other.spans.begin(), other.spans.end(), [](const Span<T>& otherSpan) {
+        // Because our spans are assumed to be disjoint, exactly one of our
+        // spans must contain otherSpan.
+        return std::any_of(spans.begin(), spans.end(), [](const Span<T>& span) {
+          return span.contains(otherSpan);
+        });
       });
-    });
   }
 };
 

From 8bb9abdc4bd22f196738ea323798751eefafb24d Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 13:07:42 -0700
Subject: [PATCH 17/30] test

---
 src/ir/constraint.cpp | 26 +++++++++++++-------------
 src/support/span.h    | 20 +++++++++-----------
 2 files changed, 22 insertions(+), 24 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 102a550dac5..e76f1fbed1b 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -25,7 +25,7 @@ namespace wasm::constraint {
 namespace {
 
 std::optional<SpansU2>
-getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
+getSpansInternal(const Constraint& c, std::optional<Type> type, bool exact) {
   using namespace Abstract;
 
   auto* cc = std::get_if<Literal>(&c.term);
@@ -174,13 +174,13 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
 
 } // anonymous namespace
 
-std::optional<SpansU2> Constraint::getSpan(std::optional<Type> type) const {
-  return getSpanInternal(*this, type, true);
+std::optional<SpansU2> Constraint::getSpans(std::optional<Type> type) const {
+  return getSpansInternal(*this, type, true);
 }
 
 std::optional<SpansU2>
-Constraint::getProvenSpan(std::optional<Type> type) const {
-  return getSpanInternal(*this, type, false);
+Constraint::getProvenSpans(std::optional<Type> type) const {
+  return getSpansInternal(*this, type, false);
 }
 
 namespace {
@@ -278,26 +278,26 @@ Result provesPair(const Constraint& a, const Constraint& b) {
   // must be a constant in this case, so that we know the type.
   if (aConstant || bConstant) {
     auto type = aConstant ? aConstant->type : bConstant->type;
-    // Use a proven span for a, and an exact one for b. This allows us to do
-    // a => proven span for a => exact span for b => b.
-    if (auto aSpan = a.getProvenSpan(type)) {
-      if (auto bSpan = b.getSpan(type)) {
-        if (aSpan->isEmpty()) {
+    // Use proven spans for a, and exact for b. This allows us to do
+    // a => proven spans for a => exact spans for b => b.
+    if (auto aSpans = a.getProvenSpans(type)) {
+      if (auto bSpans = b.getSpans(type)) {
+        if (aSpans->empty()) {
           // An empty span implies a contradiction (e.g. x > MAX_INT), as it
           // means no possible number can apply. And contradictions prove
           // anything.
           return True;
         }
-        if (bSpan->isEmpty()) {
+        if (bSpans->empty()) {
           // Anything that is not a contradiction can prove a contradiction.
           return False;
         }
-        if (bSpan->contains(*aSpan)) {
+        if (bSpans->contains(*aSpans)) {
           // b's values contains a's, e.g., b = { 0 < x < 10 } and
           // a = { 3 < x < 7 }, so a => b.
           return True;
         }
-        if (!bSpan->hasOverlap(*aSpan)) {
+        if (!bSpans->hasOverlap(*aSpans)) {
           // There is no overlap at all, e.g., { 0 < x < 10 } vs { 20 < x < 30
           // }, both cannot be true and each proves the other false.
           return False;
diff --git a/src/support/span.h b/src/support/span.h
index d98f612db02..8255d3b7e8e 100644
--- a/src/support/span.h
+++ b/src/support/span.h
@@ -90,9 +90,7 @@ template<typename T> struct Span {
 };
 
 // A union of spans, which we assume are disjoint.
-template<typename T, size_t N> struct Spans {
-  inplace_vector<Span<T>, N> spans;
-
+template<typename T, size_t N> struct Spans : public inplace_vector<Span<T>, N> {
   static constexpr T Min = std::numeric_limits<T>::lowest();
   static constexpr T Max = std::numeric_limits<T>::max();
 
@@ -103,9 +101,9 @@ template<typename T, size_t N> struct Spans {
 
   // Initialize with Spans.
   Spans(std::initializer_list<Span<T>> init) {
-    spans.reserve(init.size());
+    reserve(init.size());
     for (auto& span : init) {
-      spans.push_back(span);
+      push_back(span);
     }
   }
 
@@ -113,17 +111,17 @@ template<typename T, size_t N> struct Spans {
   Spans(std::initializer_list<T> init) {
     assert(init.size() % 2 == 0);
 
-    spans.reserve(init.size() / 2);
+    reserve(init.size() / 2);
     for (auto it = init.begin(); it != init.end(); it += 2) {
-      spans.push_back(Span<T>{*it, *(it + 1)});
+      push_back(Span<T>{*it, *(it + 1)});
     }
   }
 
   bool hasOverlap(const Spans<T, N>& other) const {
     // There is overlap if any of our spans overlaps with any of other's.
-    return std::any_of(spans.begin(), spans.end(), [](const Span<T>& span) {
+    return std::any_of(begin(), end(), [](const Span<T>& span) {
       return std::any_of(
-        other.spans.begin(), other.spans.end(), [](const Span<T>& otherSpan) {
+        other.begin(), other.end(), [](const Span<T>& otherSpan) {
           return span.hasOverlap(otherSpan);
         });
     });
@@ -132,10 +130,10 @@ template<typename T, size_t N> struct Spans {
   bool contains(const Spans<T, N>& other) const {
     // We contain other if each of their spans is contained in us.
     return std::all_of(
-      other.spans.begin(), other.spans.end(), [](const Span<T>& otherSpan) {
+      other.begin(), other.end(), [](const Span<T>& otherSpan) {
         // Because our spans are assumed to be disjoint, exactly one of our
         // spans must contain otherSpan.
-        return std::any_of(spans.begin(), spans.end(), [](const Span<T>& span) {
+        return std::any_of(begin(), end(), [](const Span<T>& span) {
           return span.contains(otherSpan);
         });
       });

From 81b0e7b8cad38f9b2a00d9f81960be8b1338b381 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 13:07:49 -0700
Subject: [PATCH 18/30] test

---
 src/support/span.h | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/support/span.h b/src/support/span.h
index 8255d3b7e8e..c1d3b6c127c 100644
--- a/src/support/span.h
+++ b/src/support/span.h
@@ -90,7 +90,8 @@ template<typename T> struct Span {
 };
 
 // A union of spans, which we assume are disjoint.
-template<typename T, size_t N> struct Spans : public inplace_vector<Span<T>, N> {
+template<typename T, size_t N>
+struct Spans : public inplace_vector<Span<T>, N> {
   static constexpr T Min = std::numeric_limits<T>::lowest();
   static constexpr T Max = std::numeric_limits<T>::max();
 

From 14aa1d2cdf76b92b335780063ee02b4e522e231a Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 13:39:27 -0700
Subject: [PATCH 19/30] gemini

---
 src/ir/constraint.cpp                    |  10 +-
 src/support/span.h                       |  37 +-
 test/gtest/CMakeLists.txt                |   1 -
 test/gtest/constraint.cpp                | 680 ++++++++++++++---------
 test/gtest/span.cpp                      | 293 +++++-----
 test/lit/passes/constraint-analysis.wast |  32 +-
 6 files changed, 594 insertions(+), 459 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index e76f1fbed1b..19c6c5b11fd 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -92,7 +92,6 @@ getSpansInternal(const Constraint& c, std::optional<Type> type, bool exact) {
         return SpansU2{0, maxUnsigned - 1};
       }
       return SpansU2{0, x - 1, x + 1, maxUnsigned};
-    }
 
     case LtS:
       if (x == minSigned) {
@@ -123,7 +122,7 @@ getSpansInternal(const Constraint& c, std::optional<Type> type, bool exact) {
       }
       if (x == maxSigned) {
         // All numbers are possible.
-        return SpansU2{0, maxUnSigned};
+        return SpansU2{0, maxUnsigned};
       }
       // A non-negative number, so all negative ones are possible, and some
       // positive.
@@ -153,8 +152,11 @@ getSpansInternal(const Constraint& c, std::optional<Type> type, bool exact) {
         return SpansU2{};
       }
       return SpansU2{x + 1, maxUnsigned};
-      break;
     case GeS:
+      if (x == minSigned) {
+        // All numbers are possible.
+        return SpansU2{0, maxUnsigned};
+      }
       if (x <= maxSigned) {
         // A non-negative number, so just a single span.
         return SpansU2{x, maxSigned};
@@ -167,7 +169,7 @@ getSpansInternal(const Constraint& c, std::optional<Type> type, bool exact) {
 
     default: {
     }
-}
+  }
 
   return {};
 }
diff --git a/src/support/span.h b/src/support/span.h
index c1d3b6c127c..c0cec022961 100644
--- a/src/support/span.h
+++ b/src/support/span.h
@@ -92,19 +92,12 @@ template<typename T> struct Span {
 // A union of spans, which we assume are disjoint.
 template<typename T, size_t N>
 struct Spans : public inplace_vector<Span<T>, N> {
-  static constexpr T Min = std::numeric_limits<T>::lowest();
-  static constexpr T Max = std::numeric_limits<T>::max();
-
-  T min = Min;
-  T max = Max;
-
   constexpr Spans() = default;
 
   // Initialize with Spans.
   Spans(std::initializer_list<Span<T>> init) {
-    reserve(init.size());
-    for (auto& span : init) {
-      push_back(span);
+    for (const auto& span : init) {
+      this->push_back(span);
     }
   }
 
@@ -112,17 +105,16 @@ struct Spans : public inplace_vector<Span<T>, N> {
   Spans(std::initializer_list<T> init) {
     assert(init.size() % 2 == 0);
 
-    reserve(init.size() / 2);
     for (auto it = init.begin(); it != init.end(); it += 2) {
-      push_back(Span<T>{*it, *(it + 1)});
+      this->push_back(Span<T>{*it, *(it + 1)});
     }
   }
 
   bool hasOverlap(const Spans<T, N>& other) const {
     // There is overlap if any of our spans overlaps with any of other's.
-    return std::any_of(begin(), end(), [](const Span<T>& span) {
+    return std::any_of(this->begin(), this->end(), [&](const Span<T>& span) {
       return std::any_of(
-        other.begin(), other.end(), [](const Span<T>& otherSpan) {
+        other.begin(), other.end(), [&](const Span<T>& otherSpan) {
           return span.hasOverlap(otherSpan);
         });
     });
@@ -131,10 +123,10 @@ struct Spans : public inplace_vector<Span<T>, N> {
   bool contains(const Spans<T, N>& other) const {
     // We contain other if each of their spans is contained in us.
     return std::all_of(
-      other.begin(), other.end(), [](const Span<T>& otherSpan) {
+      other.begin(), other.end(), [&](const Span<T>& otherSpan) {
         // Because our spans are assumed to be disjoint, exactly one of our
         // spans must contain otherSpan.
-        return std::any_of(begin(), end(), [](const Span<T>& span) {
+        return std::any_of(this->begin(), this->end(), [&](const Span<T>& span) {
           return span.contains(otherSpan);
         });
       });
@@ -155,6 +147,21 @@ inline std::ostream& operator<<(std::ostream& os, const Span<T>& span) {
   return os << '[' << span.min << ", " << span.max << ']';
 }
 
+template<typename T, size_t N>
+inline std::ostream& operator<<(std::ostream& os, const Spans<T, N>& spans) {
+  if (spans.empty()) {
+    return os << "{empty}";
+  }
+  os << '{';
+  for (size_t i = 0; i < spans.size(); ++i) {
+    if (i > 0) {
+      os << ", ";
+    }
+    os << spans[i];
+  }
+  return os << '}';
+}
+
 } // namespace wasm
 
 #endif // wasm_support_span_h
diff --git a/test/gtest/CMakeLists.txt b/test/gtest/CMakeLists.txt
index 925880bd40a..c48edef2dd7 100644
--- a/test/gtest/CMakeLists.txt
+++ b/test/gtest/CMakeLists.txt
@@ -17,7 +17,6 @@ set(unittest_SOURCES
   disjoint_sets.cpp
   graph.cpp
   int128.cpp
-  iu64.cpp
   leaves.cpp
   glbs.cpp
   inplace_vector.cpp
diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index ff9f1d3fcf3..9ce42e337ee 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -351,12 +351,10 @@ TEST(ConstraintTest, TestOrLoop) {
 
   // Changes to operations:
 
-  // Change the Eq on the left to Ne. We fail to find anything for the OR.
-  // { x != 5 } || { x > 5 && x <= 42 }   ==>   {}
-  // TODO: we could emit x != 5
+  // Change the Eq on the left to Ne:
+  // { x != 5 } || { x > 5 && x <= 42 }   ==>   { x != 5 }
   AndedConstraintSet leftNe{{Ne, {Literal(int32_t(5))}}};
-  auto empty = AndedConstraintSet::makeProvesNothing();
-  checkOr(leftNe, right, empty);
+  checkOr(leftNe, right, leftNe);
 
   // Change the GtS on the right to GtU:
   // { x == 5 } || { x >U 5 && x <= 42 }   ==>   { x >=U 5 && x <= 42 }
@@ -426,12 +424,10 @@ TEST(ConstraintTest, TestOrLoopUnsigned) {
 
   // Changes to operations:
 
-  // Change the Eq on the left to Ne. We fail to find anything for the OR.
-  // { x != 5 } || { x > 5 && x <= 42 }   ==>   {}
-  // TODO: we could emit x != 5
+  // Change the Eq on the left to Ne:
+  // { x != 5 } || { x > 5 && x <= 42 }   ==>   { x != 5 }
   AndedConstraintSet leftNe{{Ne, {Literal(int32_t(5))}}};
-  auto empty = AndedConstraintSet::makeProvesNothing();
-  checkOr(leftNe, right, empty);
+  checkOr(leftNe, right, leftNe);
 
   // Add an operation on the right, x != 21:
   // { x == 5 } || { x >  5 && x <= 42 && x != 21 }   ==>
@@ -738,352 +734,378 @@ TEST(ConstraintTest, ComplexOrRegression) {
   EXPECT_TRUE(right.get(1).empty());
 }
 
-TEST(ConstraintTest, GetSpan) {
-  const IU64 minI32(std::numeric_limits<int32_t>::min());
-  const IU64 maxI32(std::numeric_limits<int32_t>::max());
-  const IU64 maxU32(std::numeric_limits<uint32_t>::max());
-  const IU64 minI64(std::numeric_limits<int64_t>::min());
-  const IU64 maxI64(std::numeric_limits<int64_t>::max());
-  const IU64 maxU64(std::numeric_limits<uint64_t>::max());
+TEST(ConstraintTest, GetSpans) {
+  const uint64_t minI32(uint32_t(std::numeric_limits<int32_t>::min()));
+  const uint64_t maxI32(std::numeric_limits<int32_t>::max());
+  const uint64_t maxU32(std::numeric_limits<uint32_t>::max());
+  const uint64_t minI64(uint64_t(std::numeric_limits<int64_t>::min()));
+  const uint64_t maxI64(std::numeric_limits<int64_t>::max());
+  const uint64_t maxU64(std::numeric_limits<uint64_t>::max());
 
   // Non-literal terms have no constant span.
-  EXPECT_EQ((Constraint{Eq, {Index(0)}}.getSpan()), std::nullopt);
-  EXPECT_EQ((Constraint{LtS, {Index(1)}}.getSpan()), std::nullopt);
-  EXPECT_EQ((Constraint{GeU, {Index(2)}}.getSpan()), std::nullopt);
-
-  // Unsupported operations (e.g. Ne) have no constant span.
-  EXPECT_EQ((Constraint{Ne, {Literal(int32_t(5))}}.getSpan()), std::nullopt);
-  EXPECT_EQ((Constraint{Ne, {Literal(int32_t(0))}}.getSpan()), std::nullopt);
-
-  // Eq (i32): non-negative values up to int32_t max have an unambiguous span.
-  EXPECT_EQ((Constraint{Eq, {Literal(int32_t(0))}}.getSpan()),
-            (Span<IU64>{0, 0}));
-  EXPECT_EQ((Constraint{Eq, {Literal(int32_t(1))}}.getSpan()),
-            (Span<IU64>{1, 1}));
-  EXPECT_EQ((Constraint{Eq, {Literal(int32_t(42))}}.getSpan()),
-            (Span<IU64>{42, 42}));
+  EXPECT_EQ((Constraint{Eq, {Index(0)}}.getSpans()), std::nullopt);
+  EXPECT_EQ((Constraint{LtS, {Index(1)}}.getSpans()), std::nullopt);
+  EXPECT_EQ((Constraint{GeU, {Index(2)}}.getSpans()), std::nullopt);
+
+  // Ne operation
+  EXPECT_EQ((Constraint{Ne, {Literal(int32_t(0))}}.getSpans()),
+            (SpansU2{1, maxU32}));
+  EXPECT_EQ((Constraint{Ne, {Literal(int32_t(5))}}.getSpans()),
+            (SpansU2{0, 4, 6, maxU32}));
+  EXPECT_EQ((Constraint{Ne, {Literal(uint32_t(maxU32))}}.getSpans()),
+            (SpansU2{0, maxU32 - 1}));
+
+  EXPECT_EQ((Constraint{Ne, {Literal(int64_t(0))}}.getSpans()),
+            (SpansU2{1, maxU64}));
+  EXPECT_EQ((Constraint{Ne, {Literal(int64_t(5))}}.getSpans()),
+            (SpansU2{0, 4, 6, maxU64}));
+  EXPECT_EQ((Constraint{Ne, {Literal(uint64_t(maxU64))}}.getSpans()),
+            (SpansU2{0, maxU64 - 1}));
+
+  // Eq (i32)
+  EXPECT_EQ((Constraint{Eq, {Literal(int32_t(0))}}.getSpans()),
+            (SpansU2{0, 0}));
+  EXPECT_EQ((Constraint{Eq, {Literal(int32_t(1))}}.getSpans()),
+            (SpansU2{1, 1}));
+  EXPECT_EQ((Constraint{Eq, {Literal(int32_t(42))}}.getSpans()),
+            (SpansU2{42, 42}));
   EXPECT_EQ(
-    (Constraint{Eq, {Literal(std::numeric_limits<int32_t>::max())}}.getSpan()),
-    (Span<IU64>{maxI32, maxI32}));
-
-  // Eq (i32) with negative or large unsigned values returns nullopt due to
-  // signed/unsigned ambiguity.
-  EXPECT_EQ((Constraint{Eq, {Literal(int32_t(-1))}}.getSpan()), std::nullopt);
-  EXPECT_EQ((Constraint{Eq, {Literal(int32_t(-42))}}.getSpan()), std::nullopt);
+    (Constraint{Eq, {Literal(std::numeric_limits<int32_t>::max())}}.getSpans()),
+    (SpansU2{maxI32, maxI32}));
+  EXPECT_EQ((Constraint{Eq, {Literal(int32_t(-1))}}.getSpans()),
+            (SpansU2{maxU32, maxU32}));
+  EXPECT_EQ((Constraint{Eq, {Literal(int32_t(-42))}}.getSpans()),
+            (SpansU2{uint32_t(-42), uint32_t(-42)}));
   EXPECT_EQ(
-    (Constraint{Eq, {Literal(std::numeric_limits<int32_t>::min())}}.getSpan()),
-    std::nullopt);
-  EXPECT_EQ((Constraint{Eq, {Literal(uint32_t(0x80000000u))}}.getSpan()),
-            std::nullopt);
+    (Constraint{Eq, {Literal(std::numeric_limits<int32_t>::min())}}.getSpans()),
+    (SpansU2{minI32, minI32}));
+  EXPECT_EQ((Constraint{Eq, {Literal(uint32_t(0x80000000u))}}.getSpans()),
+            (SpansU2{0x80000000u, 0x80000000u}));
   EXPECT_EQ(
-    (Constraint{Eq, {Literal(std::numeric_limits<uint32_t>::max())}}.getSpan()),
-    std::nullopt);
-
-  // Eq (i64): non-negative values up to int64_t max have an unambiguous span.
-  EXPECT_EQ((Constraint{Eq, {Literal(int64_t(0))}}.getSpan()),
-            (Span<IU64>{0, 0}));
-  EXPECT_EQ((Constraint{Eq, {Literal(int64_t(42))}}.getSpan()),
-            (Span<IU64>{42, 42}));
+    (Constraint{Eq, {Literal(std::numeric_limits<uint32_t>::max())}}.getSpans()),
+    (SpansU2{maxU32, maxU32}));
+
+  // Eq (i64)
+  EXPECT_EQ((Constraint{Eq, {Literal(int64_t(0))}}.getSpans()),
+            (SpansU2{0, 0}));
+  EXPECT_EQ((Constraint{Eq, {Literal(int64_t(42))}}.getSpans()),
+            (SpansU2{42, 42}));
   EXPECT_EQ(
     (Constraint{Eq, {Literal(int64_t(std::numeric_limits<int32_t>::max()) + 1)}}
-       .getSpan()),
-    (Span<IU64>{uint64_t(std::numeric_limits<int32_t>::max()) + 1,
-                uint64_t(std::numeric_limits<int32_t>::max()) + 1}));
+       .getSpans()),
+    (SpansU2{uint64_t(std::numeric_limits<int32_t>::max()) + 1,
+             uint64_t(std::numeric_limits<int32_t>::max()) + 1}));
   EXPECT_EQ(
-    (Constraint{Eq, {Literal(std::numeric_limits<int64_t>::max())}}.getSpan()),
-    (Span<IU64>{maxI64, maxI64}));
-
-  // Eq (i64) with negative or large unsigned values returns nullopt.
-  EXPECT_EQ((Constraint{Eq, {Literal(int64_t(-1))}}.getSpan()), std::nullopt);
+    (Constraint{Eq, {Literal(std::numeric_limits<int64_t>::max())}}.getSpans()),
+    (SpansU2{maxI64, maxI64}));
+  EXPECT_EQ((Constraint{Eq, {Literal(int64_t(-1))}}.getSpans()),
+            (SpansU2{maxU64, maxU64}));
   EXPECT_EQ(
-    (Constraint{Eq, {Literal(std::numeric_limits<int64_t>::min())}}.getSpan()),
-    std::nullopt);
-  EXPECT_EQ((Constraint{Eq, {Literal(uint64_t(uint64_t(1) << 63))}}.getSpan()),
-            std::nullopt);
+    (Constraint{Eq, {Literal(std::numeric_limits<int64_t>::min())}}.getSpans()),
+    (SpansU2{minI64, minI64}));
+  EXPECT_EQ((Constraint{Eq, {Literal(uint64_t(uint64_t(1) << 63))}}.getSpans()),
+            (SpansU2{minI64, minI64}));
   EXPECT_EQ(
-    (Constraint{Eq, {Literal(std::numeric_limits<uint64_t>::max())}}.getSpan()),
-    std::nullopt);
-
-  // LtS (i32): [minI32, C - 1]
-  EXPECT_EQ((Constraint{LtS, {Literal(int32_t(10))}}.getSpan()),
-            (Span<IU64>{minI32, IU64(9)}));
-  EXPECT_EQ((Constraint{LtS, {Literal(int32_t(0))}}.getSpan()),
-            (Span<IU64>{minI32, IU64(-1)}));
-  EXPECT_EQ((Constraint{LtS, {Literal(int32_t(-5))}}.getSpan()),
-            (Span<IU64>{minI32, IU64(-6)}));
+    (Constraint{Eq, {Literal(std::numeric_limits<uint64_t>::max())}}.getSpans()),
+    (SpansU2{maxU64, maxU64}));
+
+  // LtS (i32):
+  EXPECT_EQ((Constraint{LtS, {Literal(int32_t(10))}}.getSpans()),
+            (SpansU2{0, 9, minI32, maxU32}));
+  EXPECT_EQ((Constraint{LtS, {Literal(int32_t(0))}}.getSpans()),
+            (SpansU2{minI32, maxU32}));
+  EXPECT_EQ((Constraint{LtS, {Literal(int32_t(-5))}}.getSpans()),
+            (SpansU2{minI32, uint32_t(-6)}));
   EXPECT_EQ(
-    (Constraint{LtS, {Literal(std::numeric_limits<int32_t>::max())}}.getSpan()),
-    (Span<IU64>{minI32, IU64(std::numeric_limits<int32_t>::max() - 1)}));
+    (Constraint{LtS, {Literal(std::numeric_limits<int32_t>::max())}}.getSpans()),
+    (SpansU2{0, maxI32 - 1, minI32, maxU32}));
   // LtS min signed (i32): empty span
   auto ltsMin32 =
-    Constraint{LtS, {Literal(std::numeric_limits<int32_t>::min())}}.getSpan();
+    Constraint{LtS, {Literal(std::numeric_limits<int32_t>::min())}}.getSpans();
   ASSERT_TRUE(ltsMin32.has_value());
-  EXPECT_TRUE(ltsMin32->isEmpty());
-  EXPECT_EQ(ltsMin32, Span<IU64>::empty());
-
-  // LtS (i64): [minI64, C - 1]
-  EXPECT_EQ((Constraint{LtS, {Literal(int64_t(100))}}.getSpan()),
-            (Span<IU64>{minI64, IU64(99)}));
-  EXPECT_EQ((Constraint{LtS, {Literal(int64_t(0))}}.getSpan()),
-            (Span<IU64>{minI64, IU64(-1)}));
+  EXPECT_TRUE(ltsMin32->empty());
+  EXPECT_EQ(ltsMin32, SpansU2{});
+
+  // LtS (i64):
+  EXPECT_EQ((Constraint{LtS, {Literal(int64_t(100))}}.getSpans()),
+            (SpansU2{0, 99, minI64, maxU64}));
+  EXPECT_EQ((Constraint{LtS, {Literal(int64_t(0))}}.getSpans()),
+            (SpansU2{minI64, maxU64}));
+  EXPECT_EQ((Constraint{LtS, {Literal(int64_t(-5))}}.getSpans()),
+            (SpansU2{minI64, uint64_t(-6)}));
   EXPECT_EQ(
-    (Constraint{LtS, {Literal(std::numeric_limits<int64_t>::max())}}.getSpan()),
-    (Span<IU64>{minI64, IU64(std::numeric_limits<int64_t>::max() - 1)}));
+    (Constraint{LtS, {Literal(std::numeric_limits<int64_t>::max())}}.getSpans()),
+    (SpansU2{0, maxI64 - 1, minI64, maxU64}));
   // LtS min signed (i64): empty span
   auto ltsMin64 =
-    Constraint{LtS, {Literal(std::numeric_limits<int64_t>::min())}}.getSpan();
+    Constraint{LtS, {Literal(std::numeric_limits<int64_t>::min())}}.getSpans();
   ASSERT_TRUE(ltsMin64.has_value());
-  EXPECT_TRUE(ltsMin64->isEmpty());
-  EXPECT_EQ(ltsMin64, Span<IU64>::empty());
+  EXPECT_TRUE(ltsMin64->empty());
+  EXPECT_EQ(ltsMin64, SpansU2{});
 
   // LtU (i32): [0, C - 1]
-  EXPECT_EQ((Constraint{LtU, {Literal(uint32_t(10))}}.getSpan()),
-            (Span<IU64>{IU64(0), IU64(9)}));
-  EXPECT_EQ((Constraint{LtU, {Literal(uint32_t(1))}}.getSpan()),
-            (Span<IU64>{IU64(0), IU64(0)}));
+  EXPECT_EQ((Constraint{LtU, {Literal(uint32_t(10))}}.getSpans()),
+            (SpansU2{0, 9}));
+  EXPECT_EQ((Constraint{LtU, {Literal(uint32_t(1))}}.getSpans()),
+            (SpansU2{0, 0}));
   EXPECT_EQ(
     (Constraint{LtU, {Literal(std::numeric_limits<uint32_t>::max())}}
-       .getSpan()),
-    (Span<IU64>{IU64(0),
-                IU64(uint64_t(std::numeric_limits<uint32_t>::max()) - 1)}));
+       .getSpans()),
+    (SpansU2{0, maxU32 - 1}));
   // LtU 0 (i32): empty span
-  auto ltuZero32 = Constraint{LtU, {Literal(uint32_t(0))}}.getSpan();
+  auto ltuZero32 = Constraint{LtU, {Literal(uint32_t(0))}}.getSpans();
   ASSERT_TRUE(ltuZero32.has_value());
-  EXPECT_TRUE(ltuZero32->isEmpty());
-  EXPECT_EQ(ltuZero32, Span<IU64>::empty());
+  EXPECT_TRUE(ltuZero32->empty());
+  EXPECT_EQ(ltuZero32, SpansU2{});
 
   // LtU (i64): [0, C - 1]
-  EXPECT_EQ((Constraint{LtU, {Literal(uint64_t(100))}}.getSpan()),
-            (Span<IU64>{IU64(0), IU64(99)}));
+  EXPECT_EQ((Constraint{LtU, {Literal(uint64_t(100))}}.getSpans()),
+            (SpansU2{0, 99}));
   EXPECT_EQ(
     (Constraint{LtU, {Literal(std::numeric_limits<uint64_t>::max())}}
-       .getSpan()),
-    (Span<IU64>{IU64(0), IU64(std::numeric_limits<uint64_t>::max() - 1)}));
+       .getSpans()),
+    (SpansU2{0, maxU64 - 1}));
   // LtU 0 (i64): empty span
-  auto ltuZero64 = Constraint{LtU, {Literal(uint64_t(0))}}.getSpan();
+  auto ltuZero64 = Constraint{LtU, {Literal(uint64_t(0))}}.getSpans();
   ASSERT_TRUE(ltuZero64.has_value());
-  EXPECT_TRUE(ltuZero64->isEmpty());
-  EXPECT_EQ(ltuZero64, Span<IU64>::empty());
-
-  // LeS (i32): [minI32, C]
-  EXPECT_EQ((Constraint{LeS, {Literal(int32_t(10))}}.getSpan()),
-            (Span<IU64>{minI32, IU64(10)}));
-  EXPECT_EQ((Constraint{LeS, {Literal(int32_t(0))}}.getSpan()),
-            (Span<IU64>{minI32, IU64(0)}));
-  EXPECT_EQ((Constraint{LeS, {Literal(int32_t(-5))}}.getSpan()),
-            (Span<IU64>{minI32, IU64(-5)}));
+  EXPECT_TRUE(ltuZero64->empty());
+  EXPECT_EQ(ltuZero64, SpansU2{});
+
+  // LeS (i32):
+  EXPECT_EQ((Constraint{LeS, {Literal(int32_t(10))}}.getSpans()),
+            (SpansU2{0, 10, minI32, maxU32}));
+  EXPECT_EQ((Constraint{LeS, {Literal(int32_t(0))}}.getSpans()),
+            (SpansU2{0, 0, minI32, maxU32}));
+  EXPECT_EQ((Constraint{LeS, {Literal(int32_t(-5))}}.getSpans()),
+            (SpansU2{minI32, uint32_t(-5)}));
   EXPECT_EQ(
-    (Constraint{LeS, {Literal(std::numeric_limits<int32_t>::min())}}.getSpan()),
-    (Span<IU64>{minI32, minI32}));
+    (Constraint{LeS, {Literal(std::numeric_limits<int32_t>::min())}}.getSpans()),
+    (SpansU2{minI32, minI32}));
   EXPECT_EQ(
-    (Constraint{LeS, {Literal(std::numeric_limits<int32_t>::max())}}.getSpan()),
-    (Span<IU64>{minI32, maxI32}));
-
-  // LeS (i64): [minI64, C]
-  EXPECT_EQ((Constraint{LeS, {Literal(int64_t(10))}}.getSpan()),
-            (Span<IU64>{minI64, IU64(10)}));
+    (Constraint{LeS, {Literal(std::numeric_limits<int32_t>::max())}}.getSpans()),
+    (SpansU2{0, maxU32}));
+
+  // LeS (i64):
+  EXPECT_EQ((Constraint{LeS, {Literal(int64_t(10))}}.getSpans()),
+            (SpansU2{0, 10, minI64, maxU64}));
+  EXPECT_EQ((Constraint{LeS, {Literal(int64_t(0))}}.getSpans()),
+            (SpansU2{0, 0, minI64, maxU64}));
+  EXPECT_EQ((Constraint{LeS, {Literal(int64_t(-5))}}.getSpans()),
+            (SpansU2{minI64, uint64_t(-5)}));
   EXPECT_EQ(
-    (Constraint{LeS, {Literal(std::numeric_limits<int64_t>::min())}}.getSpan()),
-    (Span<IU64>{minI64, minI64}));
+    (Constraint{LeS, {Literal(std::numeric_limits<int64_t>::min())}}.getSpans()),
+    (SpansU2{minI64, minI64}));
   EXPECT_EQ(
-    (Constraint{LeS, {Literal(std::numeric_limits<int64_t>::max())}}.getSpan()),
-    (Span<IU64>{minI64, maxI64}));
+    (Constraint{LeS, {Literal(std::numeric_limits<int64_t>::max())}}.getSpans()),
+    (SpansU2{0, maxU64}));
 
   // LeU (i32): [0, C]
-  EXPECT_EQ((Constraint{LeU, {Literal(uint32_t(0))}}.getSpan()),
-            (Span<IU64>{IU64(0), IU64(0)}));
-  EXPECT_EQ((Constraint{LeU, {Literal(uint32_t(10))}}.getSpan()),
-            (Span<IU64>{IU64(0), IU64(10)}));
+  EXPECT_EQ((Constraint{LeU, {Literal(uint32_t(0))}}.getSpans()),
+            (SpansU2{0, 0}));
+  EXPECT_EQ((Constraint{LeU, {Literal(uint32_t(10))}}.getSpans()),
+            (SpansU2{0, 10}));
   EXPECT_EQ((Constraint{LeU, {Literal(std::numeric_limits<uint32_t>::max())}}
-               .getSpan()),
-            (Span<IU64>{IU64(0), maxU32}));
+               .getSpans()),
+            (SpansU2{0, maxU32}));
 
   // LeU (i64): [0, C]
-  EXPECT_EQ((Constraint{LeU, {Literal(uint64_t(0))}}.getSpan()),
-            (Span<IU64>{IU64(0), IU64(0)}));
-  EXPECT_EQ((Constraint{LeU, {Literal(uint64_t(10))}}.getSpan()),
-            (Span<IU64>{IU64(0), IU64(10)}));
+  EXPECT_EQ((Constraint{LeU, {Literal(uint64_t(0))}}.getSpans()),
+            (SpansU2{0, 0}));
+  EXPECT_EQ((Constraint{LeU, {Literal(uint64_t(10))}}.getSpans()),
+            (SpansU2{0, 10}));
   EXPECT_EQ((Constraint{LeU, {Literal(std::numeric_limits<uint64_t>::max())}}
-               .getSpan()),
-            (Span<IU64>{IU64(0), maxU64}));
-
-  // GtS (i32): [C + 1, maxI32]
-  EXPECT_EQ((Constraint{GtS, {Literal(int32_t(10))}}.getSpan()),
-            (Span<IU64>{IU64(11), maxI32}));
-  EXPECT_EQ((Constraint{GtS, {Literal(int32_t(0))}}.getSpan()),
-            (Span<IU64>{IU64(1), maxI32}));
-  EXPECT_EQ((Constraint{GtS, {Literal(int32_t(-5))}}.getSpan()),
-            (Span<IU64>{IU64(-4), maxI32}));
+               .getSpans()),
+            (SpansU2{0, maxU64}));
+
+  // GtS (i32):
+  EXPECT_EQ((Constraint{GtS, {Literal(int32_t(10))}}.getSpans()),
+            (SpansU2{11, maxI32}));
+  EXPECT_EQ((Constraint{GtS, {Literal(int32_t(0))}}.getSpans()),
+            (SpansU2{1, maxI32}));
+  EXPECT_EQ((Constraint{GtS, {Literal(int32_t(-5))}}.getSpans()),
+            (SpansU2{0, maxI32, uint32_t(-4), maxU32}));
+  EXPECT_EQ((Constraint{GtS, {Literal(int32_t(-1))}}.getSpans()),
+            (SpansU2{0, maxI32}));
   EXPECT_EQ(
-    (Constraint{GtS, {Literal(std::numeric_limits<int32_t>::min())}}.getSpan()),
-    (Span<IU64>{IU64(std::numeric_limits<int32_t>::min() + 1), maxI32}));
+    (Constraint{GtS, {Literal(std::numeric_limits<int32_t>::min())}}.getSpans()),
+    (SpansU2{0, maxI32, minI32 + 1, maxU32}));
   EXPECT_EQ((Constraint{GtS, {Literal(std::numeric_limits<int32_t>::max() - 1)}}
-               .getSpan()),
-            (Span<IU64>{maxI32, maxI32}));
+               .getSpans()),
+            (SpansU2{maxI32, maxI32}));
   // GtS max signed (i32): empty span
   auto gtsMax32 =
-    Constraint{GtS, {Literal(std::numeric_limits<int32_t>::max())}}.getSpan();
+    Constraint{GtS, {Literal(std::numeric_limits<int32_t>::max())}}.getSpans();
   ASSERT_TRUE(gtsMax32.has_value());
-  EXPECT_TRUE(gtsMax32->isEmpty());
-  EXPECT_EQ(gtsMax32, Span<IU64>::empty());
-
-  // GtS (i64): [C + 1, maxI64]
-  EXPECT_EQ((Constraint{GtS, {Literal(int64_t(10))}}.getSpan()),
-            (Span<IU64>{IU64(11), maxI64}));
-  EXPECT_EQ((Constraint{GtS, {Literal(int64_t(0))}}.getSpan()),
-            (Span<IU64>{IU64(1), maxI64}));
+  EXPECT_TRUE(gtsMax32->empty());
+  EXPECT_EQ(gtsMax32, SpansU2{});
+
+  // GtS (i64):
+  EXPECT_EQ((Constraint{GtS, {Literal(int64_t(10))}}.getSpans()),
+            (SpansU2{11, maxI64}));
+  EXPECT_EQ((Constraint{GtS, {Literal(int64_t(0))}}.getSpans()),
+            (SpansU2{1, maxI64}));
+  EXPECT_EQ((Constraint{GtS, {Literal(int64_t(-5))}}.getSpans()),
+            (SpansU2{0, maxI64, uint64_t(-4), maxU64}));
+  EXPECT_EQ((Constraint{GtS, {Literal(int64_t(-1))}}.getSpans()),
+            (SpansU2{0, maxI64}));
   EXPECT_EQ(
-    (Constraint{GtS, {Literal(std::numeric_limits<int64_t>::min())}}.getSpan()),
-    (Span<IU64>{IU64(std::numeric_limits<int64_t>::min() + 1), maxI64}));
+    (Constraint{GtS, {Literal(std::numeric_limits<int64_t>::min())}}.getSpans()),
+    (SpansU2{0, maxI64, minI64 + 1, maxU64}));
   EXPECT_EQ((Constraint{GtS, {Literal(std::numeric_limits<int64_t>::max() - 1)}}
-               .getSpan()),
-            (Span<IU64>{maxI64, maxI64}));
+               .getSpans()),
+            (SpansU2{maxI64, maxI64}));
   // GtS max signed (i64): empty span
   auto gtsMax64 =
-    Constraint{GtS, {Literal(std::numeric_limits<int64_t>::max())}}.getSpan();
+    Constraint{GtS, {Literal(std::numeric_limits<int64_t>::max())}}.getSpans();
   ASSERT_TRUE(gtsMax64.has_value());
-  EXPECT_TRUE(gtsMax64->isEmpty());
-  EXPECT_EQ(gtsMax64, Span<IU64>::empty());
+  EXPECT_TRUE(gtsMax64->empty());
+  EXPECT_EQ(gtsMax64, SpansU2{});
 
   // GtU (i32): [C + 1, maxU32]
-  EXPECT_EQ((Constraint{GtU, {Literal(uint32_t(0))}}.getSpan()),
-            (Span<IU64>{IU64(1), maxU32}));
-  EXPECT_EQ((Constraint{GtU, {Literal(uint32_t(10))}}.getSpan()),
-            (Span<IU64>{IU64(11), maxU32}));
+  EXPECT_EQ((Constraint{GtU, {Literal(uint32_t(0))}}.getSpans()),
+            (SpansU2{1, maxU32}));
+  EXPECT_EQ((Constraint{GtU, {Literal(uint32_t(10))}}.getSpans()),
+            (SpansU2{11, maxU32}));
   EXPECT_EQ(
     (Constraint{GtU, {Literal(std::numeric_limits<uint32_t>::max() - 1)}}
-       .getSpan()),
-    (Span<IU64>{maxU32, maxU32}));
+       .getSpans()),
+    (SpansU2{maxU32, maxU32}));
   // GtU max unsigned (i32): empty span
   auto gtuMax32 =
-    Constraint{GtU, {Literal(std::numeric_limits<uint32_t>::max())}}.getSpan();
+    Constraint{GtU, {Literal(std::numeric_limits<uint32_t>::max())}}.getSpans();
   ASSERT_TRUE(gtuMax32.has_value());
-  EXPECT_TRUE(gtuMax32->isEmpty());
-  EXPECT_EQ(gtuMax32, Span<IU64>::empty());
+  EXPECT_TRUE(gtuMax32->empty());
+  EXPECT_EQ(gtuMax32, SpansU2{});
 
   // GtU (i64): [C + 1, maxU64]
-  EXPECT_EQ((Constraint{GtU, {Literal(uint64_t(0))}}.getSpan()),
-            (Span<IU64>{IU64(1), maxU64}));
-  EXPECT_EQ((Constraint{GtU, {Literal(uint64_t(10))}}.getSpan()),
-            (Span<IU64>{IU64(11), maxU64}));
+  EXPECT_EQ((Constraint{GtU, {Literal(uint64_t(0))}}.getSpans()),
+            (SpansU2{1, maxU64}));
+  EXPECT_EQ((Constraint{GtU, {Literal(uint64_t(10))}}.getSpans()),
+            (SpansU2{11, maxU64}));
   EXPECT_EQ(
     (Constraint{GtU, {Literal(std::numeric_limits<uint64_t>::max() - 1)}}
-       .getSpan()),
-    (Span<IU64>{maxU64, maxU64}));
+       .getSpans()),
+    (SpansU2{maxU64, maxU64}));
   // GtU max unsigned (i64): empty span
   auto gtuMax64 =
-    Constraint{GtU, {Literal(std::numeric_limits<uint64_t>::max())}}.getSpan();
+    Constraint{GtU, {Literal(std::numeric_limits<uint64_t>::max())}}.getSpans();
   ASSERT_TRUE(gtuMax64.has_value());
-  EXPECT_TRUE(gtuMax64->isEmpty());
-  EXPECT_EQ(gtuMax64, Span<IU64>::empty());
-
-  // GeS (i32): [C, maxI32]
-  EXPECT_EQ((Constraint{GeS, {Literal(int32_t(10))}}.getSpan()),
-            (Span<IU64>{IU64(10), maxI32}));
-  EXPECT_EQ((Constraint{GeS, {Literal(int32_t(0))}}.getSpan()),
-            (Span<IU64>{IU64(0), maxI32}));
-  EXPECT_EQ((Constraint{GeS, {Literal(int32_t(-5))}}.getSpan()),
-            (Span<IU64>{IU64(-5), maxI32}));
+  EXPECT_TRUE(gtuMax64->empty());
+  EXPECT_EQ(gtuMax64, SpansU2{});
+
+  // GeS (i32):
+  EXPECT_EQ((Constraint{GeS, {Literal(int32_t(10))}}.getSpans()),
+            (SpansU2{10, maxI32}));
+  EXPECT_EQ((Constraint{GeS, {Literal(int32_t(0))}}.getSpans()),
+            (SpansU2{0, maxI32}));
+  EXPECT_EQ((Constraint{GeS, {Literal(int32_t(-5))}}.getSpans()),
+            (SpansU2{0, maxI32, uint32_t(-5), maxU32}));
+  EXPECT_EQ((Constraint{GeS, {Literal(int32_t(-1))}}.getSpans()),
+            (SpansU2{0, maxI32, maxU32, maxU32}));
   EXPECT_EQ(
-    (Constraint{GeS, {Literal(std::numeric_limits<int32_t>::min())}}.getSpan()),
-    (Span<IU64>{minI32, maxI32}));
+    (Constraint{GeS, {Literal(std::numeric_limits<int32_t>::min())}}.getSpans()),
+    (SpansU2{0, maxU32}));
   EXPECT_EQ(
-    (Constraint{GeS, {Literal(std::numeric_limits<int32_t>::max())}}.getSpan()),
-    (Span<IU64>{maxI32, maxI32}));
-
-  // GeS (i64): [C, maxI64]
-  EXPECT_EQ((Constraint{GeS, {Literal(int64_t(10))}}.getSpan()),
-            (Span<IU64>{IU64(10), maxI64}));
-  EXPECT_EQ((Constraint{GeS, {Literal(int64_t(0))}}.getSpan()),
-            (Span<IU64>{IU64(0), maxI64}));
+    (Constraint{GeS, {Literal(std::numeric_limits<int32_t>::max())}}.getSpans()),
+    (SpansU2{maxI32, maxI32}));
+
+  // GeS (i64):
+  EXPECT_EQ((Constraint{GeS, {Literal(int64_t(10))}}.getSpans()),
+            (SpansU2{10, maxI64}));
+  EXPECT_EQ((Constraint{GeS, {Literal(int64_t(0))}}.getSpans()),
+            (SpansU2{0, maxI64}));
+  EXPECT_EQ((Constraint{GeS, {Literal(int64_t(-5))}}.getSpans()),
+            (SpansU2{0, maxI64, uint64_t(-5), maxU64}));
+  EXPECT_EQ((Constraint{GeS, {Literal(int64_t(-1))}}.getSpans()),
+            (SpansU2{0, maxI64, maxU64, maxU64}));
   EXPECT_EQ(
-    (Constraint{GeS, {Literal(std::numeric_limits<int64_t>::min())}}.getSpan()),
-    (Span<IU64>{minI64, maxI64}));
+    (Constraint{GeS, {Literal(std::numeric_limits<int64_t>::min())}}.getSpans()),
+    (SpansU2{0, maxU64}));
   EXPECT_EQ(
-    (Constraint{GeS, {Literal(std::numeric_limits<int64_t>::max())}}.getSpan()),
-    (Span<IU64>{maxI64, maxI64}));
+    (Constraint{GeS, {Literal(std::numeric_limits<int64_t>::max())}}.getSpans()),
+    (SpansU2{maxI64, maxI64}));
 
   // GeU (i32): [C, maxU32]
-  EXPECT_EQ((Constraint{GeU, {Literal(uint32_t(0))}}.getSpan()),
-            (Span<IU64>{IU64(0), maxU32}));
-  EXPECT_EQ((Constraint{GeU, {Literal(uint32_t(10))}}.getSpan()),
-            (Span<IU64>{IU64(10), maxU32}));
+  EXPECT_EQ((Constraint{GeU, {Literal(uint32_t(0))}}.getSpans()),
+            (SpansU2{0, maxU32}));
+  EXPECT_EQ((Constraint{GeU, {Literal(uint32_t(10))}}.getSpans()),
+            (SpansU2{10, maxU32}));
   EXPECT_EQ((Constraint{GeU, {Literal(std::numeric_limits<uint32_t>::max())}}
-               .getSpan()),
-            (Span<IU64>{maxU32, maxU32}));
+               .getSpans()),
+            (SpansU2{maxU32, maxU32}));
 
   // GeU (i64): [C, maxU64]
-  EXPECT_EQ((Constraint{GeU, {Literal(uint64_t(0))}}.getSpan()),
-            (Span<IU64>{IU64(0), maxU64}));
-  EXPECT_EQ((Constraint{GeU, {Literal(uint64_t(10))}}.getSpan()),
-            (Span<IU64>{IU64(10), maxU64}));
+  EXPECT_EQ((Constraint{GeU, {Literal(uint64_t(0))}}.getSpans()),
+            (SpansU2{0, maxU64}));
+  EXPECT_EQ((Constraint{GeU, {Literal(uint64_t(10))}}.getSpans()),
+            (SpansU2{10, maxU64}));
   EXPECT_EQ((Constraint{GeU, {Literal(std::numeric_limits<uint64_t>::max())}}
-               .getSpan()),
-            (Span<IU64>{maxU64, maxU64}));
+               .getSpans()),
+            (SpansU2{maxU64, maxU64}));
 }
 
-TEST(ConstraintTest, GetSpanType) {
-  const IU64 minI32(std::numeric_limits<int32_t>::min());
-  const IU64 minI32Plus1(std::numeric_limits<int32_t>::min() + 1);
+TEST(ConstraintTest, GetSpansType) {
+  const uint64_t minI32(uint32_t(std::numeric_limits<int32_t>::min()));
+  const uint64_t minI32Plus1(minI32 + 1);
 
-  const IU64 maxI32(std::numeric_limits<int32_t>::max());
-  const IU64 maxI32Minus1(std::numeric_limits<int32_t>::max() - 1);
+  const uint64_t maxI32(std::numeric_limits<int32_t>::max());
+  const uint64_t maxI32Minus1(maxI32 - 1);
 
-  const IU64 maxU32(std::numeric_limits<uint32_t>::max());
-  const IU64 maxU32Minus1(std::numeric_limits<uint32_t>::max() - 1);
+  const uint64_t maxU32(std::numeric_limits<uint32_t>::max());
+  const uint64_t maxU32Minus1(maxU32 - 1);
 
-  const IU64 minI64(std::numeric_limits<int64_t>::min());
-  const IU64 minI64Plus1(std::numeric_limits<int64_t>::min() + 1);
+  const uint64_t minI64(uint64_t(std::numeric_limits<int64_t>::min()));
+  const uint64_t minI64Plus1(minI64 + 1);
 
-  const IU64 maxI64(std::numeric_limits<int64_t>::max());
-  const IU64 maxI64Minus1(std::numeric_limits<int64_t>::max() - 1);
+  const uint64_t maxI64(std::numeric_limits<int64_t>::max());
+  const uint64_t maxI64Minus1(maxI64 - 1);
 
-  const IU64 maxU64(std::numeric_limits<uint64_t>::max());
-  const IU64 maxU64Minus1(std::numeric_limits<uint64_t>::max() - 1);
+  const uint64_t maxU64(std::numeric_limits<uint64_t>::max());
+  const uint64_t maxU64Minus1(maxU64 - 1);
 
-  // Providing the type to getSpan() doesn't help with certain things.
-  EXPECT_EQ((Constraint{Eq, {Index(0)}}.getSpan(Type::i32)), std::nullopt);
-  EXPECT_EQ((Constraint{Ne, {Index(1)}}.getSpan(Type::i64)), std::nullopt);
-  EXPECT_EQ((Constraint{GeU, {Index(2)}}.getSpan(Type::i32)), std::nullopt);
-  EXPECT_EQ((Constraint{GeS, {Index(0)}}.getSpan(Type::i64)), std::nullopt);
-  EXPECT_EQ((Constraint{LeU, {Index(1)}}.getSpan(Type::i64)), std::nullopt);
-  EXPECT_EQ((Constraint{LeS, {Index(2)}}.getSpan(Type::i32)), std::nullopt);
+  // Providing the type to getSpans() doesn't help with certain things.
+  EXPECT_EQ((Constraint{Eq, {Index(0)}}.getSpans(Type::i32)), std::nullopt);
+  EXPECT_EQ((Constraint{Ne, {Index(1)}}.getSpans(Type::i64)), std::nullopt);
+  EXPECT_EQ((Constraint{GeU, {Index(2)}}.getSpans(Type::i32)), std::nullopt);
+  EXPECT_EQ((Constraint{GeS, {Index(0)}}.getSpans(Type::i64)), std::nullopt);
+  EXPECT_EQ((Constraint{LeU, {Index(1)}}.getSpans(Type::i64)), std::nullopt);
+  EXPECT_EQ((Constraint{LeS, {Index(2)}}.getSpans(Type::i32)), std::nullopt);
 
   // But it does help with others: x < y means x cannot be MAX_INT, so we can
   // report a *proven* span, if not an exact one.
-  EXPECT_EQ((Constraint{LtS, {Index(0)}}.getProvenSpan(Type::i32)),
-            (Span<IU64>{minI32, maxI32Minus1}));
-  EXPECT_EQ((Constraint{LtS, {Index(1)}}.getProvenSpan(Type::i64)),
-            (Span<IU64>{minI64, maxI64Minus1}));
-
-  EXPECT_EQ((Constraint{LtU, {Index(2)}}.getProvenSpan(Type::i32)),
-            (Span<IU64>{0, maxU32Minus1}));
-  EXPECT_EQ((Constraint{LtU, {Index(0)}}.getProvenSpan(Type::i64)),
-            (Span<IU64>{0, maxU64Minus1}));
-
-  EXPECT_EQ((Constraint{GtS, {Index(1)}}.getProvenSpan(Type::i32)),
-            (Span<IU64>{minI32Plus1, maxI32}));
-  EXPECT_EQ((Constraint{GtS, {Index(2)}}.getProvenSpan(Type::i64)),
-            (Span<IU64>{minI64Plus1, maxI64}));
-
-  EXPECT_EQ((Constraint{GtU, {Index(0)}}.getProvenSpan(Type::i32)),
-            (Span<IU64>{1, maxU32}));
-  EXPECT_EQ((Constraint{GtU, {Index(1)}}.getProvenSpan(Type::i64)),
-            (Span<IU64>{1, maxU64}));
+  EXPECT_EQ((Constraint{LtS, {Index(0)}}.getProvenSpans(Type::i32)),
+            (SpansU2{0, maxI32Minus1, minI32, maxU32}));
+  EXPECT_EQ((Constraint{LtS, {Index(1)}}.getProvenSpans(Type::i64)),
+            (SpansU2{0, maxI64Minus1, minI64, maxU64}));
+
+  EXPECT_EQ((Constraint{LtU, {Index(2)}}.getProvenSpans(Type::i32)),
+            (SpansU2{0, maxU32Minus1}));
+  EXPECT_EQ((Constraint{LtU, {Index(0)}}.getProvenSpans(Type::i64)),
+            (SpansU2{0, maxU64Minus1}));
+
+  EXPECT_EQ((Constraint{GtS, {Index(1)}}.getProvenSpans(Type::i32)),
+            (SpansU2{0, maxI32, minI32Plus1, maxU32}));
+  EXPECT_EQ((Constraint{GtS, {Index(2)}}.getProvenSpans(Type::i64)),
+            (SpansU2{0, maxI64, minI64Plus1, maxU64}));
+
+  EXPECT_EQ((Constraint{GtU, {Index(0)}}.getProvenSpans(Type::i32)),
+            (SpansU2{1, maxU32}));
+  EXPECT_EQ((Constraint{GtU, {Index(1)}}.getProvenSpans(Type::i64)),
+            (SpansU2{1, maxU64}));
 
   // But all the last things are impossible with an exact span.
-  EXPECT_EQ((Constraint{LtS, {Index(0)}}.getSpan(Type::i32)), std::nullopt);
-  EXPECT_EQ((Constraint{LtS, {Index(1)}}.getSpan(Type::i64)), std::nullopt);
-  EXPECT_EQ((Constraint{LtU, {Index(2)}}.getSpan(Type::i32)), std::nullopt);
-  EXPECT_EQ((Constraint{LtU, {Index(0)}}.getSpan(Type::i64)), std::nullopt);
-  EXPECT_EQ((Constraint{GtS, {Index(1)}}.getSpan(Type::i32)), std::nullopt);
-  EXPECT_EQ((Constraint{GtS, {Index(2)}}.getSpan(Type::i64)), std::nullopt);
-  EXPECT_EQ((Constraint{GtU, {Index(0)}}.getSpan(Type::i32)), std::nullopt);
-  EXPECT_EQ((Constraint{GtU, {Index(1)}}.getSpan(Type::i64)), std::nullopt);
+  EXPECT_EQ((Constraint{LtS, {Index(0)}}.getSpans(Type::i32)), std::nullopt);
+  EXPECT_EQ((Constraint{LtS, {Index(1)}}.getSpans(Type::i64)), std::nullopt);
+  EXPECT_EQ((Constraint{LtU, {Index(2)}}.getSpans(Type::i32)), std::nullopt);
+  EXPECT_EQ((Constraint{LtU, {Index(0)}}.getSpans(Type::i64)), std::nullopt);
+  EXPECT_EQ((Constraint{GtS, {Index(1)}}.getSpans(Type::i32)), std::nullopt);
+  EXPECT_EQ((Constraint{GtS, {Index(2)}}.getSpans(Type::i64)), std::nullopt);
+  EXPECT_EQ((Constraint{GtU, {Index(0)}}.getSpans(Type::i32)), std::nullopt);
+  EXPECT_EQ((Constraint{GtU, {Index(1)}}.getSpans(Type::i64)), std::nullopt);
 
   // Proven spans are otherwise like normal ones.
-  EXPECT_EQ((Constraint{Eq, {Literal(int32_t(42))}}.getProvenSpan()),
-            (Span<IU64>{42, 42}));
+  EXPECT_EQ((Constraint{Eq, {Literal(int32_t(42))}}.getProvenSpans()),
+            (SpansU2{42, 42}));
 }
 
 TEST(ConstraintTest, SpanOptimizations) {
@@ -1092,8 +1114,8 @@ TEST(ConstraintTest, SpanOptimizations) {
   Constraint lts200{LtS, {Literal(int32_t(200))}};
   EXPECT_EQ(AndedConstraintSet{lts100}.proves(lts200), True);
 
-  // Mixing signed and unsigned works fine: x in [0, 100] (x <= 100 unsigned)
-  // proves x in [-MIN_INT, 200] (x < 200 signed) is true.
+  // Mixing signed and unsigned works fine: x in [0, 100] (x < 100 unsigned)
+  // proves x < 200 signed is true.
   Constraint leu100{LtU, {Literal(int32_t(100))}};
   EXPECT_EQ(AndedConstraintSet{leu100}.proves(lts200), True);
 
@@ -1165,13 +1187,13 @@ TEST(ConstraintTest, EmptySpanContradiction) {
 
 TEST(ConstraintTest, GetSpanFloat) {
   // Non-integer types do not cause errors.
-  EXPECT_EQ((Constraint{Eq, {Literal(float(3.14159))}}.getSpan()),
+  EXPECT_EQ((Constraint{Eq, {Literal(float(3.14159))}}.getSpans()),
             std::nullopt);
 }
 
 TEST(ConstraintTest, GetSpanGC) {
   // Reference types do not cause errors.
-  EXPECT_EQ((Constraint{Eq, {Literal::makeNull(HeapType::eq)}}.getSpan()),
+  EXPECT_EQ((Constraint{Eq, {Literal::makeNull(HeapType::eq)}}.getSpans()),
             std::nullopt);
 }
 
@@ -1206,7 +1228,7 @@ TEST(ConstraintTest, SignedUnsignedLessMix) {
   Constraint ltu_minus10{LtU, {Literal(int32_t(-10))}};
   // x < -10 signed means all the numbers with the high/sign bit set, except for
   // -1 to -10 (which are the very highest in unsigned terms), that is,
-  // [1, large number] in the unsigned representation of bits. x < -10
+  // [minI32, large number] in the unsigned representation of bits. x < -10
   // *un*signed is similar, but *does* include 0, so the unsigned one does not
   // prove the signed.
   EXPECT_EQ(AndedConstraintSet{lts_minus10}.proves(ltu_minus10), True);
@@ -1232,7 +1254,20 @@ TEST(ConstraintTest, SignedUnsignedMoreMix) {
   EXPECT_EQ(AndedConstraintSet{gts10}.proves(gtu10), True);
   EXPECT_EQ(AndedConstraintSet{gtu10}.proves(gts10), Unknown);
 
-  // TODO: add negative cases
+  // Negative cases: x > -10 signed and unsigned.
+  Constraint gts_minus10{GtS, {Literal(int32_t(-10))}};
+  Constraint gtu_minus10{GtU, {Literal(int32_t(-10))}};
+  // x > -10 unsigned means values in [uint32_t(-9), maxU32], which are all
+  // signed negative numbers > -10. So unsigned proves signed.
+  EXPECT_EQ(AndedConstraintSet{gtu_minus10}.proves(gts_minus10), True);
+  // x > -10 signed includes non-negative numbers like 0, which are not > -10 unsigned.
+  EXPECT_EQ(AndedConstraintSet{gts_minus10}.proves(gtu_minus10), Unknown);
+
+  // Cross comparisons:
+  EXPECT_EQ(AndedConstraintSet{gtu10}.proves(gts_minus10), Unknown);
+  EXPECT_EQ(AndedConstraintSet{gts_minus10}.proves(gtu10), Unknown);
+  EXPECT_EQ(AndedConstraintSet{gts10}.proves(gtu_minus10), False);
+  EXPECT_EQ(AndedConstraintSet{gtu_minus10}.proves(gts10), False);
 }
 
 TEST(ConstraintTest, SignedUnsignedLessAndMoreMix) {
@@ -1247,5 +1282,102 @@ TEST(ConstraintTest, SignedUnsignedLessAndMoreMix) {
   EXPECT_EQ(AndedConstraintSet{gts10}.proves(ltu10), False);
   EXPECT_EQ(AndedConstraintSet{gtu10}.proves(lts10), Unknown);
 
-  // TODO: add negative cases
+  // Negative cases:
+  Constraint lts_minus10{LtS, {Literal(int32_t(-10))}};
+  Constraint ltu_minus10{LtU, {Literal(int32_t(-10))}};
+  Constraint gts_minus10{GtS, {Literal(int32_t(-10))}};
+  Constraint gtu_minus10{GtU, {Literal(int32_t(-10))}};
+
+  EXPECT_EQ(AndedConstraintSet{lts_minus10}.proves(gtu_minus10), False);
+  EXPECT_EQ(AndedConstraintSet{gtu_minus10}.proves(lts_minus10), False);
+  EXPECT_EQ(AndedConstraintSet{lts_minus10}.proves(gts_minus10), False);
+  EXPECT_EQ(AndedConstraintSet{gts_minus10}.proves(lts_minus10), False);
+
+  EXPECT_EQ(AndedConstraintSet{ltu_minus10}.proves(gts_minus10), Unknown);
+  EXPECT_EQ(AndedConstraintSet{gts_minus10}.proves(ltu_minus10), Unknown);
+  EXPECT_EQ(AndedConstraintSet{ltu_minus10}.proves(gtu_minus10), False);
+  EXPECT_EQ(AndedConstraintSet{gtu_minus10}.proves(ltu_minus10), False);
+
+  // Cross mixed cases:
+  EXPECT_EQ(AndedConstraintSet{lts_minus10}.proves(gtu10), True);
+  EXPECT_EQ(AndedConstraintSet{gtu10}.proves(lts_minus10), Unknown);
+
+  EXPECT_EQ(AndedConstraintSet{gtu_minus10}.proves(lts10), True);
+  EXPECT_EQ(AndedConstraintSet{lts10}.proves(gtu_minus10), Unknown);
+
+  EXPECT_EQ(AndedConstraintSet{ltu10}.proves(gts_minus10), True);
+  EXPECT_EQ(AndedConstraintSet{gts_minus10}.proves(ltu10), Unknown);
+
+  EXPECT_EQ(AndedConstraintSet{gts10}.proves(ltu_minus10), True);
+  EXPECT_EQ(AndedConstraintSet{ltu_minus10}.proves(gts10), Unknown);
+}
+
+TEST(ConstraintTest, SignedUnsigned64) {
+  // Same sign/unsign mixing tests on 64-bit integers.
+  Constraint eq5{Eq, {Literal(int64_t(5))}};
+  Constraint lts10{LtS, {Literal(int64_t(10))}};
+  Constraint ltu10{LtU, {Literal(int64_t(10))}};
+  EXPECT_EQ(AndedConstraintSet{eq5}.proves(lts10), True);
+  EXPECT_EQ(AndedConstraintSet{eq5}.proves(ltu10), True);
+
+  Constraint lts_minus10{LtS, {Literal(int64_t(-10))}};
+  Constraint ltu_minus10{LtU, {Literal(int64_t(-10))}};
+  EXPECT_EQ(AndedConstraintSet{eq5}.proves(lts_minus10), False);
+  EXPECT_EQ(AndedConstraintSet{eq5}.proves(ltu_minus10), True);
+
+  EXPECT_EQ(AndedConstraintSet{lts10}.proves(ltu10), Unknown);
+  EXPECT_EQ(AndedConstraintSet{ltu10}.proves(lts10), True);
+
+  EXPECT_EQ(AndedConstraintSet{lts_minus10}.proves(ltu_minus10), True);
+  EXPECT_EQ(AndedConstraintSet{ltu_minus10}.proves(lts_minus10), Unknown);
+
+  EXPECT_EQ(AndedConstraintSet{lts_minus10}.proves(ltu10), False);
+  EXPECT_EQ(AndedConstraintSet{lts10}.proves(ltu_minus10), Unknown);
+
+  Constraint gts10{GtS, {Literal(int64_t(10))}};
+  Constraint gtu10{GtU, {Literal(int64_t(10))}};
+  EXPECT_EQ(AndedConstraintSet{gts10}.proves(gtu10), True);
+  EXPECT_EQ(AndedConstraintSet{gtu10}.proves(gts10), Unknown);
+
+  Constraint gts_minus10{GtS, {Literal(int64_t(-10))}};
+  Constraint gtu_minus10{GtU, {Literal(int64_t(-10))}};
+  EXPECT_EQ(AndedConstraintSet{gtu_minus10}.proves(gts_minus10), True);
+  EXPECT_EQ(AndedConstraintSet{gts_minus10}.proves(gtu_minus10), Unknown);
+
+  EXPECT_EQ(AndedConstraintSet{lts_minus10}.proves(gtu10), True);
+  EXPECT_EQ(AndedConstraintSet{gtu_minus10}.proves(lts10), True);
+  EXPECT_EQ(AndedConstraintSet{ltu10}.proves(gts_minus10), True);
+  EXPECT_EQ(AndedConstraintSet{gts10}.proves(ltu_minus10), True);
+}
+
+TEST(ConstraintTest, ProvenanceInference) {
+  // x < y proves x != MAX_INT, so x == MAX_INT is False.
+  Constraint ltsLocal{LtS, {Index(0)}};
+  Constraint eqMaxI32{Eq, {Literal(std::numeric_limits<int32_t>::max())}};
+  EXPECT_EQ(AndedConstraintSet{ltsLocal}.proves(eqMaxI32), False);
+
+  Constraint gtsMaxMinus1{
+    GtS, {Literal(std::numeric_limits<int32_t>::max() - 1)}};
+  EXPECT_EQ(AndedConstraintSet{ltsLocal}.proves(gtsMaxMinus1), False);
+
+  // x > y proves x != MIN_INT, so x == MIN_INT is False.
+  Constraint gtsLocal{GtS, {Index(0)}};
+  Constraint eqMinI32{Eq, {Literal(std::numeric_limits<int32_t>::min())}};
+  EXPECT_EQ(AndedConstraintSet{gtsLocal}.proves(eqMinI32), False);
+
+  Constraint lesMinI32{LeS, {Literal(std::numeric_limits<int32_t>::min())}};
+  EXPECT_EQ(AndedConstraintSet{gtsLocal}.proves(lesMinI32), False);
+
+  // x <_u y proves x != MAX_UINT, so x == MAX_UINT is False.
+  Constraint ltuLocal{LtU, {Index(0)}};
+  Constraint eqMaxU32{Eq, {Literal(std::numeric_limits<uint32_t>::max())}};
+  EXPECT_EQ(AndedConstraintSet{ltuLocal}.proves(eqMaxU32), False);
+
+  // x >_u y proves x != 0, so x == 0 is False.
+  Constraint gtuLocal{GtU, {Index(0)}};
+  Constraint eqZeroU32{Eq, {Literal(uint32_t(0))}};
+  EXPECT_EQ(AndedConstraintSet{gtuLocal}.proves(eqZeroU32), False);
+
+  Constraint leuZeroU32{LeU, {Literal(uint32_t(0))}};
+  EXPECT_EQ(AndedConstraintSet{gtuLocal}.proves(leuZeroU32), False);
 }
diff --git a/test/gtest/span.cpp b/test/gtest/span.cpp
index f05fd80e2ff..85d6cec2946 100644
--- a/test/gtest/span.cpp
+++ b/test/gtest/span.cpp
@@ -18,7 +18,6 @@
 #include <limits>
 #include <sstream>
 
-#include "support/iu64.h"
 #include "support/span.h"
 #include "gtest/gtest.h"
 
@@ -185,178 +184,164 @@ TEST(SpanTest, StreamOutput) {
 }
 
 // ============================================================================
-// Span<IU64> tests (corner cases, sign mixing, large range)
+// Spans<T, N> and SpansU2 tests
 // ============================================================================
 
-TEST(SpanIU64Test, FullAndLimits) {
-  EXPECT_EQ(Span<IU64>::Min, IU64(std::numeric_limits<int64_t>::min()));
-  EXPECT_EQ(Span<IU64>::Max, IU64(std::numeric_limits<uint64_t>::max()));
-
-  Span<IU64> full = Span<IU64>::full();
-  EXPECT_TRUE(full.isFull());
-  EXPECT_FALSE(full.isEmpty());
-  EXPECT_EQ(full.min, IU64(std::numeric_limits<int64_t>::min()));
-  EXPECT_EQ(full.max, IU64(std::numeric_limits<uint64_t>::max()));
-
-  // Default constructed span is full
-  Span<IU64> def;
-  EXPECT_TRUE(def.isFull());
-  EXPECT_FALSE(def.isEmpty());
-  EXPECT_EQ(def, full);
+TEST(SpansTest, Construction) {
+  SpansU2 empty;
+  EXPECT_TRUE(empty.empty());
+  EXPECT_EQ(empty.size(), 0u);
+
+  SpansU2 fromSpans{Span<uint64_t>(0, 10), Span<uint64_t>(20, 30)};
+  EXPECT_FALSE(fromSpans.empty());
+  EXPECT_EQ(fromSpans.size(), 2u);
+  EXPECT_EQ(fromSpans[0], Span<uint64_t>(0, 10));
+  EXPECT_EQ(fromSpans[1], Span<uint64_t>(20, 30));
+
+  SpansU2 fromCoords{0, 10, 20, 30};
+  EXPECT_EQ(fromCoords.size(), 2u);
+  EXPECT_EQ(fromCoords[0], Span<uint64_t>(0, 10));
+  EXPECT_EQ(fromCoords[1], Span<uint64_t>(20, 30));
+
+  SpansU2 single{5, 15};
+  EXPECT_EQ(single.size(), 1u);
+  EXPECT_EQ(single[0], Span<uint64_t>(5, 15));
 }
 
-TEST(SpanIU64Test, Empty) {
-  Span<IU64> empty = Span<IU64>::empty();
-  EXPECT_TRUE(empty.isEmpty());
-  EXPECT_FALSE(empty.isFull());
-
-  Span<IU64> empty2{IU64(100), IU64(-100)};
-  EXPECT_TRUE(empty2.isEmpty());
-  EXPECT_FALSE(empty2.isFull());
-  EXPECT_EQ(empty, empty2);
+TEST(SpansTest, Equality) {
+  EXPECT_EQ(SpansU2(), SpansU2());
+  EXPECT_EQ((SpansU2{0, 10}), (SpansU2{0, 10}));
+  EXPECT_EQ((SpansU2{0, 10, 20, 30}), (SpansU2{0, 10, 20, 30}));
 
-  Span<IU64> empty3{IU64(uint64_t(1)), IU64(int64_t(-1))};
-  EXPECT_TRUE(empty3.isEmpty());
-  EXPECT_EQ(empty, empty3);
+  EXPECT_NE((SpansU2{0, 10}), SpansU2());
+  EXPECT_NE((SpansU2{0, 10}), (SpansU2{0, 11}));
+  EXPECT_NE((SpansU2{0, 10}), (SpansU2{0, 10, 20, 30}));
 }
 
-TEST(SpanIU64Test, SingletonsAtExtremes) {
-  // Min int64 singleton
-  Span<IU64> minI64{IU64(std::numeric_limits<int64_t>::min()),
-                    IU64(std::numeric_limits<int64_t>::min())};
-  EXPECT_FALSE(minI64.isEmpty());
-  EXPECT_FALSE(minI64.isFull());
-  EXPECT_EQ(minI64.min, IU64(std::numeric_limits<int64_t>::min()));
-  EXPECT_EQ(minI64.max, IU64(std::numeric_limits<int64_t>::min()));
-
-  // -1 singleton
-  Span<IU64> negOne{IU64(-1), IU64(-1)};
-  EXPECT_FALSE(negOne.isEmpty());
-
-  // 0 singleton
-  Span<IU64> zero{IU64(0), IU64(0)};
-  EXPECT_FALSE(zero.isEmpty());
-
-  // 1 singleton
-  Span<IU64> one{IU64(1), IU64(1)};
-  EXPECT_FALSE(one.isEmpty());
-
-  // Max int64 singleton
-  Span<IU64> maxI64{IU64(std::numeric_limits<int64_t>::max()),
-                    IU64(std::numeric_limits<int64_t>::max())};
-  EXPECT_FALSE(maxI64.isEmpty());
-
-  // 2^63 singleton (above int64_t max, into uint64_t territory)
-  Span<IU64> highBit{IU64(uint64_t(1) << 63), IU64(uint64_t(1) << 63)};
-  EXPECT_FALSE(highBit.isEmpty());
-
-  // Max uint64 singleton
-  Span<IU64> maxU64{IU64(std::numeric_limits<uint64_t>::max()),
-                    IU64(std::numeric_limits<uint64_t>::max())};
-  EXPECT_FALSE(maxU64.isEmpty());
-}
-
-TEST(SpanIU64Test, CrossingZero) {
-  Span<IU64> span{IU64(-10), IU64(10)};
-  EXPECT_FALSE(span.isEmpty());
-  EXPECT_FALSE(span.isFull());
-
-  // Contains points inside
-  EXPECT_TRUE(span.contains(Span<IU64>(IU64(-10), IU64(-10))));
-  EXPECT_TRUE(span.contains(Span<IU64>(IU64(-5), IU64(5))));
-  EXPECT_TRUE(span.contains(Span<IU64>(IU64(0), IU64(0))));
-  EXPECT_TRUE(span.contains(Span<IU64>(IU64(10), IU64(10))));
-
-  // Does not contain points outside
-  EXPECT_FALSE(span.contains(Span<IU64>(IU64(-11), IU64(-11))));
-  EXPECT_FALSE(span.contains(Span<IU64>(IU64(11), IU64(11))));
-  EXPECT_FALSE(span.contains(Span<IU64>(IU64(-15), IU64(5))));
-  EXPECT_FALSE(span.contains(Span<IU64>(IU64(-5), IU64(15))));
-}
+TEST(SpansTest, HasOverlap) {
+  SpansU2 empty;
+  SpansU2 s1{0, 10, 20, 30};
+  SpansU2 s2{5, 15};
+  SpansU2 s3{25, 35};
+  SpansU2 s4{11, 19};
+  SpansU2 s5{31, 40};
+  SpansU2 s6{10, 20};
 
-TEST(SpanIU64Test, NegativeAndPositiveIntersections) {
-  Span<IU64> neg{IU64(-100), IU64(-10)};
-  Span<IU64> pos{IU64(10), IU64(100)};
+  EXPECT_FALSE(empty.hasOverlap(s1));
+  EXPECT_FALSE(s1.hasOverlap(empty));
+  EXPECT_FALSE(empty.hasOverlap(empty));
 
-  EXPECT_FALSE(neg.hasOverlap(pos));
-  EXPECT_FALSE(pos.hasOverlap(neg));
-  EXPECT_TRUE(neg.intersection(pos).isEmpty());
-  EXPECT_TRUE(pos.intersection(neg).isEmpty());
+  // Overlap with first span
+  EXPECT_TRUE(s1.hasOverlap(s2));
+  EXPECT_TRUE(s2.hasOverlap(s1));
 
-  Span<IU64> touchNegZero{IU64(-10), IU64(0)};
-  Span<IU64> touchZeroPos{IU64(0), IU64(10)};
-  EXPECT_TRUE(touchNegZero.hasOverlap(touchZeroPos));
-  EXPECT_EQ(touchNegZero.intersection(touchZeroPos),
-            Span<IU64>(IU64(0), IU64(0)));
+  // Overlap with second span
+  EXPECT_TRUE(s1.hasOverlap(s3));
+  EXPECT_TRUE(s3.hasOverlap(s1));
 
-  Span<IU64> overlap{IU64(-50), IU64(50)};
-  EXPECT_EQ(neg.intersection(overlap), Span<IU64>(IU64(-50), IU64(-10)));
-  EXPECT_EQ(pos.intersection(overlap), Span<IU64>(IU64(10), IU64(50)));
-}
+  // In the gap between spans: no overlap
+  EXPECT_FALSE(s1.hasOverlap(s4));
+  EXPECT_FALSE(s4.hasOverlap(s1));
 
-TEST(SpanIU64Test, SignedUnsignedBoundary) {
-  // Test around INT64_MAX and 2^63
-  int64_t maxI64 = std::numeric_limits<int64_t>::max();
-  uint64_t highBit = uint64_t(maxI64) + 1; // 0x8000000000000000ULL
+  // Beyond all spans: no overlap
+  EXPECT_FALSE(s1.hasOverlap(s5));
+  EXPECT_FALSE(s5.hasOverlap(s1));
 
-  Span<IU64> s1(IU64(maxI64 - 100), IU64(highBit + 50));
-  Span<IU64> s2(IU64(highBit), IU64(highBit + 100));
+  // Touching at endpoints: overlaps
+  EXPECT_TRUE(s1.hasOverlap(s6));
+  EXPECT_TRUE(s6.hasOverlap(s1));
+}
 
-  EXPECT_TRUE(s1.hasOverlap(s2));
-  EXPECT_EQ(s1.intersection(s2), Span<IU64>(IU64(highBit), IU64(highBit + 50)));
-
-  // Disjoint near 2^63 boundary
-  Span<IU64> s3{IU64(maxI64 - 200), IU64(maxI64)};
-  Span<IU64> s4{IU64(highBit + 1), IU64(highBit + 100)};
-  EXPECT_FALSE(s3.hasOverlap(s4));
-  EXPECT_TRUE(s3.intersection(s4).isEmpty());
-
-  // Adjacent touching at 2^63
-  Span<IU64> s5{IU64(maxI64), IU64(highBit)};
-  Span<IU64> s6{IU64(highBit), IU64(highBit + 10)};
-  EXPECT_TRUE(s5.hasOverlap(s6));
-  EXPECT_EQ(s5.intersection(s6), Span<IU64>(IU64(highBit), IU64(highBit)));
+TEST(SpansTest, Contains) {
+  SpansU2 empty;
+  SpansU2 s1{0, 100, 200, 300};
+  SpansU2 s2{10, 20};
+  SpansU2 s3{210, 220};
+  SpansU2 s4{10, 20, 210, 220};
+  SpansU2 s5{50, 150};
+  SpansU2 s6{10, 20, 250, 350};
+
+  // Empty contains empty, non-empty contains empty, empty does not contain non-empty
+  EXPECT_TRUE(empty.contains(empty));
+  EXPECT_TRUE(s1.contains(empty));
+  EXPECT_FALSE(empty.contains(s1));
+
+  // Identity
+  EXPECT_TRUE(s1.contains(s1));
+  EXPECT_TRUE(s2.contains(s2));
+
+  // Contained within first span
+  EXPECT_TRUE(s1.contains(s2));
+  EXPECT_FALSE(s2.contains(s1));
+
+  // Contained within second span
+  EXPECT_TRUE(s1.contains(s3));
+  EXPECT_FALSE(s3.contains(s1));
+
+  // Multiple spans each contained in one of s1's spans
+  EXPECT_TRUE(s1.contains(s4));
+  EXPECT_FALSE(s4.contains(s1));
+
+  // Straddles gap: not contained
+  EXPECT_FALSE(s1.contains(s5));
+
+  // One span contained, but second span extends past s1: not contained
+  EXPECT_FALSE(s1.contains(s6));
 }
 
-TEST(SpanIU64Test, ExtremeBoundaries) {
-  Span<IU64> minPart(IU64(std::numeric_limits<int64_t>::min()),
-                     IU64(std::numeric_limits<int64_t>::min() + 100));
-  Span<IU64> maxPart(IU64(std::numeric_limits<uint64_t>::max() - 100),
-                     IU64(std::numeric_limits<uint64_t>::max()));
-
-  EXPECT_FALSE(minPart.hasOverlap(maxPart));
-  EXPECT_TRUE(minPart.intersection(maxPart).isEmpty());
-
-  Span<IU64> full = Span<IU64>::full();
-  EXPECT_TRUE(full.contains(minPart));
-  EXPECT_TRUE(full.contains(maxPart));
-  EXPECT_EQ(full.intersection(minPart), minPart);
-  EXPECT_EQ(full.intersection(maxPart), maxPart);
-  EXPECT_TRUE(full.hasOverlap(minPart));
-  EXPECT_TRUE(full.hasOverlap(maxPart));
-
-  Span<IU64> allNeg(IU64(std::numeric_limits<int64_t>::min()), IU64(-1));
-  Span<IU64> allNonNeg(IU64(0), IU64(std::numeric_limits<uint64_t>::max()));
-
-  EXPECT_FALSE(allNeg.hasOverlap(allNonNeg));
-  EXPECT_TRUE(allNeg.intersection(allNonNeg).isEmpty());
-  EXPECT_TRUE(full.contains(allNeg));
-  EXPECT_TRUE(full.contains(allNonNeg));
+TEST(SpansTest, ExtremeBoundaries) {
+  uint64_t maxU64 = std::numeric_limits<uint64_t>::max();
+  uint64_t highBit = uint64_t(1) << 63;
+
+  SpansU2 lowPart{0, 100};
+  SpansU2 highPart{maxU64 - 100, maxU64};
+  SpansU2 midPart{highBit - 10, highBit + 10};
+
+  EXPECT_FALSE(lowPart.hasOverlap(highPart));
+  EXPECT_FALSE(highPart.hasOverlap(lowPart));
+  EXPECT_FALSE(lowPart.hasOverlap(midPart));
+  EXPECT_FALSE(midPart.hasOverlap(highPart));
+
+  SpansU2 split{0, 100, maxU64 - 100, maxU64};
+  EXPECT_TRUE(split.contains(lowPart));
+  EXPECT_TRUE(split.contains(highPart));
+  EXPECT_FALSE(split.contains(midPart));
+
+  SpansU2 fullRange{0, maxU64};
+  EXPECT_TRUE(fullRange.contains(split));
+  EXPECT_TRUE(fullRange.contains(lowPart));
+  EXPECT_TRUE(fullRange.contains(highPart));
+  EXPECT_TRUE(fullRange.contains(midPart));
 }
 
-TEST(SpanIU64Test, SetAndMutate) {
-  Span<IU64> s;
-  EXPECT_TRUE(s.isFull());
+TEST(SpansTest, Mutation) {
+  SpansU2 s;
+  EXPECT_TRUE(s.empty());
 
-  s.set(IU64(-12345));
-  EXPECT_FALSE(s.isFull());
-  EXPECT_FALSE(s.isEmpty());
-  EXPECT_EQ(s.min, IU64(-12345));
-  EXPECT_EQ(s.max, IU64(-12345));
+  s.push_back(Span<uint64_t>(10, 20));
+  EXPECT_EQ(s.size(), 1u);
+  EXPECT_EQ(s[0], Span<uint64_t>(10, 20));
 
-  s.setEmpty();
-  EXPECT_TRUE(s.isEmpty());
+  s.push_back(Span<uint64_t>(30, 40));
+  EXPECT_EQ(s.size(), 2u);
+  EXPECT_EQ(s[1], Span<uint64_t>(30, 40));
 
-  s.setFull();
-  EXPECT_TRUE(s.isFull());
+  s.pop_back();
+  EXPECT_EQ(s.size(), 1u);
+  EXPECT_EQ(s[0], Span<uint64_t>(10, 20));
+
+  s.clear();
+  EXPECT_TRUE(s.empty());
+}
+
+TEST(SpansTest, StreamOutput) {
+  auto toString = [](const auto& spans) {
+    std::ostringstream ss;
+    ss << spans;
+    return ss.str();
+  };
+
+  EXPECT_EQ(toString(SpansU2{}), "{empty}");
+  EXPECT_EQ(toString(SpansU2{1, 10}), "{[1, 10]}");
+  EXPECT_EQ(toString(SpansU2{1, 10, 20, 30}), "{[1, 10], [20, 30]}");
 }
diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index a2781211435..fcdb4058499 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -4743,7 +4743,10 @@
   ;; CHECK-NEXT:    )
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:   (drop
-  ;; CHECK-NEXT:    (i32.const 0)
+  ;; CHECK-NEXT:    (i32.gt_u
+  ;; CHECK-NEXT:     (local.get $0)
+  ;; CHECK-NEXT:     (i32.const -1992)
+  ;; CHECK-NEXT:    )
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
@@ -4756,7 +4759,10 @@
   ;; OPTIN-NEXT:    )
   ;; OPTIN-NEXT:   )
   ;; OPTIN-NEXT:   (drop
-  ;; OPTIN-NEXT:    (i32.const 0)
+  ;; OPTIN-NEXT:    (i32.gt_u
+  ;; OPTIN-NEXT:     (local.get $0)
+  ;; OPTIN-NEXT:     (i32.const -1992)
+  ;; OPTIN-NEXT:    )
   ;; OPTIN-NEXT:   )
   ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT: )
@@ -4768,10 +4774,9 @@
           (i32.const 1024)
         )
       )
-      ;; Here we know  $0 <_s 1024. This includes all numbers with the sign bit,
-      ;; which implies the following *unsigned* inequality is true, as it
-      ;; includes only ones with the high bit set.
-      ;; XXX FIXME the result is wrong atm
+      ;; Here we know  $0 <_s 1024. That includes non-negative numbers like 0 as
+      ;; well as negative numbers. The following *unsigned* inequality might or
+      ;; might not be true, so we optimize nothing.
       (drop
         (i32.gt_u
           (local.get $0)
@@ -4790,7 +4795,10 @@
   ;; CHECK-NEXT:    )
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:   (drop
-  ;; CHECK-NEXT:    (i32.const 0)
+  ;; CHECK-NEXT:    (i32.gt_u
+  ;; CHECK-NEXT:     (local.get $0)
+  ;; CHECK-NEXT:     (i32.const -1992)
+  ;; CHECK-NEXT:    )
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
@@ -4803,7 +4811,10 @@
   ;; OPTIN-NEXT:    )
   ;; OPTIN-NEXT:   )
   ;; OPTIN-NEXT:   (drop
-  ;; OPTIN-NEXT:    (i32.const 0)
+  ;; OPTIN-NEXT:    (i32.gt_u
+  ;; OPTIN-NEXT:     (local.get $0)
+  ;; OPTIN-NEXT:     (i32.const -1992)
+  ;; OPTIN-NEXT:    )
   ;; OPTIN-NEXT:   )
   ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT: )
@@ -4818,9 +4829,8 @@
       )
       ;; Here we know  $0 <=_s -1023. This includes most numbers with the sign
       ;; bit set, except for the lowest in absolute value. That implies the
-      ;; following *unsigned* inequality might or might not true, so we optimize
-      ;; nothing.
-      ;; XXX FIXME the result is wrong atm
+      ;; following *unsigned* inequality might or might not be true, so we
+      ;; optimize nothing.
       (drop
         (i32.gt_u
           (local.get $0)

From 8d6daf89e6e82000bf567d20013edab5cf4245bc Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 13:39:37 -0700
Subject: [PATCH 20/30] format

---
 src/support/span.h        |   7 +--
 test/gtest/constraint.cpp | 105 +++++++++++++++++++-------------------
 test/gtest/span.cpp       |   3 +-
 3 files changed, 58 insertions(+), 57 deletions(-)

diff --git a/src/support/span.h b/src/support/span.h
index c0cec022961..f5fe1240a41 100644
--- a/src/support/span.h
+++ b/src/support/span.h
@@ -126,9 +126,10 @@ struct Spans : public inplace_vector<Span<T>, N> {
       other.begin(), other.end(), [&](const Span<T>& otherSpan) {
         // Because our spans are assumed to be disjoint, exactly one of our
         // spans must contain otherSpan.
-        return std::any_of(this->begin(), this->end(), [&](const Span<T>& span) {
-          return span.contains(otherSpan);
-        });
+        return std::any_of(
+          this->begin(), this->end(), [&](const Span<T>& span) {
+            return span.contains(otherSpan);
+          });
       });
   }
 };
diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 9ce42e337ee..18a17e2f4a2 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -781,9 +781,9 @@ TEST(ConstraintTest, GetSpans) {
     (SpansU2{minI32, minI32}));
   EXPECT_EQ((Constraint{Eq, {Literal(uint32_t(0x80000000u))}}.getSpans()),
             (SpansU2{0x80000000u, 0x80000000u}));
-  EXPECT_EQ(
-    (Constraint{Eq, {Literal(std::numeric_limits<uint32_t>::max())}}.getSpans()),
-    (SpansU2{maxU32, maxU32}));
+  EXPECT_EQ((Constraint{Eq, {Literal(std::numeric_limits<uint32_t>::max())}}
+               .getSpans()),
+            (SpansU2{maxU32, maxU32}));
 
   // Eq (i64)
   EXPECT_EQ((Constraint{Eq, {Literal(int64_t(0))}}.getSpans()),
@@ -805,9 +805,9 @@ TEST(ConstraintTest, GetSpans) {
     (SpansU2{minI64, minI64}));
   EXPECT_EQ((Constraint{Eq, {Literal(uint64_t(uint64_t(1) << 63))}}.getSpans()),
             (SpansU2{minI64, minI64}));
-  EXPECT_EQ(
-    (Constraint{Eq, {Literal(std::numeric_limits<uint64_t>::max())}}.getSpans()),
-    (SpansU2{maxU64, maxU64}));
+  EXPECT_EQ((Constraint{Eq, {Literal(std::numeric_limits<uint64_t>::max())}}
+               .getSpans()),
+            (SpansU2{maxU64, maxU64}));
 
   // LtS (i32):
   EXPECT_EQ((Constraint{LtS, {Literal(int32_t(10))}}.getSpans()),
@@ -816,9 +816,9 @@ TEST(ConstraintTest, GetSpans) {
             (SpansU2{minI32, maxU32}));
   EXPECT_EQ((Constraint{LtS, {Literal(int32_t(-5))}}.getSpans()),
             (SpansU2{minI32, uint32_t(-6)}));
-  EXPECT_EQ(
-    (Constraint{LtS, {Literal(std::numeric_limits<int32_t>::max())}}.getSpans()),
-    (SpansU2{0, maxI32 - 1, minI32, maxU32}));
+  EXPECT_EQ((Constraint{LtS, {Literal(std::numeric_limits<int32_t>::max())}}
+               .getSpans()),
+            (SpansU2{0, maxI32 - 1, minI32, maxU32}));
   // LtS min signed (i32): empty span
   auto ltsMin32 =
     Constraint{LtS, {Literal(std::numeric_limits<int32_t>::min())}}.getSpans();
@@ -833,9 +833,9 @@ TEST(ConstraintTest, GetSpans) {
             (SpansU2{minI64, maxU64}));
   EXPECT_EQ((Constraint{LtS, {Literal(int64_t(-5))}}.getSpans()),
             (SpansU2{minI64, uint64_t(-6)}));
-  EXPECT_EQ(
-    (Constraint{LtS, {Literal(std::numeric_limits<int64_t>::max())}}.getSpans()),
-    (SpansU2{0, maxI64 - 1, minI64, maxU64}));
+  EXPECT_EQ((Constraint{LtS, {Literal(std::numeric_limits<int64_t>::max())}}
+               .getSpans()),
+            (SpansU2{0, maxI64 - 1, minI64, maxU64}));
   // LtS min signed (i64): empty span
   auto ltsMin64 =
     Constraint{LtS, {Literal(std::numeric_limits<int64_t>::min())}}.getSpans();
@@ -848,10 +848,9 @@ TEST(ConstraintTest, GetSpans) {
             (SpansU2{0, 9}));
   EXPECT_EQ((Constraint{LtU, {Literal(uint32_t(1))}}.getSpans()),
             (SpansU2{0, 0}));
-  EXPECT_EQ(
-    (Constraint{LtU, {Literal(std::numeric_limits<uint32_t>::max())}}
-       .getSpans()),
-    (SpansU2{0, maxU32 - 1}));
+  EXPECT_EQ((Constraint{LtU, {Literal(std::numeric_limits<uint32_t>::max())}}
+               .getSpans()),
+            (SpansU2{0, maxU32 - 1}));
   // LtU 0 (i32): empty span
   auto ltuZero32 = Constraint{LtU, {Literal(uint32_t(0))}}.getSpans();
   ASSERT_TRUE(ltuZero32.has_value());
@@ -861,10 +860,9 @@ TEST(ConstraintTest, GetSpans) {
   // LtU (i64): [0, C - 1]
   EXPECT_EQ((Constraint{LtU, {Literal(uint64_t(100))}}.getSpans()),
             (SpansU2{0, 99}));
-  EXPECT_EQ(
-    (Constraint{LtU, {Literal(std::numeric_limits<uint64_t>::max())}}
-       .getSpans()),
-    (SpansU2{0, maxU64 - 1}));
+  EXPECT_EQ((Constraint{LtU, {Literal(std::numeric_limits<uint64_t>::max())}}
+               .getSpans()),
+            (SpansU2{0, maxU64 - 1}));
   // LtU 0 (i64): empty span
   auto ltuZero64 = Constraint{LtU, {Literal(uint64_t(0))}}.getSpans();
   ASSERT_TRUE(ltuZero64.has_value());
@@ -878,12 +876,12 @@ TEST(ConstraintTest, GetSpans) {
             (SpansU2{0, 0, minI32, maxU32}));
   EXPECT_EQ((Constraint{LeS, {Literal(int32_t(-5))}}.getSpans()),
             (SpansU2{minI32, uint32_t(-5)}));
-  EXPECT_EQ(
-    (Constraint{LeS, {Literal(std::numeric_limits<int32_t>::min())}}.getSpans()),
-    (SpansU2{minI32, minI32}));
-  EXPECT_EQ(
-    (Constraint{LeS, {Literal(std::numeric_limits<int32_t>::max())}}.getSpans()),
-    (SpansU2{0, maxU32}));
+  EXPECT_EQ((Constraint{LeS, {Literal(std::numeric_limits<int32_t>::min())}}
+               .getSpans()),
+            (SpansU2{minI32, minI32}));
+  EXPECT_EQ((Constraint{LeS, {Literal(std::numeric_limits<int32_t>::max())}}
+               .getSpans()),
+            (SpansU2{0, maxU32}));
 
   // LeS (i64):
   EXPECT_EQ((Constraint{LeS, {Literal(int64_t(10))}}.getSpans()),
@@ -892,12 +890,12 @@ TEST(ConstraintTest, GetSpans) {
             (SpansU2{0, 0, minI64, maxU64}));
   EXPECT_EQ((Constraint{LeS, {Literal(int64_t(-5))}}.getSpans()),
             (SpansU2{minI64, uint64_t(-5)}));
-  EXPECT_EQ(
-    (Constraint{LeS, {Literal(std::numeric_limits<int64_t>::min())}}.getSpans()),
-    (SpansU2{minI64, minI64}));
-  EXPECT_EQ(
-    (Constraint{LeS, {Literal(std::numeric_limits<int64_t>::max())}}.getSpans()),
-    (SpansU2{0, maxU64}));
+  EXPECT_EQ((Constraint{LeS, {Literal(std::numeric_limits<int64_t>::min())}}
+               .getSpans()),
+            (SpansU2{minI64, minI64}));
+  EXPECT_EQ((Constraint{LeS, {Literal(std::numeric_limits<int64_t>::max())}}
+               .getSpans()),
+            (SpansU2{0, maxU64}));
 
   // LeU (i32): [0, C]
   EXPECT_EQ((Constraint{LeU, {Literal(uint32_t(0))}}.getSpans()),
@@ -926,9 +924,9 @@ TEST(ConstraintTest, GetSpans) {
             (SpansU2{0, maxI32, uint32_t(-4), maxU32}));
   EXPECT_EQ((Constraint{GtS, {Literal(int32_t(-1))}}.getSpans()),
             (SpansU2{0, maxI32}));
-  EXPECT_EQ(
-    (Constraint{GtS, {Literal(std::numeric_limits<int32_t>::min())}}.getSpans()),
-    (SpansU2{0, maxI32, minI32 + 1, maxU32}));
+  EXPECT_EQ((Constraint{GtS, {Literal(std::numeric_limits<int32_t>::min())}}
+               .getSpans()),
+            (SpansU2{0, maxI32, minI32 + 1, maxU32}));
   EXPECT_EQ((Constraint{GtS, {Literal(std::numeric_limits<int32_t>::max() - 1)}}
                .getSpans()),
             (SpansU2{maxI32, maxI32}));
@@ -948,9 +946,9 @@ TEST(ConstraintTest, GetSpans) {
             (SpansU2{0, maxI64, uint64_t(-4), maxU64}));
   EXPECT_EQ((Constraint{GtS, {Literal(int64_t(-1))}}.getSpans()),
             (SpansU2{0, maxI64}));
-  EXPECT_EQ(
-    (Constraint{GtS, {Literal(std::numeric_limits<int64_t>::min())}}.getSpans()),
-    (SpansU2{0, maxI64, minI64 + 1, maxU64}));
+  EXPECT_EQ((Constraint{GtS, {Literal(std::numeric_limits<int64_t>::min())}}
+               .getSpans()),
+            (SpansU2{0, maxI64, minI64 + 1, maxU64}));
   EXPECT_EQ((Constraint{GtS, {Literal(std::numeric_limits<int64_t>::max() - 1)}}
                .getSpans()),
             (SpansU2{maxI64, maxI64}));
@@ -1002,12 +1000,12 @@ TEST(ConstraintTest, GetSpans) {
             (SpansU2{0, maxI32, uint32_t(-5), maxU32}));
   EXPECT_EQ((Constraint{GeS, {Literal(int32_t(-1))}}.getSpans()),
             (SpansU2{0, maxI32, maxU32, maxU32}));
-  EXPECT_EQ(
-    (Constraint{GeS, {Literal(std::numeric_limits<int32_t>::min())}}.getSpans()),
-    (SpansU2{0, maxU32}));
-  EXPECT_EQ(
-    (Constraint{GeS, {Literal(std::numeric_limits<int32_t>::max())}}.getSpans()),
-    (SpansU2{maxI32, maxI32}));
+  EXPECT_EQ((Constraint{GeS, {Literal(std::numeric_limits<int32_t>::min())}}
+               .getSpans()),
+            (SpansU2{0, maxU32}));
+  EXPECT_EQ((Constraint{GeS, {Literal(std::numeric_limits<int32_t>::max())}}
+               .getSpans()),
+            (SpansU2{maxI32, maxI32}));
 
   // GeS (i64):
   EXPECT_EQ((Constraint{GeS, {Literal(int64_t(10))}}.getSpans()),
@@ -1018,12 +1016,12 @@ TEST(ConstraintTest, GetSpans) {
             (SpansU2{0, maxI64, uint64_t(-5), maxU64}));
   EXPECT_EQ((Constraint{GeS, {Literal(int64_t(-1))}}.getSpans()),
             (SpansU2{0, maxI64, maxU64, maxU64}));
-  EXPECT_EQ(
-    (Constraint{GeS, {Literal(std::numeric_limits<int64_t>::min())}}.getSpans()),
-    (SpansU2{0, maxU64}));
-  EXPECT_EQ(
-    (Constraint{GeS, {Literal(std::numeric_limits<int64_t>::max())}}.getSpans()),
-    (SpansU2{maxI64, maxI64}));
+  EXPECT_EQ((Constraint{GeS, {Literal(std::numeric_limits<int64_t>::min())}}
+               .getSpans()),
+            (SpansU2{0, maxU64}));
+  EXPECT_EQ((Constraint{GeS, {Literal(std::numeric_limits<int64_t>::max())}}
+               .getSpans()),
+            (SpansU2{maxI64, maxI64}));
 
   // GeU (i32): [C, maxU32]
   EXPECT_EQ((Constraint{GeU, {Literal(uint32_t(0))}}.getSpans()),
@@ -1260,7 +1258,8 @@ TEST(ConstraintTest, SignedUnsignedMoreMix) {
   // x > -10 unsigned means values in [uint32_t(-9), maxU32], which are all
   // signed negative numbers > -10. So unsigned proves signed.
   EXPECT_EQ(AndedConstraintSet{gtu_minus10}.proves(gts_minus10), True);
-  // x > -10 signed includes non-negative numbers like 0, which are not > -10 unsigned.
+  // x > -10 signed includes non-negative numbers like 0, which are not > -10
+  // unsigned.
   EXPECT_EQ(AndedConstraintSet{gts_minus10}.proves(gtu_minus10), Unknown);
 
   // Cross comparisons:
@@ -1356,8 +1355,8 @@ TEST(ConstraintTest, ProvenanceInference) {
   Constraint eqMaxI32{Eq, {Literal(std::numeric_limits<int32_t>::max())}};
   EXPECT_EQ(AndedConstraintSet{ltsLocal}.proves(eqMaxI32), False);
 
-  Constraint gtsMaxMinus1{
-    GtS, {Literal(std::numeric_limits<int32_t>::max() - 1)}};
+  Constraint gtsMaxMinus1{GtS,
+                          {Literal(std::numeric_limits<int32_t>::max() - 1)}};
   EXPECT_EQ(AndedConstraintSet{ltsLocal}.proves(gtsMaxMinus1), False);
 
   // x > y proves x != MIN_INT, so x == MIN_INT is False.
diff --git a/test/gtest/span.cpp b/test/gtest/span.cpp
index 85d6cec2946..26296d5e2a8 100644
--- a/test/gtest/span.cpp
+++ b/test/gtest/span.cpp
@@ -261,7 +261,8 @@ TEST(SpansTest, Contains) {
   SpansU2 s5{50, 150};
   SpansU2 s6{10, 20, 250, 350};
 
-  // Empty contains empty, non-empty contains empty, empty does not contain non-empty
+  // Empty contains empty, non-empty contains empty, empty does not contain
+  // non-empty
   EXPECT_TRUE(empty.contains(empty));
   EXPECT_TRUE(s1.contains(empty));
   EXPECT_FALSE(empty.contains(s1));

From dcb4d4bc9106f5d61ab020e1dc64a0bc16e34319 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 14:43:06 -0700
Subject: [PATCH 21/30] work

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

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 19c6c5b11fd..bcb3650b345 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -41,7 +41,8 @@ getSpansInternal(const Constraint& c, std::optional<Type> type, bool exact) {
     return {};
   }
 
-  // Maximum values, as represented as uint64_t's.
+  // Maximum values, as represented as uint64_t's. We generate spans on unsigned
+  // values, converting signed ones to their unsigned representations.
   uint64_t maxUnsigned = type && *type == Type::i32
                            ? std::numeric_limits<uint32_t>::max()
                            : std::numeric_limits<uint64_t>::max();

From 7e00a983581d2f39ba2b83548ca526efa7787a09 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 15:05:13 -0700
Subject: [PATCH 22/30] test

---
 test/gtest/constraint.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 18a17e2f4a2..3a82e11defc 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -915,6 +915,8 @@ TEST(ConstraintTest, GetSpans) {
                .getSpans()),
             (SpansU2{0, maxU64}));
 
+waka
+
   // GtS (i32):
   EXPECT_EQ((Constraint{GtS, {Literal(int32_t(10))}}.getSpans()),
             (SpansU2{11, maxI32}));
@@ -1227,8 +1229,8 @@ TEST(ConstraintTest, SignedUnsignedLessMix) {
   // x < -10 signed means all the numbers with the high/sign bit set, except for
   // -1 to -10 (which are the very highest in unsigned terms), that is,
   // [minI32, large number] in the unsigned representation of bits. x < -10
-  // *un*signed is similar, but *does* include 0, so the unsigned one does not
-  // prove the signed.
+  // *un*signed does actually include 0 and other values, so the unsigned one
+  // does not prove the signed.
   EXPECT_EQ(AndedConstraintSet{lts_minus10}.proves(ltu_minus10), True);
   EXPECT_EQ(AndedConstraintSet{ltu_minus10}.proves(lts_minus10), Unknown);
 

From 19037712533b891f02b6d15879d50066ba3ff7dc Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 15:05:20 -0700
Subject: [PATCH 23/30] test

---
 test/gtest/constraint.cpp | 2 --
 1 file changed, 2 deletions(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 3a82e11defc..eb85d3f20b2 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -915,8 +915,6 @@ TEST(ConstraintTest, GetSpans) {
                .getSpans()),
             (SpansU2{0, maxU64}));
 
-waka
-
   // GtS (i32):
   EXPECT_EQ((Constraint{GtS, {Literal(int32_t(10))}}.getSpans()),
             (SpansU2{11, maxI32}));

From 351660f8b46e90b87e6446edda256b7f2bcb6954 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 25 Aug 2026 15:20:08 -0700
Subject: [PATCH 24/30] test

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

diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index fcdb4058499..822c365afb3 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -4824,7 +4824,7 @@
       (br_if $block
         (i32.gt_s
           (local.get $0)
-         (i32.const -1023) ;; this changed
+          (i32.const -1023) ;; this changed
         )
       )
       ;; Here we know  $0 <=_s -1023. This includes most numbers with the sign
@@ -4839,4 +4839,49 @@
       )
     )
   )
+
+  ;; CHECK:      (func $sign-unsigned-less-more-mix-3-yes (type $0) (param $0 i32)
+  ;; CHECK-NEXT:  (block $block
+  ;; CHECK-NEXT:   (br_if $block
+  ;; CHECK-NEXT:    (i32.gt_s
+  ;; CHECK-NEXT:     (local.get $0)
+  ;; CHECK-NEXT:     (i32.const -4096)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (drop
+  ;; CHECK-NEXT:    (i32.const 0)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $sign-unsigned-less-more-mix-3-yes (type $0) (param $0 i32)
+  ;; OPTIN-NEXT:  (block $block
+  ;; OPTIN-NEXT:   (br_if $block
+  ;; OPTIN-NEXT:    (i32.gt_s
+  ;; OPTIN-NEXT:     (local.get $0)
+  ;; OPTIN-NEXT:     (i32.const -4096)
+  ;; OPTIN-NEXT:    )
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (drop
+  ;; OPTIN-NEXT:    (i32.const 0)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $sign-unsigned-less-more-mix-3-yes (param $0 i32)
+    ;; Similar to the above, but the 1024 was replaced by -4096.
+    (block $block
+      (br_if $block
+        (i32.gt_s
+          (local.get $0)
+          (i32.const -4096) ;; this changed
+        )
+      )
+      ;; Now we can optimize: there is no overlap possible, so this is 0.
+      (drop
+        (i32.gt_u
+          (local.get $0)
+          (i32.const -1992)
+        )
+      )
+    )
+  )
 )

From 42945c0304beec938bc1a4a34c681dc396ab547f Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Wed, 26 Aug 2026 09:00:12 -0700
Subject: [PATCH 25/30] typo

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

diff --git a/src/support/span.h b/src/support/span.h
index f5fe1240a41..80a06b1600c 100644
--- a/src/support/span.h
+++ b/src/support/span.h
@@ -136,7 +136,7 @@ struct Spans : public inplace_vector<Span<T>, N> {
 
 // A useful set of 2 spans that can contain any integer value. 2 spans is enough
 // to contain spans for any inequality, signed or unsigned: we represent numbers
-// as unsigned internally, and so e.g. signed x < 10 ends up as two disjoint
+// as unsigned internally, and so e.g. signed x <= 10 ends up as two disjoint
 // spans, [0..10] and [2^32..MAX_INT].
 using SpansU2 = Spans<uint64_t, 2>;
 

From 5465232de949fd600ed69dddb423e5d9824f1e92 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Wed, 26 Aug 2026 09:00:42 -0700
Subject: [PATCH 26/30] typo

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

diff --git a/src/support/span.h b/src/support/span.h
index 80a06b1600c..43f3bde5c18 100644
--- a/src/support/span.h
+++ b/src/support/span.h
@@ -137,7 +137,7 @@ struct Spans : public inplace_vector<Span<T>, N> {
 // A useful set of 2 spans that can contain any integer value. 2 spans is enough
 // to contain spans for any inequality, signed or unsigned: we represent numbers
 // as unsigned internally, and so e.g. signed x <= 10 ends up as two disjoint
-// spans, [0..10] and [2^32..MAX_INT].
+// spans, [0..10] and [2^31..MAX_INT].
 using SpansU2 = Spans<uint64_t, 2>;
 
 template<typename T>

From 1f9b43c7b34ca98e0b1addeb3bd219484c188cfe Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Wed, 26 Aug 2026 14:05:52 -0700
Subject: [PATCH 27/30] avoid Most Vexing Parse

---
 test/gtest/constraint.cpp | 36 ++++++++++++++++++------------------
 1 file changed, 18 insertions(+), 18 deletions(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index eb85d3f20b2..85d335615f7 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -735,12 +735,12 @@ TEST(ConstraintTest, ComplexOrRegression) {
 }
 
 TEST(ConstraintTest, GetSpans) {
-  const uint64_t minI32(uint32_t(std::numeric_limits<int32_t>::min()));
-  const uint64_t maxI32(std::numeric_limits<int32_t>::max());
-  const uint64_t maxU32(std::numeric_limits<uint32_t>::max());
-  const uint64_t minI64(uint64_t(std::numeric_limits<int64_t>::min()));
-  const uint64_t maxI64(std::numeric_limits<int64_t>::max());
-  const uint64_t maxU64(std::numeric_limits<uint64_t>::max());
+  const uint64_t minI32 = uint32_t(std::numeric_limits<int32_t>::min());
+  const uint64_t maxI32 = std::numeric_limits<int32_t>::max();
+  const uint64_t maxU32 = std::numeric_limits<uint32_t>::max();
+  const uint64_t minI64 = uint64_t(std::numeric_limits<int64_t>::min());
+  const uint64_t maxI64 = std::numeric_limits<int64_t>::max();
+  const uint64_t maxU64 = std::numeric_limits<uint64_t>::max();
 
   // Non-literal terms have no constant span.
   EXPECT_EQ((Constraint{Eq, {Index(0)}}.getSpans()), std::nullopt);
@@ -1043,23 +1043,23 @@ TEST(ConstraintTest, GetSpans) {
 }
 
 TEST(ConstraintTest, GetSpansType) {
-  const uint64_t minI32(uint32_t(std::numeric_limits<int32_t>::min()));
-  const uint64_t minI32Plus1(minI32 + 1);
+  const uint64_t minI32 = uint32_t(std::numeric_limits<int32_t>::min());
+  const uint64_t minI32Plus1 = minI32 + 1;
 
-  const uint64_t maxI32(std::numeric_limits<int32_t>::max());
-  const uint64_t maxI32Minus1(maxI32 - 1);
+  const uint64_t maxI32 = std::numeric_limits<int32_t>::max();
+  const uint64_t maxI32Minus1 = maxI32 - 1;
 
-  const uint64_t maxU32(std::numeric_limits<uint32_t>::max());
-  const uint64_t maxU32Minus1(maxU32 - 1);
+  const uint64_t maxU32 = std::numeric_limits<uint32_t>::max();
+  const uint64_t maxU32Minus1 = maxU32 - 1;
 
-  const uint64_t minI64(uint64_t(std::numeric_limits<int64_t>::min()));
-  const uint64_t minI64Plus1(minI64 + 1);
+  const uint64_t minI64 = uint64_t(std::numeric_limits<int64_t>::min());
+  const uint64_t minI64Plus1 = minI64 + 1;
 
-  const uint64_t maxI64(std::numeric_limits<int64_t>::max());
-  const uint64_t maxI64Minus1(maxI64 - 1);
+  const uint64_t maxI64 = std::numeric_limits<int64_t>::max();
+  const uint64_t maxI64Minus1 = maxI64 - 1;
 
-  const uint64_t maxU64(std::numeric_limits<uint64_t>::max());
-  const uint64_t maxU64Minus1(maxU64 - 1);
+  const uint64_t maxU64 = std::numeric_limits<uint64_t>::max();
+  const uint64_t maxU64Minus1 = maxU64 - 1;
 
   // Providing the type to getSpans() doesn't help with certain things.
   EXPECT_EQ((Constraint{Eq, {Index(0)}}.getSpans(Type::i32)), std::nullopt);

From ddc288a8aabee98060ce941ff78617dae5de06db Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Wed, 26 Aug 2026 14:54:33 -0700
Subject: [PATCH 28/30] feedback: use {{a, b}, {c, d}} notation

---
 src/ir/constraint.cpp     |  48 +++++-----
 src/support/span.h        |   9 --
 test/gtest/constraint.cpp | 196 +++++++++++++++++++-------------------
 test/gtest/span.cpp       |  52 +++++-----
 4 files changed, 148 insertions(+), 157 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index bcb3650b345..c7e3c9ef25b 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -63,15 +63,15 @@ getSpansInternal(const Constraint& c, std::optional<Type> type, bool exact) {
       case LtS:
         // In the signed case, this is a pair of spans: all to the left and all
         // to the right of MAX_INT.
-        return SpansU2{0, maxSigned - 1, maxSigned + 1, maxUnsigned};
+        return SpansU2{{0, maxSigned - 1}, {maxSigned + 1, maxUnsigned}};
       case LtU:
-        return SpansU2{0, maxUnsigned - 1};
+        return SpansU2{{0, maxUnsigned - 1}};
 
       // Similarly, x > y proves x != MIN_INT.
       case GtS:
-        return SpansU2{0, minSigned - 1, minSigned + 1, maxUnsigned};
+        return SpansU2{{0, minSigned - 1}, {minSigned + 1, maxUnsigned}};
       case GtU:
-        return SpansU2{1, maxUnsigned};
+        return SpansU2{{1, maxUnsigned}};
 
       default: {
       }
@@ -84,15 +84,15 @@ getSpansInternal(const Constraint& c, std::optional<Type> type, bool exact) {
 
   switch (c.op) {
     case Eq:
-      return SpansU2{x, x};
+      return SpansU2{{x, x}};
     case Ne:
       if (x == 0) {
-        return SpansU2{1, maxUnsigned};
+        return SpansU2{{1, maxUnsigned}};
       }
       if (x == maxUnsigned) {
-        return SpansU2{0, maxUnsigned - 1};
+        return SpansU2{{0, maxUnsigned - 1}};
       }
-      return SpansU2{0, x - 1, x + 1, maxUnsigned};
+      return SpansU2{{0, x - 1}, {x + 1, maxUnsigned}};
 
     case LtS:
       if (x == minSigned) {
@@ -101,35 +101,35 @@ getSpansInternal(const Constraint& c, std::optional<Type> type, bool exact) {
       }
       if (x > maxSigned) {
         // A negative number, so just a single span.
-        return SpansU2{maxSigned + 1, x - 1};
+        return SpansU2{{maxSigned + 1, x - 1}};
       }
       if (x == 0) {
         // All negative numbers are possible.
-        return SpansU2{maxSigned + 1, maxUnsigned};
+        return SpansU2{{maxSigned + 1, maxUnsigned}};
       }
       // A positive number, so all negative ones are possible, and some
       // positive.
-      return SpansU2{0, x - 1, maxSigned + 1, maxUnsigned};
+      return SpansU2{{0, x - 1}, {maxSigned + 1, maxUnsigned}};
     case LtU:
       if (x == 0) {
         // Less than the lowest possible number is an empty span.
         return SpansU2{};
       }
-      return SpansU2{0, x - 1};
+      return SpansU2{{0, x - 1}};
     case LeS:
       if (x > maxSigned) {
         // A negative number, so just a single span.
-        return SpansU2{maxSigned + 1, x};
+        return SpansU2{{maxSigned + 1, x}};
       }
       if (x == maxSigned) {
         // All numbers are possible.
-        return SpansU2{0, maxUnsigned};
+        return SpansU2{{0, maxUnsigned}};
       }
       // A non-negative number, so all negative ones are possible, and some
       // positive.
-      return SpansU2{0, x, maxSigned + 1, maxUnsigned};
+      return SpansU2{{0, x}, {maxSigned + 1, maxUnsigned}};
     case LeU:
-      return SpansU2{0, x};
+      return SpansU2{{0, x}};
 
     case GtS:
       if (x == maxSigned) {
@@ -138,35 +138,35 @@ getSpansInternal(const Constraint& c, std::optional<Type> type, bool exact) {
       }
       if (x <= maxSigned) {
         // A non-negative number, so just a single span.
-        return SpansU2{x + 1, maxSigned};
+        return SpansU2{{x + 1, maxSigned}};
       }
       if (x == maxUnsigned) {
         // GtS negative one, so 0 and above.
-        return SpansU2{0, maxSigned};
+        return SpansU2{{0, maxSigned}};
       }
       // A negative number, so all positive ones are possible, and some
       // negative.
-      return SpansU2{0, maxSigned, x + 1, maxUnsigned};
+      return SpansU2{{0, maxSigned}, {x + 1, maxUnsigned}};
     case GtU:
       if (x == maxUnsigned) {
         // Greater than the highest possible number is an empty span.
         return SpansU2{};
       }
-      return SpansU2{x + 1, maxUnsigned};
+      return SpansU2{{x + 1, maxUnsigned}};
     case GeS:
       if (x == minSigned) {
         // All numbers are possible.
-        return SpansU2{0, maxUnsigned};
+        return SpansU2{{0, maxUnsigned}};
       }
       if (x <= maxSigned) {
         // A non-negative number, so just a single span.
-        return SpansU2{x, maxSigned};
+        return SpansU2{{x, maxSigned}};
       }
       // A negative number, so all positive ones are possible, and some
       // negative.
-      return SpansU2{0, maxSigned, x, maxUnsigned};
+      return SpansU2{{0, maxSigned}, {x, maxUnsigned}};
     case GeU:
-      return SpansU2{x, maxUnsigned};
+      return SpansU2{{x, maxUnsigned}};
 
     default: {
     }
diff --git a/src/support/span.h b/src/support/span.h
index 43f3bde5c18..0d55562a1bd 100644
--- a/src/support/span.h
+++ b/src/support/span.h
@@ -101,15 +101,6 @@ struct Spans : public inplace_vector<Span<T>, N> {
     }
   }
 
-  // Initialize with pairs of coordinates.
-  Spans(std::initializer_list<T> init) {
-    assert(init.size() % 2 == 0);
-
-    for (auto it = init.begin(); it != init.end(); it += 2) {
-      this->push_back(Span<T>{*it, *(it + 1)});
-    }
-  }
-
   bool hasOverlap(const Spans<T, N>& other) const {
     // There is overlap if any of our spans overlaps with any of other's.
     return std::any_of(this->begin(), this->end(), [&](const Span<T>& span) {
diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 85d335615f7..11d82ae3dc2 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -749,76 +749,76 @@ TEST(ConstraintTest, GetSpans) {
 
   // Ne operation
   EXPECT_EQ((Constraint{Ne, {Literal(int32_t(0))}}.getSpans()),
-            (SpansU2{1, maxU32}));
+            (SpansU2{{1, maxU32}}));
   EXPECT_EQ((Constraint{Ne, {Literal(int32_t(5))}}.getSpans()),
-            (SpansU2{0, 4, 6, maxU32}));
+            (SpansU2{{0, 4}, {6, maxU32}}));
   EXPECT_EQ((Constraint{Ne, {Literal(uint32_t(maxU32))}}.getSpans()),
-            (SpansU2{0, maxU32 - 1}));
+            (SpansU2{{0, maxU32 - 1}}));
 
   EXPECT_EQ((Constraint{Ne, {Literal(int64_t(0))}}.getSpans()),
-            (SpansU2{1, maxU64}));
+            (SpansU2{{1, maxU64}}));
   EXPECT_EQ((Constraint{Ne, {Literal(int64_t(5))}}.getSpans()),
-            (SpansU2{0, 4, 6, maxU64}));
+            (SpansU2{{0, 4}, {6, maxU64}}));
   EXPECT_EQ((Constraint{Ne, {Literal(uint64_t(maxU64))}}.getSpans()),
-            (SpansU2{0, maxU64 - 1}));
+            (SpansU2{{0, maxU64 - 1}}));
 
   // Eq (i32)
   EXPECT_EQ((Constraint{Eq, {Literal(int32_t(0))}}.getSpans()),
-            (SpansU2{0, 0}));
+            (SpansU2{{0, 0}}));
   EXPECT_EQ((Constraint{Eq, {Literal(int32_t(1))}}.getSpans()),
-            (SpansU2{1, 1}));
+            (SpansU2{{1, 1}}));
   EXPECT_EQ((Constraint{Eq, {Literal(int32_t(42))}}.getSpans()),
-            (SpansU2{42, 42}));
+            (SpansU2{{42, 42}}));
   EXPECT_EQ(
     (Constraint{Eq, {Literal(std::numeric_limits<int32_t>::max())}}.getSpans()),
-    (SpansU2{maxI32, maxI32}));
+    (SpansU2{{maxI32, maxI32}}));
   EXPECT_EQ((Constraint{Eq, {Literal(int32_t(-1))}}.getSpans()),
-            (SpansU2{maxU32, maxU32}));
+            (SpansU2{{maxU32, maxU32}}));
   EXPECT_EQ((Constraint{Eq, {Literal(int32_t(-42))}}.getSpans()),
-            (SpansU2{uint32_t(-42), uint32_t(-42)}));
+            (SpansU2{{uint32_t(-42), uint32_t(-42)}}));
   EXPECT_EQ(
     (Constraint{Eq, {Literal(std::numeric_limits<int32_t>::min())}}.getSpans()),
-    (SpansU2{minI32, minI32}));
+    (SpansU2{{minI32, minI32}}));
   EXPECT_EQ((Constraint{Eq, {Literal(uint32_t(0x80000000u))}}.getSpans()),
-            (SpansU2{0x80000000u, 0x80000000u}));
+            (SpansU2{{0x80000000u, 0x80000000u}}));
   EXPECT_EQ((Constraint{Eq, {Literal(std::numeric_limits<uint32_t>::max())}}
                .getSpans()),
-            (SpansU2{maxU32, maxU32}));
+            (SpansU2{{maxU32, maxU32}}));
 
   // Eq (i64)
   EXPECT_EQ((Constraint{Eq, {Literal(int64_t(0))}}.getSpans()),
-            (SpansU2{0, 0}));
+            (SpansU2{{0, 0}}));
   EXPECT_EQ((Constraint{Eq, {Literal(int64_t(42))}}.getSpans()),
-            (SpansU2{42, 42}));
+            (SpansU2{{42, 42}}));
   EXPECT_EQ(
     (Constraint{Eq, {Literal(int64_t(std::numeric_limits<int32_t>::max()) + 1)}}
        .getSpans()),
-    (SpansU2{uint64_t(std::numeric_limits<int32_t>::max()) + 1,
-             uint64_t(std::numeric_limits<int32_t>::max()) + 1}));
+    (SpansU2{{uint64_t(std::numeric_limits<int32_t>::max()) + 1,
+              uint64_t(std::numeric_limits<int32_t>::max()) + 1}}));
   EXPECT_EQ(
     (Constraint{Eq, {Literal(std::numeric_limits<int64_t>::max())}}.getSpans()),
-    (SpansU2{maxI64, maxI64}));
+    (SpansU2{{maxI64, maxI64}}));
   EXPECT_EQ((Constraint{Eq, {Literal(int64_t(-1))}}.getSpans()),
-            (SpansU2{maxU64, maxU64}));
+            (SpansU2{{maxU64, maxU64}}));
   EXPECT_EQ(
     (Constraint{Eq, {Literal(std::numeric_limits<int64_t>::min())}}.getSpans()),
-    (SpansU2{minI64, minI64}));
+    (SpansU2{{minI64, minI64}}));
   EXPECT_EQ((Constraint{Eq, {Literal(uint64_t(uint64_t(1) << 63))}}.getSpans()),
-            (SpansU2{minI64, minI64}));
+            (SpansU2{{minI64, minI64}}));
   EXPECT_EQ((Constraint{Eq, {Literal(std::numeric_limits<uint64_t>::max())}}
                .getSpans()),
-            (SpansU2{maxU64, maxU64}));
+            (SpansU2{{maxU64, maxU64}}));
 
   // LtS (i32):
   EXPECT_EQ((Constraint{LtS, {Literal(int32_t(10))}}.getSpans()),
-            (SpansU2{0, 9, minI32, maxU32}));
+            (SpansU2{{0, 9}, {minI32, maxU32}}));
   EXPECT_EQ((Constraint{LtS, {Literal(int32_t(0))}}.getSpans()),
-            (SpansU2{minI32, maxU32}));
+            (SpansU2{{minI32, maxU32}}));
   EXPECT_EQ((Constraint{LtS, {Literal(int32_t(-5))}}.getSpans()),
-            (SpansU2{minI32, uint32_t(-6)}));
+            (SpansU2{{minI32, uint32_t(-6)}}));
   EXPECT_EQ((Constraint{LtS, {Literal(std::numeric_limits<int32_t>::max())}}
                .getSpans()),
-            (SpansU2{0, maxI32 - 1, minI32, maxU32}));
+            (SpansU2{{0, maxI32 - 1}, {minI32, maxU32}}));
   // LtS min signed (i32): empty span
   auto ltsMin32 =
     Constraint{LtS, {Literal(std::numeric_limits<int32_t>::min())}}.getSpans();
@@ -828,14 +828,14 @@ TEST(ConstraintTest, GetSpans) {
 
   // LtS (i64):
   EXPECT_EQ((Constraint{LtS, {Literal(int64_t(100))}}.getSpans()),
-            (SpansU2{0, 99, minI64, maxU64}));
+            (SpansU2{{0, 99}, {minI64, maxU64}}));
   EXPECT_EQ((Constraint{LtS, {Literal(int64_t(0))}}.getSpans()),
-            (SpansU2{minI64, maxU64}));
+            (SpansU2{{minI64, maxU64}}));
   EXPECT_EQ((Constraint{LtS, {Literal(int64_t(-5))}}.getSpans()),
-            (SpansU2{minI64, uint64_t(-6)}));
+            (SpansU2{{minI64, uint64_t(-6)}}));
   EXPECT_EQ((Constraint{LtS, {Literal(std::numeric_limits<int64_t>::max())}}
                .getSpans()),
-            (SpansU2{0, maxI64 - 1, minI64, maxU64}));
+            (SpansU2{{0, maxI64 - 1}, {minI64, maxU64}}));
   // LtS min signed (i64): empty span
   auto ltsMin64 =
     Constraint{LtS, {Literal(std::numeric_limits<int64_t>::min())}}.getSpans();
@@ -845,12 +845,12 @@ TEST(ConstraintTest, GetSpans) {
 
   // LtU (i32): [0, C - 1]
   EXPECT_EQ((Constraint{LtU, {Literal(uint32_t(10))}}.getSpans()),
-            (SpansU2{0, 9}));
+            (SpansU2{{0, 9}}));
   EXPECT_EQ((Constraint{LtU, {Literal(uint32_t(1))}}.getSpans()),
-            (SpansU2{0, 0}));
+            (SpansU2{{0, 0}}));
   EXPECT_EQ((Constraint{LtU, {Literal(std::numeric_limits<uint32_t>::max())}}
                .getSpans()),
-            (SpansU2{0, maxU32 - 1}));
+            (SpansU2{{0, maxU32 - 1}}));
   // LtU 0 (i32): empty span
   auto ltuZero32 = Constraint{LtU, {Literal(uint32_t(0))}}.getSpans();
   ASSERT_TRUE(ltuZero32.has_value());
@@ -859,10 +859,10 @@ TEST(ConstraintTest, GetSpans) {
 
   // LtU (i64): [0, C - 1]
   EXPECT_EQ((Constraint{LtU, {Literal(uint64_t(100))}}.getSpans()),
-            (SpansU2{0, 99}));
+            (SpansU2{{0, 99}}));
   EXPECT_EQ((Constraint{LtU, {Literal(std::numeric_limits<uint64_t>::max())}}
                .getSpans()),
-            (SpansU2{0, maxU64 - 1}));
+            (SpansU2{{0, maxU64 - 1}}));
   // LtU 0 (i64): empty span
   auto ltuZero64 = Constraint{LtU, {Literal(uint64_t(0))}}.getSpans();
   ASSERT_TRUE(ltuZero64.has_value());
@@ -871,65 +871,65 @@ TEST(ConstraintTest, GetSpans) {
 
   // LeS (i32):
   EXPECT_EQ((Constraint{LeS, {Literal(int32_t(10))}}.getSpans()),
-            (SpansU2{0, 10, minI32, maxU32}));
+            (SpansU2{{0, 10}, {minI32, maxU32}}));
   EXPECT_EQ((Constraint{LeS, {Literal(int32_t(0))}}.getSpans()),
-            (SpansU2{0, 0, minI32, maxU32}));
+            (SpansU2{{0, 0}, {minI32, maxU32}}));
   EXPECT_EQ((Constraint{LeS, {Literal(int32_t(-5))}}.getSpans()),
-            (SpansU2{minI32, uint32_t(-5)}));
+            (SpansU2{{minI32, uint32_t(-5)}}));
   EXPECT_EQ((Constraint{LeS, {Literal(std::numeric_limits<int32_t>::min())}}
                .getSpans()),
-            (SpansU2{minI32, minI32}));
+            (SpansU2{{minI32, minI32}}));
   EXPECT_EQ((Constraint{LeS, {Literal(std::numeric_limits<int32_t>::max())}}
                .getSpans()),
-            (SpansU2{0, maxU32}));
+            (SpansU2{{0, maxU32}}));
 
   // LeS (i64):
   EXPECT_EQ((Constraint{LeS, {Literal(int64_t(10))}}.getSpans()),
-            (SpansU2{0, 10, minI64, maxU64}));
+            (SpansU2{{0, 10}, {minI64, maxU64}}));
   EXPECT_EQ((Constraint{LeS, {Literal(int64_t(0))}}.getSpans()),
-            (SpansU2{0, 0, minI64, maxU64}));
+            (SpansU2{{0, 0}, {minI64, maxU64}}));
   EXPECT_EQ((Constraint{LeS, {Literal(int64_t(-5))}}.getSpans()),
-            (SpansU2{minI64, uint64_t(-5)}));
+            (SpansU2{{minI64, uint64_t(-5)}}));
   EXPECT_EQ((Constraint{LeS, {Literal(std::numeric_limits<int64_t>::min())}}
                .getSpans()),
-            (SpansU2{minI64, minI64}));
+            (SpansU2{{minI64, minI64}}));
   EXPECT_EQ((Constraint{LeS, {Literal(std::numeric_limits<int64_t>::max())}}
                .getSpans()),
-            (SpansU2{0, maxU64}));
+            (SpansU2{{0, maxU64}}));
 
   // LeU (i32): [0, C]
   EXPECT_EQ((Constraint{LeU, {Literal(uint32_t(0))}}.getSpans()),
-            (SpansU2{0, 0}));
+            (SpansU2{{0, 0}}));
   EXPECT_EQ((Constraint{LeU, {Literal(uint32_t(10))}}.getSpans()),
-            (SpansU2{0, 10}));
+            (SpansU2{{0, 10}}));
   EXPECT_EQ((Constraint{LeU, {Literal(std::numeric_limits<uint32_t>::max())}}
                .getSpans()),
-            (SpansU2{0, maxU32}));
+            (SpansU2{{0, maxU32}}));
 
   // LeU (i64): [0, C]
   EXPECT_EQ((Constraint{LeU, {Literal(uint64_t(0))}}.getSpans()),
-            (SpansU2{0, 0}));
+            (SpansU2{{0, 0}}));
   EXPECT_EQ((Constraint{LeU, {Literal(uint64_t(10))}}.getSpans()),
-            (SpansU2{0, 10}));
+            (SpansU2{{0, 10}}));
   EXPECT_EQ((Constraint{LeU, {Literal(std::numeric_limits<uint64_t>::max())}}
                .getSpans()),
-            (SpansU2{0, maxU64}));
+            (SpansU2{{0, maxU64}}));
 
   // GtS (i32):
   EXPECT_EQ((Constraint{GtS, {Literal(int32_t(10))}}.getSpans()),
-            (SpansU2{11, maxI32}));
+            (SpansU2{{11, maxI32}}));
   EXPECT_EQ((Constraint{GtS, {Literal(int32_t(0))}}.getSpans()),
-            (SpansU2{1, maxI32}));
+            (SpansU2{{1, maxI32}}));
   EXPECT_EQ((Constraint{GtS, {Literal(int32_t(-5))}}.getSpans()),
-            (SpansU2{0, maxI32, uint32_t(-4), maxU32}));
+            (SpansU2{{0, maxI32}, {uint32_t(-4), maxU32}}));
   EXPECT_EQ((Constraint{GtS, {Literal(int32_t(-1))}}.getSpans()),
-            (SpansU2{0, maxI32}));
+            (SpansU2{{0, maxI32}}));
   EXPECT_EQ((Constraint{GtS, {Literal(std::numeric_limits<int32_t>::min())}}
                .getSpans()),
-            (SpansU2{0, maxI32, minI32 + 1, maxU32}));
+            (SpansU2{{0, maxI32}, {minI32 + 1, maxU32}}));
   EXPECT_EQ((Constraint{GtS, {Literal(std::numeric_limits<int32_t>::max() - 1)}}
                .getSpans()),
-            (SpansU2{maxI32, maxI32}));
+            (SpansU2{{maxI32, maxI32}}));
   // GtS max signed (i32): empty span
   auto gtsMax32 =
     Constraint{GtS, {Literal(std::numeric_limits<int32_t>::max())}}.getSpans();
@@ -939,19 +939,19 @@ TEST(ConstraintTest, GetSpans) {
 
   // GtS (i64):
   EXPECT_EQ((Constraint{GtS, {Literal(int64_t(10))}}.getSpans()),
-            (SpansU2{11, maxI64}));
+            (SpansU2{{11, maxI64}}));
   EXPECT_EQ((Constraint{GtS, {Literal(int64_t(0))}}.getSpans()),
-            (SpansU2{1, maxI64}));
+            (SpansU2{{1, maxI64}}));
   EXPECT_EQ((Constraint{GtS, {Literal(int64_t(-5))}}.getSpans()),
-            (SpansU2{0, maxI64, uint64_t(-4), maxU64}));
+            (SpansU2{{0, maxI64}, {uint64_t(-4), maxU64}}));
   EXPECT_EQ((Constraint{GtS, {Literal(int64_t(-1))}}.getSpans()),
-            (SpansU2{0, maxI64}));
+            (SpansU2{{0, maxI64}}));
   EXPECT_EQ((Constraint{GtS, {Literal(std::numeric_limits<int64_t>::min())}}
                .getSpans()),
-            (SpansU2{0, maxI64, minI64 + 1, maxU64}));
+            (SpansU2{{0, maxI64}, {minI64 + 1, maxU64}}));
   EXPECT_EQ((Constraint{GtS, {Literal(std::numeric_limits<int64_t>::max() - 1)}}
                .getSpans()),
-            (SpansU2{maxI64, maxI64}));
+            (SpansU2{{maxI64, maxI64}}));
   // GtS max signed (i64): empty span
   auto gtsMax64 =
     Constraint{GtS, {Literal(std::numeric_limits<int64_t>::max())}}.getSpans();
@@ -961,13 +961,13 @@ TEST(ConstraintTest, GetSpans) {
 
   // GtU (i32): [C + 1, maxU32]
   EXPECT_EQ((Constraint{GtU, {Literal(uint32_t(0))}}.getSpans()),
-            (SpansU2{1, maxU32}));
+            (SpansU2{{1, maxU32}}));
   EXPECT_EQ((Constraint{GtU, {Literal(uint32_t(10))}}.getSpans()),
-            (SpansU2{11, maxU32}));
+            (SpansU2{{11, maxU32}}));
   EXPECT_EQ(
     (Constraint{GtU, {Literal(std::numeric_limits<uint32_t>::max() - 1)}}
        .getSpans()),
-    (SpansU2{maxU32, maxU32}));
+    (SpansU2{{maxU32, maxU32}}));
   // GtU max unsigned (i32): empty span
   auto gtuMax32 =
     Constraint{GtU, {Literal(std::numeric_limits<uint32_t>::max())}}.getSpans();
@@ -977,13 +977,13 @@ TEST(ConstraintTest, GetSpans) {
 
   // GtU (i64): [C + 1, maxU64]
   EXPECT_EQ((Constraint{GtU, {Literal(uint64_t(0))}}.getSpans()),
-            (SpansU2{1, maxU64}));
+            (SpansU2{{1, maxU64}}));
   EXPECT_EQ((Constraint{GtU, {Literal(uint64_t(10))}}.getSpans()),
-            (SpansU2{11, maxU64}));
+            (SpansU2{{11, maxU64}}));
   EXPECT_EQ(
     (Constraint{GtU, {Literal(std::numeric_limits<uint64_t>::max() - 1)}}
        .getSpans()),
-    (SpansU2{maxU64, maxU64}));
+    (SpansU2{{maxU64, maxU64}}));
   // GtU max unsigned (i64): empty span
   auto gtuMax64 =
     Constraint{GtU, {Literal(std::numeric_limits<uint64_t>::max())}}.getSpans();
@@ -993,53 +993,53 @@ TEST(ConstraintTest, GetSpans) {
 
   // GeS (i32):
   EXPECT_EQ((Constraint{GeS, {Literal(int32_t(10))}}.getSpans()),
-            (SpansU2{10, maxI32}));
+            (SpansU2{{10, maxI32}}));
   EXPECT_EQ((Constraint{GeS, {Literal(int32_t(0))}}.getSpans()),
-            (SpansU2{0, maxI32}));
+            (SpansU2{{0, maxI32}}));
   EXPECT_EQ((Constraint{GeS, {Literal(int32_t(-5))}}.getSpans()),
-            (SpansU2{0, maxI32, uint32_t(-5), maxU32}));
+            (SpansU2{{0, maxI32}, {uint32_t(-5), maxU32}}));
   EXPECT_EQ((Constraint{GeS, {Literal(int32_t(-1))}}.getSpans()),
-            (SpansU2{0, maxI32, maxU32, maxU32}));
+            (SpansU2{{0, maxI32}, {maxU32, maxU32}}));
   EXPECT_EQ((Constraint{GeS, {Literal(std::numeric_limits<int32_t>::min())}}
                .getSpans()),
-            (SpansU2{0, maxU32}));
+            (SpansU2{{0, maxU32}}));
   EXPECT_EQ((Constraint{GeS, {Literal(std::numeric_limits<int32_t>::max())}}
                .getSpans()),
-            (SpansU2{maxI32, maxI32}));
+            (SpansU2{{maxI32, maxI32}}));
 
   // GeS (i64):
   EXPECT_EQ((Constraint{GeS, {Literal(int64_t(10))}}.getSpans()),
-            (SpansU2{10, maxI64}));
+            (SpansU2{{10, maxI64}}));
   EXPECT_EQ((Constraint{GeS, {Literal(int64_t(0))}}.getSpans()),
-            (SpansU2{0, maxI64}));
+            (SpansU2{{0, maxI64}}));
   EXPECT_EQ((Constraint{GeS, {Literal(int64_t(-5))}}.getSpans()),
-            (SpansU2{0, maxI64, uint64_t(-5), maxU64}));
+            (SpansU2{{0, maxI64}, {uint64_t(-5), maxU64}}));
   EXPECT_EQ((Constraint{GeS, {Literal(int64_t(-1))}}.getSpans()),
-            (SpansU2{0, maxI64, maxU64, maxU64}));
+            (SpansU2{{0, maxI64}, {maxU64, maxU64}}));
   EXPECT_EQ((Constraint{GeS, {Literal(std::numeric_limits<int64_t>::min())}}
                .getSpans()),
-            (SpansU2{0, maxU64}));
+            (SpansU2{{0, maxU64}}));
   EXPECT_EQ((Constraint{GeS, {Literal(std::numeric_limits<int64_t>::max())}}
                .getSpans()),
-            (SpansU2{maxI64, maxI64}));
+            (SpansU2{{maxI64, maxI64}}));
 
   // GeU (i32): [C, maxU32]
   EXPECT_EQ((Constraint{GeU, {Literal(uint32_t(0))}}.getSpans()),
-            (SpansU2{0, maxU32}));
+            (SpansU2{{0, maxU32}}));
   EXPECT_EQ((Constraint{GeU, {Literal(uint32_t(10))}}.getSpans()),
-            (SpansU2{10, maxU32}));
+            (SpansU2{{10, maxU32}}));
   EXPECT_EQ((Constraint{GeU, {Literal(std::numeric_limits<uint32_t>::max())}}
                .getSpans()),
-            (SpansU2{maxU32, maxU32}));
+            (SpansU2{{maxU32, maxU32}}));
 
   // GeU (i64): [C, maxU64]
   EXPECT_EQ((Constraint{GeU, {Literal(uint64_t(0))}}.getSpans()),
-            (SpansU2{0, maxU64}));
+            (SpansU2{{0, maxU64}}));
   EXPECT_EQ((Constraint{GeU, {Literal(uint64_t(10))}}.getSpans()),
-            (SpansU2{10, maxU64}));
+            (SpansU2{{10, maxU64}}));
   EXPECT_EQ((Constraint{GeU, {Literal(std::numeric_limits<uint64_t>::max())}}
                .getSpans()),
-            (SpansU2{maxU64, maxU64}));
+            (SpansU2{{maxU64, maxU64}}));
 }
 
 TEST(ConstraintTest, GetSpansType) {
@@ -1072,24 +1072,24 @@ TEST(ConstraintTest, GetSpansType) {
   // But it does help with others: x < y means x cannot be MAX_INT, so we can
   // report a *proven* span, if not an exact one.
   EXPECT_EQ((Constraint{LtS, {Index(0)}}.getProvenSpans(Type::i32)),
-            (SpansU2{0, maxI32Minus1, minI32, maxU32}));
+            (SpansU2{{0, maxI32Minus1}, {minI32, maxU32}}));
   EXPECT_EQ((Constraint{LtS, {Index(1)}}.getProvenSpans(Type::i64)),
-            (SpansU2{0, maxI64Minus1, minI64, maxU64}));
+            (SpansU2{{0, maxI64Minus1}, {minI64, maxU64}}));
 
   EXPECT_EQ((Constraint{LtU, {Index(2)}}.getProvenSpans(Type::i32)),
-            (SpansU2{0, maxU32Minus1}));
+            (SpansU2{{0, maxU32Minus1}}));
   EXPECT_EQ((Constraint{LtU, {Index(0)}}.getProvenSpans(Type::i64)),
-            (SpansU2{0, maxU64Minus1}));
+            (SpansU2{{0, maxU64Minus1}}));
 
   EXPECT_EQ((Constraint{GtS, {Index(1)}}.getProvenSpans(Type::i32)),
-            (SpansU2{0, maxI32, minI32Plus1, maxU32}));
+            (SpansU2{{0, maxI32}, {minI32Plus1, maxU32}}));
   EXPECT_EQ((Constraint{GtS, {Index(2)}}.getProvenSpans(Type::i64)),
-            (SpansU2{0, maxI64, minI64Plus1, maxU64}));
+            (SpansU2{{0, maxI64}, {minI64Plus1, maxU64}}));
 
   EXPECT_EQ((Constraint{GtU, {Index(0)}}.getProvenSpans(Type::i32)),
-            (SpansU2{1, maxU32}));
+            (SpansU2{{1, maxU32}}));
   EXPECT_EQ((Constraint{GtU, {Index(1)}}.getProvenSpans(Type::i64)),
-            (SpansU2{1, maxU64}));
+            (SpansU2{{1, maxU64}}));
 
   // But all the last things are impossible with an exact span.
   EXPECT_EQ((Constraint{LtS, {Index(0)}}.getSpans(Type::i32)), std::nullopt);
@@ -1103,7 +1103,7 @@ TEST(ConstraintTest, GetSpansType) {
 
   // Proven spans are otherwise like normal ones.
   EXPECT_EQ((Constraint{Eq, {Literal(int32_t(42))}}.getProvenSpans()),
-            (SpansU2{42, 42}));
+            (SpansU2{{42, 42}}));
 }
 
 TEST(ConstraintTest, SpanOptimizations) {
diff --git a/test/gtest/span.cpp b/test/gtest/span.cpp
index 26296d5e2a8..c5e98b31909 100644
--- a/test/gtest/span.cpp
+++ b/test/gtest/span.cpp
@@ -198,34 +198,34 @@ TEST(SpansTest, Construction) {
   EXPECT_EQ(fromSpans[0], Span<uint64_t>(0, 10));
   EXPECT_EQ(fromSpans[1], Span<uint64_t>(20, 30));
 
-  SpansU2 fromCoords{0, 10, 20, 30};
+  SpansU2 fromCoords{{0, 10}, {20, 30}};
   EXPECT_EQ(fromCoords.size(), 2u);
   EXPECT_EQ(fromCoords[0], Span<uint64_t>(0, 10));
   EXPECT_EQ(fromCoords[1], Span<uint64_t>(20, 30));
 
-  SpansU2 single{5, 15};
+  SpansU2 single{{5, 15}};
   EXPECT_EQ(single.size(), 1u);
   EXPECT_EQ(single[0], Span<uint64_t>(5, 15));
 }
 
 TEST(SpansTest, Equality) {
   EXPECT_EQ(SpansU2(), SpansU2());
-  EXPECT_EQ((SpansU2{0, 10}), (SpansU2{0, 10}));
-  EXPECT_EQ((SpansU2{0, 10, 20, 30}), (SpansU2{0, 10, 20, 30}));
+  EXPECT_EQ((SpansU2{{0, 10}}), (SpansU2{{0, 10}}));
+  EXPECT_EQ((SpansU2{{0, 10}, {20, 30}}), (SpansU2{{0, 10}, {20, 30}}));
 
-  EXPECT_NE((SpansU2{0, 10}), SpansU2());
-  EXPECT_NE((SpansU2{0, 10}), (SpansU2{0, 11}));
-  EXPECT_NE((SpansU2{0, 10}), (SpansU2{0, 10, 20, 30}));
+  EXPECT_NE((SpansU2{{0, 10}}), SpansU2());
+  EXPECT_NE((SpansU2{{0, 10}}), (SpansU2{{0, 11}}));
+  EXPECT_NE((SpansU2{{0, 10}}), (SpansU2{{0, 10}, {20, 30}}));
 }
 
 TEST(SpansTest, HasOverlap) {
   SpansU2 empty;
-  SpansU2 s1{0, 10, 20, 30};
-  SpansU2 s2{5, 15};
-  SpansU2 s3{25, 35};
-  SpansU2 s4{11, 19};
-  SpansU2 s5{31, 40};
-  SpansU2 s6{10, 20};
+  SpansU2 s1{{0, 10}, {20, 30}};
+  SpansU2 s2{{5, 15}};
+  SpansU2 s3{{25, 35}};
+  SpansU2 s4{{11, 19}};
+  SpansU2 s5{{31, 40}};
+  SpansU2 s6{{10, 20}};
 
   EXPECT_FALSE(empty.hasOverlap(s1));
   EXPECT_FALSE(s1.hasOverlap(empty));
@@ -254,12 +254,12 @@ TEST(SpansTest, HasOverlap) {
 
 TEST(SpansTest, Contains) {
   SpansU2 empty;
-  SpansU2 s1{0, 100, 200, 300};
-  SpansU2 s2{10, 20};
-  SpansU2 s3{210, 220};
-  SpansU2 s4{10, 20, 210, 220};
-  SpansU2 s5{50, 150};
-  SpansU2 s6{10, 20, 250, 350};
+  SpansU2 s1{{0, 100}, {200, 300}};
+  SpansU2 s2{{10, 20}};
+  SpansU2 s3{{210, 220}};
+  SpansU2 s4{{10, 20}, {210, 220}};
+  SpansU2 s5{{50, 150}};
+  SpansU2 s6{{10, 20}, {250, 350}};
 
   // Empty contains empty, non-empty contains empty, empty does not contain
   // non-empty
@@ -294,21 +294,21 @@ TEST(SpansTest, ExtremeBoundaries) {
   uint64_t maxU64 = std::numeric_limits<uint64_t>::max();
   uint64_t highBit = uint64_t(1) << 63;
 
-  SpansU2 lowPart{0, 100};
-  SpansU2 highPart{maxU64 - 100, maxU64};
-  SpansU2 midPart{highBit - 10, highBit + 10};
+  SpansU2 lowPart{{0, 100}};
+  SpansU2 highPart{{maxU64 - 100, maxU64}};
+  SpansU2 midPart{{highBit - 10, highBit + 10}};
 
   EXPECT_FALSE(lowPart.hasOverlap(highPart));
   EXPECT_FALSE(highPart.hasOverlap(lowPart));
   EXPECT_FALSE(lowPart.hasOverlap(midPart));
   EXPECT_FALSE(midPart.hasOverlap(highPart));
 
-  SpansU2 split{0, 100, maxU64 - 100, maxU64};
+  SpansU2 split{{0, 100}, {maxU64 - 100, maxU64}};
   EXPECT_TRUE(split.contains(lowPart));
   EXPECT_TRUE(split.contains(highPart));
   EXPECT_FALSE(split.contains(midPart));
 
-  SpansU2 fullRange{0, maxU64};
+  SpansU2 fullRange{{0, maxU64}};
   EXPECT_TRUE(fullRange.contains(split));
   EXPECT_TRUE(fullRange.contains(lowPart));
   EXPECT_TRUE(fullRange.contains(highPart));
@@ -343,6 +343,6 @@ TEST(SpansTest, StreamOutput) {
   };
 
   EXPECT_EQ(toString(SpansU2{}), "{empty}");
-  EXPECT_EQ(toString(SpansU2{1, 10}), "{[1, 10]}");
-  EXPECT_EQ(toString(SpansU2{1, 10, 20, 30}), "{[1, 10], [20, 30]}");
+  EXPECT_EQ(toString(SpansU2{{1, 10}}), "{[1, 10]}");
+  EXPECT_EQ(toString(SpansU2{{1, 10}, {20, 30}}), "{[1, 10], [20, 30]}");
 }

From 71215dfdea98f659082d332854c638ba1c993d18 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Wed, 26 Aug 2026 15:10:11 -0700
Subject: [PATCH 29/30] fix warning?

---
 src/support/span.h | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/support/span.h b/src/support/span.h
index 0d55562a1bd..c643452116d 100644
--- a/src/support/span.h
+++ b/src/support/span.h
@@ -19,6 +19,7 @@
 
 #include <algorithm>
 #include <cassert>
+#include <cstdint>
 #include <iostream>
 #include <limits>
 

From 1ce95889a9608086a8d4cb6421a63cbebc942e2b Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Wed, 26 Aug 2026 15:51:34 -0700
Subject: [PATCH 30/30] Try to work around a gcc 13 compiler error

---
 src/support/span.h | 38 +++++++++++++++++++++++---------------
 1 file changed, 23 insertions(+), 15 deletions(-)

diff --git a/src/support/span.h b/src/support/span.h
index c643452116d..e5038efc58e 100644
--- a/src/support/span.h
+++ b/src/support/span.h
@@ -104,25 +104,33 @@ struct Spans : public inplace_vector<Span<T>, N> {
 
   bool hasOverlap(const Spans<T, N>& other) const {
     // There is overlap if any of our spans overlaps with any of other's.
-    return std::any_of(this->begin(), this->end(), [&](const Span<T>& span) {
-      return std::any_of(
-        other.begin(), other.end(), [&](const Span<T>& otherSpan) {
-          return span.hasOverlap(otherSpan);
-        });
-    });
+    for (const auto& span : *this) {
+      for (const auto& otherSpan : other) {
+        if (span.hasOverlap(otherSpan)) {
+          return true;
+        }
+      }
+    }
+    return false;
   }
 
   bool contains(const Spans<T, N>& other) const {
     // We contain other if each of their spans is contained in us.
-    return std::all_of(
-      other.begin(), other.end(), [&](const Span<T>& otherSpan) {
-        // Because our spans are assumed to be disjoint, exactly one of our
-        // spans must contain otherSpan.
-        return std::any_of(
-          this->begin(), this->end(), [&](const Span<T>& span) {
-            return span.contains(otherSpan);
-          });
-      });
+    for (const auto& otherSpan : other) {
+      // Because our spans are assumed to be disjoint, exactly one of our
+      // spans must contain otherSpan.
+      bool found = false;
+      for (const auto& span : *this) {
+        if (span.contains(otherSpan)) {
+          found = true;
+          break;
+        }
+      }
+      if (!found) {
+        return false;
+      }
+    }
+    return true;
   }
 };