diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index a02f0bdbcec..e0839a5f964 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -24,8 +24,8 @@ namespace wasm::constraint {
 
 namespace {
 
-std::optional<Span<IU64>>
-getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
+std::optional<SpansU2>
+getSpansInternal(const Constraint& c, std::optional<Type> type, bool exact) {
   using namespace Abstract;
 
   auto* cc = std::get_if<Literal>(&c.term);
@@ -41,15 +41,15 @@ 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
-                       ? std::numeric_limits<uint32_t>::max()
-                       : std::numeric_limits<uint64_t>::max();
+  // 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();
+  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,17 +59,19 @@ 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 Span<IU64>{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 Span<IU64>{0, maxUnsigned - 1};
+        return SpansU2{{0, maxUnsigned - 1}};
 
-      // Similarly, x > y proves x > MIN_INT.
+      // Similarly, x > y proves x != MIN_INT.
       case GtS:
-        return Span<IU64>{minSigned + 1, maxSigned};
+        return SpansU2{{0, minSigned - 1}, {minSigned + 1, maxUnsigned}};
       case GtU:
-        return Span<IU64>{1, maxUnsigned};
+        return SpansU2{{1, maxUnsigned}};
 
       default: {
       }
@@ -78,61 +80,93 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
     return {};
   }
 
+  auto x = cc->getUnsigned();
+
   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 Span<IU64>{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:
-      if (cc->getInteger() == minSigned) {
+      if (x == minSigned) {
         // Less than the lowest possible number is an empty span.
-        return Span<IU64>::empty();
-      } else {
-        return Span<IU64>{minSigned, cc->getInteger() - 1};
+        return SpansU2{};
       }
-      break;
+      if (x > maxSigned) {
+        // A negative number, so just a single span.
+        return SpansU2{{maxSigned + 1, x - 1}};
+      }
+      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 Span<IU64>::empty();
-      } else {
-        return Span<IU64>{0, cc->getUnsigned() - 1};
+        return SpansU2{};
       }
-      break;
+      return SpansU2{{0, x - 1}};
     case LeS:
-      return Span<IU64>{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 Span<IU64>{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 Span<IU64>::empty();
-      } else {
-        return Span<IU64>{cc->getInteger() + 1, maxSigned};
+        return SpansU2{};
       }
-      break;
+      if (x <= maxSigned) {
+        // A non-negative number, so just a single span.
+        return SpansU2{{x + 1, maxSigned}};
+      }
+      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 (cc->getUnsigned() == maxUnsigned) {
+      if (x == maxUnsigned) {
         // Greater than the highest possible number is an empty span.
-        return Span<IU64>::empty();
-      } else {
-        return Span<IU64>{cc->getUnsigned() + 1, maxUnsigned};
+        return SpansU2{};
       }
-      break;
+      return SpansU2{{x + 1, maxUnsigned}};
     case GeS:
-      return Span<IU64>{cc->getInteger(), maxSigned};
+      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}};
+      }
+      // A negative number, so all positive ones are possible, and some
+      // negative.
+      return SpansU2{{0, maxSigned}, {x, maxUnsigned}};
     case GeU:
-      return Span<IU64>{cc->getUnsigned(), maxUnsigned};
+      return SpansU2{{x, maxUnsigned}};
 
     default: {
     }
@@ -143,13 +177,13 @@ getSpanInternal(const Constraint& c, std::optional<Type> type, bool exact) {
 
 } // anonymous namespace
 
-std::optional<Span<IU64>> 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<Span<IU64>>
-Constraint::getProvenSpan(std::optional<Type> type) const {
-  return getSpanInternal(*this, type, false);
+std::optional<SpansU2>
+Constraint::getProvenSpans(std::optional<Type> type) const {
+  return getSpansInternal(*this, type, false);
 }
 
 namespace {
@@ -247,26 +281,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/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/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..e5038efc58e 100644
--- a/src/support/span.h
+++ b/src/support/span.h
@@ -19,9 +19,12 @@
 
 #include <algorithm>
 #include <cassert>
+#include <cstdint>
 #include <iostream>
 #include <limits>
 
+#include "support/inplace_vector.h"
+
 namespace wasm {
 
 // A span of values.
@@ -87,6 +90,56 @@ template<typename T> struct Span {
   bool operator!=(const Span& other) const { return !(*this == other); }
 };
 
+// A union of spans, which we assume are disjoint.
+template<typename T, size_t N>
+struct Spans : public inplace_vector<Span<T>, N> {
+  constexpr Spans() = default;
+
+  // Initialize with Spans.
+  Spans(std::initializer_list<Span<T>> init) {
+    for (const auto& span : init) {
+      this->push_back(span);
+    }
+  }
+
+  bool hasOverlap(const Spans<T, N>& other) const {
+    // There is overlap if any of our spans overlaps with any of other's.
+    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.
+    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;
+  }
+};
+
+// 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^31..MAX_INT].
+using SpansU2 = Spans<uint64_t, 2>;
+
 template<typename T>
 inline std::ostream& operator<<(std::ostream& os, const Span<T>& span) {
   if (span.isEmpty()) {
@@ -95,6 +148,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 cf8f633e983..5c00d18f047 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,376 @@ 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, {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);
+  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>::min())}}.getSpan()),
-    std::nullopt);
-  EXPECT_EQ((Constraint{Eq, {Literal(uint32_t(0x80000000u))}}.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<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<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())}}
+               .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);
-  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)}));
-  EXPECT_EQ(
-    (Constraint{LtS, {Literal(std::numeric_limits<int32_t>::max())}}.getSpan()),
-    (Span<IU64>{minI32, IU64(std::numeric_limits<int32_t>::max() - 1)}));
+    (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())}}
+               .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())}}
+               .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_EQ(
-    (Constraint{LtS, {Literal(std::numeric_limits<int64_t>::max())}}.getSpan()),
-    (Span<IU64>{minI64, IU64(std::numeric_limits<int64_t>::max() - 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())}}
+               .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(std::numeric_limits<uint32_t>::max())}}
-       .getSpan()),
-    (Span<IU64>{IU64(0),
-                IU64(uint64_t(std::numeric_limits<uint32_t>::max()) - 1)}));
+  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())}}
+               .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(std::numeric_limits<uint64_t>::max())}}
-       .getSpan()),
-    (Span<IU64>{IU64(0), IU64(std::numeric_limits<uint64_t>::max() - 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}}));
   // 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_EQ(
-    (Constraint{LeS, {Literal(std::numeric_limits<int32_t>::min())}}.getSpan()),
-    (Span<IU64>{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)}));
-  EXPECT_EQ(
-    (Constraint{LeS, {Literal(std::numeric_limits<int64_t>::min())}}.getSpan()),
-    (Span<IU64>{minI64, minI64}));
-  EXPECT_EQ(
-    (Constraint{LeS, {Literal(std::numeric_limits<int64_t>::max())}}.getSpan()),
-    (Span<IU64>{minI64, maxI64}));
+  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())}}
+               .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()),
+            (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())}}
+               .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))}}.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}));
-  EXPECT_EQ(
-    (Constraint{GtS, {Literal(std::numeric_limits<int32_t>::min())}}.getSpan()),
-    (Span<IU64>{IU64(std::numeric_limits<int32_t>::min() + 1), 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())}}
+               .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_EQ(
-    (Constraint{GtS, {Literal(std::numeric_limits<int64_t>::min())}}.getSpan()),
-    (Span<IU64>{IU64(std::numeric_limits<int64_t>::min() + 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())}}
+               .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_EQ(
-    (Constraint{GeS, {Literal(std::numeric_limits<int32_t>::min())}}.getSpan()),
-    (Span<IU64>{minI32, maxI32}));
-  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}));
-  EXPECT_EQ(
-    (Constraint{GeS, {Literal(std::numeric_limits<int64_t>::min())}}.getSpan()),
-    (Span<IU64>{minI64, maxI64}));
-  EXPECT_EQ(
-    (Constraint{GeS, {Literal(std::numeric_limits<int64_t>::max())}}.getSpan()),
-    (Span<IU64>{maxI64, maxI64}));
+  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())}}
+               .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()),
+            (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())}}
+               .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))}}.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 +1112,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,16 +1185,202 @@ 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);
 }
 
+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, 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))}};
+  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);
+
+  // 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), that is,
+  // [minI32, large number] in the unsigned representation of bits. x < -10
+  // *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);
+
+  // 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);
+}
+
+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);
+
+  // 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) {
+  // 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);
+
+  // 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);
+}
+
 TEST(ConstraintTest, FloatNegativeZero) {
   // f == 0.0 proves f == -0.0 is True.
   AndedConstraintSet s;
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");
-}
diff --git a/test/gtest/span.cpp b/test/gtest/span.cpp
index f05fd80e2ff..c5e98b31909 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,165 @@ 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 46a9058a130..a3799bbd647 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -4947,4 +4947,155 @@
       )
     )
   )
+
+  ;; 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.gt_u
+  ;; CHECK-NEXT:     (local.get $0)
+  ;; CHECK-NEXT:     (i32.const -1992)
+  ;; CHECK-NEXT:    )
+  ;; 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.gt_u
+  ;; OPTIN-NEXT:     (local.get $0)
+  ;; OPTIN-NEXT:     (i32.const -1992)
+  ;; OPTIN-NEXT:    )
+  ;; 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. 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)
+          (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.gt_u
+  ;; CHECK-NEXT:     (local.get $0)
+  ;; CHECK-NEXT:     (i32.const -1992)
+  ;; CHECK-NEXT:    )
+  ;; 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.gt_u
+  ;; OPTIN-NEXT:     (local.get $0)
+  ;; OPTIN-NEXT:     (i32.const -1992)
+  ;; OPTIN-NEXT:    )
+  ;; 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 be true, so we
+      ;; optimize nothing.
+      (drop
+        (i32.gt_u
+          (local.get $0)
+          (i32.const -1992)
+        )
+      )
+    )
+  )
+
+  ;; 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)
+        )
+      )
+    )
+  )
 )