diff --git a/src/crab/split_dbm.cpp b/src/crab/split_dbm.cpp
index 1005a1272..b5137d203 100644
--- a/src/crab/split_dbm.cpp
+++ b/src/crab/split_dbm.cpp
@@ -1130,14 +1130,62 @@ string_invariant SplitDBM::to_set() const {
     if (this->is_top()) {
         return string_invariant::top();
     }
+    // Extract all the edges
+    SubGraph g_excl{this->g, 0};
+
+    std::map<variable_t, variable_t> equivalence_classes;
+    std::set<std::tuple<variable_t, variable_t, Weight>> diff_csts;
+    for (const vert_id s : g_excl.verts()) {
+        const variable_t vs = *rev_map.at(s);
+        variable_t least = vs;
+        for (const vert_id d : g_excl.succs(s)) {
+            const variable_t vd = *rev_map.at(d);
+            const Weight w = g_excl.edge_val(s, d);
+            if (w == 0) {
+                least = std::min(least, vd, variable_t::printing_order);
+            } else {
+                diff_csts.emplace(vd, vs, w);
+            }
+        }
+        equivalence_classes.insert_or_assign(vs, least);
+    }
+
+    std::set<variable_t> representatives;
+    std::map<variable_t, std::string> equivalence_str;
+    for (const auto [vs, least] : equivalence_classes) {
+        if (vs == least) {
+            representatives.insert(vs);
+        } else {
+            equivalence_str[least] += "=" + vs.name();
+        }
+    }
 
     std::set<std::string> result;
-    // Intervals
+    for (const auto& [v, eqs] : equivalence_str) {
+        result.insert(v.name() + eqs);
+    }
 
-    // Extract all the edges
-    SubGraph g_excl(this->g, 0);
+    // simplify: x - y <= k && y - x <= -k
+    //        -> x <= y + k <= x
+    //        -> x = y + k
+    for (const auto& [vd, vs, w] : diff_csts) {
+        if (!representatives.contains(vd) || !representatives.contains(vs)) {
+            continue;
+        }
+        auto dual = to_string(vs, vd, -w, false);
+        if (result.contains(dual)) {
+            assert(w != 0);
+            result.erase(dual);
+            result.insert(to_string(vd, vs, w, true));
+        } else {
+            result.insert(to_string(vd, vs, w, false));
+        }
+    }
+
+    // Intervals
     for (vert_id v : g_excl.verts()) {
-        if (!this->rev_map[v]) {
+        const auto pvar = this->rev_map[v];
+        if (!pvar || !representatives.contains(*pvar)) {
             continue;
         }
         if (!this->g.elem(0, v) && !this->g.elem(v, 0)) {
@@ -1147,7 +1195,7 @@ string_invariant SplitDBM::to_set() const {
                          this->g.elem(0, v) ? number_t(this->g.edge_val(0, v)) : extended_number::plus_infinity()};
         assert(!v_out.is_bottom());
 
-        variable_t variable = *this->rev_map[v];
+        variable_t variable = *pvar;
 
         std::stringstream elem;
         elem << variable;
@@ -1164,7 +1212,7 @@ string_invariant SplitDBM::to_set() const {
             }
         } else {
             elem << "=";
-            if (v_out.lb() == v_out.ub()) {
+            if (v_out.is_singleton()) {
                 elem << v_out.lb();
             } else {
                 elem << v_out;
@@ -1173,40 +1221,13 @@ string_invariant SplitDBM::to_set() const {
         result.insert(elem.str());
     }
 
-    std::set<std::tuple<variable_t, variable_t, Weight>> diff_csts;
-    for (vert_id s : g_excl.verts()) {
-        if (!this->rev_map[s]) {
-            continue;
-        }
-        variable_t vs = *this->rev_map[s];
-        for (vert_id d : g_excl.succs(s)) {
-            if (!this->rev_map[d]) {
-                continue;
-            }
-            variable_t vd = *this->rev_map[d];
-            diff_csts.emplace(vd, vs, g_excl.edge_val(s, d));
-        }
-    }
-    // simplify: x - y <= k && y - x <= -k
-    //        -> x <= y + k <= x
-    //        -> x = y + k
-    for (const auto& [vd, vs, w] : diff_csts) {
-        auto dual = to_string(vs, vd, -w, false);
-        if (result.count(dual)) {
-            result.erase(dual);
-            result.insert(to_string(vd, vs, w, true));
-        } else {
-            result.insert(to_string(vd, vs, w, false));
-        }
-    }
     return string_invariant{result};
 }
 
 std::ostream& operator<<(std::ostream& o, const SplitDBM& dom) { return o << dom.to_set(); }
 
 bool SplitDBM::eval_expression_overflow(const linear_expression_t& e, Weight& out) const {
-    [[maybe_unused]]
-    const bool overflow = convert_NtoW_overflow(e.constant_term(), out);
+    [[maybe_unused]] const bool overflow = convert_NtoW_overflow(e.constant_term(), out);
     assert(!overflow);
     for (const auto& [variable, coefficient] : e.variable_terms()) {
         Weight coef;
diff --git a/src/crab/var_factory.cpp b/src/crab/var_factory.cpp
index 7eeaadf54..5497a384a 100644
--- a/src/crab/var_factory.cpp
+++ b/src/crab/var_factory.cpp
@@ -191,6 +191,8 @@ std::vector<variable_t> variable_t::get_type_variables() {
 
 bool variable_t::is_in_stack() const { return this->name()[0] == 's'; }
 
+bool variable_t::printing_order(const variable_t& a, const variable_t& b) { return a.name() < b.name(); }
+
 std::vector<variable_t> variable_t::get_loop_counters() {
     std::vector<variable_t> res;
     for (const std::string& name : *names) {
diff --git a/src/crab/variable.hpp b/src/crab/variable.hpp
index bb0075aea..719a2eb85 100644
--- a/src/crab/variable.hpp
+++ b/src/crab/variable.hpp
@@ -78,6 +78,7 @@ class variable_t final {
     static variable_t loop_counter(const std::string& label);
     [[nodiscard]]
     bool is_in_stack() const;
+    static bool printing_order(const variable_t& a, const variable_t& b);
 }; // class variable_t
 
 } // namespace crab
diff --git a/test-data/add.yaml b/test-data/add.yaml
index 7d29c6011..f9618a1b4 100644
--- a/test-data/add.yaml
+++ b/test-data/add.yaml
@@ -25,7 +25,6 @@ code:
 post:
   - r0.type=number
   - r0.svalue=[2147483649, 2147483651]
-  - r0.uvalue=[2147483649, 2147483651]
   - r0.svalue=r0.uvalue
 ---
 test-case: add immediate to unknown number
@@ -90,7 +89,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[10, 15]
-  - r1.uvalue=[10, 15]
   - r1.svalue=r1.uvalue
 
 ---
@@ -106,15 +104,12 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[10, 15]
-  - r1.uvalue=[10, 15]
   - r2.type=number
   - r2.svalue=5
   - r2.uvalue=5
   - r1.svalue=r1.uvalue
   - r1.svalue-r2.svalue<=10
-  - r1.uvalue-r2.svalue<=10
   - r2.svalue-r1.svalue<=-5
-  - r2.svalue-r1.uvalue<=-5
 
 ---
 test-case: add interval number register to constant register pointer
@@ -130,19 +125,11 @@ post:
   - r2.type=packet
   - r2.packet_offset=[3, 5]
   - r2.svalue=[10, 16]
-  - r2.uvalue=[10, 16]
   - r2.svalue=r2.uvalue
   - r7.type=number
-  - r7.svalue=[3, 5]
   - r7.uvalue=[3, 5]
-  - r7.svalue-r2.svalue<=-7
-  - r7.svalue-r2.uvalue<=-7
-  - r2.svalue-r7.svalue<=11
-  - r2.uvalue-r7.svalue<=11
   - r2.packet_offset-r2.svalue<=-7
-  - r2.packet_offset-r2.uvalue<=-7
   - r2.svalue-r2.packet_offset<=11
-  - r2.uvalue-r2.packet_offset<=11
   - r2.packet_offset=r7.svalue
 
 ---
@@ -159,19 +146,14 @@ post:
   - r7.type=packet
   - r7.packet_offset=[3, 5]
   - r7.svalue=[10, 16]
-  - r7.uvalue=[10, 16]
   - r7.svalue=r7.uvalue
   - r2.type=packet
   - r2.packet_offset=0
   - r2.svalue=[7, 11]
   - r2.uvalue=[7, 11]
   - r2.svalue-r7.svalue<=-3
-  - r2.svalue-r7.uvalue<=-3
   - r7.svalue-r2.svalue<=5
-  - r7.uvalue-r2.svalue<=5
   - r2.packet_offset-r7.packet_offset<=-3
   - r7.packet_offset-r2.packet_offset<=5
   - r7.packet_offset-r7.svalue<=-7
-  - r7.packet_offset-r7.uvalue<=-7
   - r7.svalue-r7.packet_offset<=11
-  - r7.uvalue-r7.packet_offset<=11
diff --git a/test-data/assign.yaml b/test-data/assign.yaml
index cfbf98917..3e1ae396a 100644
--- a/test-data/assign.yaml
+++ b/test-data/assign.yaml
@@ -183,7 +183,6 @@ code:
 post:
   - r2.svalue=[0, 4294967295]
   - r2.svalue=r2.uvalue
-  - r2.uvalue=[0, 4294967295]
   - r10.type=stack
   - r10.stack_offset=512
 
@@ -221,7 +220,6 @@ post:
   - r1.shared_offset=0
   - r1.shared_region_size=16
   - r2.svalue=[0, 4294967295]
-  - r2.uvalue=[0, 4294967295]
   - r2.svalue=r2.uvalue
 
 messages:
@@ -241,7 +239,6 @@ post:
   - r1.shared_region_size=16
   - r1.stack_offset=500
   - r1.stack_numeric_size=16
-  - r2.type in {stack, shared}
   - r2.shared_offset=0
   - r2.shared_region_size=16
   - r2.stack_offset=500
@@ -304,15 +301,12 @@ code:
     r1 = r2
 
 post:
-  - packet_size=r1.packet_offset
+  - packet_size=r1.packet_offset=r2.packet_offset
+  - r1.svalue=r2.svalue
+  - r1.uvalue=r2.uvalue
   - r1.type=packet
   - r1.svalue=[4098, 2147418112]
-  - packet_size=r2.packet_offset
   - r2.type=packet
-  - r2.svalue=[4098, 2147418112]
-  - r1.packet_offset=r2.packet_offset
-  - r1.svalue=r2.svalue
-  - r1.uvalue=r2.uvalue
 ---
 test-case: 32-bit assign register packet value
 
@@ -324,7 +318,6 @@ code:
 
 post:
   - r1.svalue=[0, 4294967295]
-  - r1.uvalue=[0, 4294967295]
   - r1.svalue=r1.uvalue
   - packet_size=r2.packet_offset
   - r2.type=packet
@@ -348,8 +341,6 @@ post:
   - r1.uvalue=[1, 2147418112]
   - r2.ctx_offset=0
   - r2.type=ctx
-  - r2.svalue=[1, 2147418112]
-  - r2.uvalue=[1, 2147418112]
   - r1.svalue=r2.svalue
   - r1.uvalue=r2.uvalue
 ---
@@ -367,7 +358,6 @@ post:
   - r1.svalue=[1, 2147418112]
   - r1.uvalue=[1, 2147418112]
   - r2.svalue=[1, 2147418112]
-  - r2.uvalue=[1, 2147418112]
   - r2.svalue=r2.uvalue
 
 messages:
@@ -401,7 +391,6 @@ post:
   - r1.map_fd=1
   - r1.type=map_fd
   - r2.svalue=[0, 4294967295]
-  - r2.uvalue=[0, 4294967295]
   - r2.svalue=r2.uvalue
 
 messages:
@@ -435,7 +424,6 @@ post:
   - r1.map_fd=1
   - r1.type=map_fd_programs
   - r2.svalue=[0, 4294967295]
-  - r2.uvalue=[0, 4294967295]
   - r2.svalue=r2.uvalue
 
 messages:
diff --git a/test-data/atomic.yaml b/test-data/atomic.yaml
index c5f615d66..b50d9f0a8 100644
--- a/test-data/atomic.yaml
+++ b/test-data/atomic.yaml
@@ -4,224 +4,224 @@
 test-case: atomic 32-bit ADD shared
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u32 *)(r2 + 4) += r1
 
 post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 32-bit ADD and fetch shared
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u32 *)(r2 + 4) += r1 fetch
 
 post: ["r1.type=number",
-       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 64-bit ADD shared
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u64 *)(r2 + 4) += r1
 
 post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 64-bit ADD and fetch shared
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u64 *)(r2 + 4) += r1 fetch
 
 post: ["r1.type=number",
-       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 32-bit AND shared
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u32 *)(r2 + 4) &= r1
 
 post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 32-bit AND and fetch shared
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u32 *)(r2 + 4) &= r1 fetch
 
 post: ["r1.type=number",
-       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 64-bit AND shared
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u64 *)(r2 + 4) &= r1
 
 post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 64-bit AND and fetch shared
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u64 *)(r2 + 4) &= r1 fetch
 
 post: ["r1.type=number",
-       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 32-bit OR shared
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u32 *)(r2 + 4) |= r1
 
 post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 32-bit OR and fetch shared
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u32 *)(r2 + 4) |= r1 fetch
 
 post: ["r1.type=number",
-       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 64-bit OR shared
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u64 *)(r2 + 4) |= r1
 
 post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 64-bit OR and fetch shared
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u64 *)(r2 + 4) |= r1 fetch
 
 post: ["r1.type=number",
-       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 32-bit XOR shared
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u32 *)(r2 + 4) ^= r1
 
 post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 32-bit XOR and fetch shared
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u32 *)(r2 + 4) ^= r1 fetch
 
 post: ["r1.type=number",
-       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 64-bit XOR shared
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u64 *)(r2 + 4) ^= r1
 
 post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 64-bit XOR and fetch shared
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u64 *)(r2 + 4) ^= r1 fetch
 
 post: ["r1.type=number",
-       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 32-bit XCHG shared
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u32 *)(r2 + 4) x= r1
 
 post: ["r1.type=number",
-       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 64-bit XCHG shared
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u64 *)(r2 + 4) x= r1
 
 post: ["r1.type=number",
-       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 32-bit CMPXCHG shared
 
 pre: ["r0.type=number", "r0.svalue=1", "r0.uvalue=1",
       "r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
@@ -229,13 +229,13 @@ code:
 
 post: ["r0.type=number",
        "r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 64-bit CMPXCHG shared
 
 pre: ["r0.type=number", "r0.svalue=2", "r0.uvalue=2",
       "r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
@@ -243,19 +243,19 @@ code:
 
 post: ["r0.type=number",
        "r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 ---
 test-case: atomic 32-bit ADD past end of shared region
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=shared", "r2.shared_region_size=10", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=10", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u32 *)(r2 + 4) += r1
 
 post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-       "r2.type=shared", "r2.shared_region_size=10", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=10", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 messages:
   - "0: Upper bound must be at most r2.shared_region_size (valid_access(r2.offset+4, width=4) for write)"
@@ -263,7 +263,7 @@ messages:
 test-case: atomic 32-bit ADD stack
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...7].type=number", "s[4...7].svalue=1", "s[4...7].uvalue=1"]
 
@@ -272,14 +272,14 @@ code:
     lock *(u32 *)(r2 + 4) += r1
 
 post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...7].type=number", "s[4...7].svalue=3", "s[4...7].uvalue=3"]
 ---
 test-case: atomic 32-bit ADD and fetch stack
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...7].type=number", "s[4...7].svalue=1", "s[4...7].uvalue=1"]
 
@@ -288,14 +288,14 @@ code:
     lock *(u32 *)(r2 + 4) += r1 fetch
 
 post: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...7].type=number", "s[4...7].svalue=3", "s[4...7].uvalue=3"]
 ---
 test-case: atomic 64-bit ADD stack
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...11].type=number", "s[4...11].svalue=1", "s[4...11].uvalue=1"]
 
@@ -304,14 +304,14 @@ code:
     lock *(u64 *)(r2 + 4) += r1
 
 post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...11].type=number", "s[4...11].svalue=3", "s[4...11].uvalue=3"]
 ---
 test-case: atomic 64-bit ADD and fetch stack
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...11].type=number", "s[4...11].svalue=1", "s[4...11].uvalue=1"]
 
@@ -320,14 +320,14 @@ code:
     lock *(u64 *)(r2 + 4) += r1 fetch
 
 post: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...11].type=number", "s[4...11].svalue=3", "s[4...11].uvalue=3"]
 ---
 test-case: atomic 32-bit AND stack
 
 pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"]
 
@@ -336,14 +336,14 @@ code:
     lock *(u32 *)(r2 + 4) &= r1
 
 post: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...7].type=number", "s[4...7].svalue=1", "s[4...7].uvalue=1"]
 ---
 test-case: atomic 32-bit AND and fetch stack
 
 pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"]
 
@@ -352,14 +352,14 @@ code:
     lock *(u32 *)(r2 + 4) &= r1 fetch
 
 post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...7].type=number", "s[4...7].svalue=1", "s[4...7].uvalue=1"]
 ---
 test-case: atomic 64-bit AND stack
 
 pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"]
 
@@ -368,14 +368,14 @@ code:
     lock *(u64 *)(r2 + 4) &= r1
 
 post: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...11].type=number", "s[4...11].svalue=1", "s[4...11].uvalue=1"]
 ---
 test-case: atomic 64-bit AND and fetch stack
 
 pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"]
 
@@ -384,14 +384,14 @@ code:
     lock *(u64 *)(r2 + 4) &= r1 fetch
 
 post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...11].type=number", "s[4...11].svalue=1", "s[4...11].uvalue=1"]
 ---
 test-case: atomic 32-bit OR stack
 
 pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"]
 
@@ -400,14 +400,14 @@ code:
     lock *(u32 *)(r2 + 4) |= r1
 
 post: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...7].type=number", "s[4...7].svalue=7", "s[4...7].uvalue=7"]
 ---
 test-case: atomic 32-bit OR and fetch stack
 
 pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"]
 
@@ -416,14 +416,14 @@ code:
     lock *(u32 *)(r2 + 4) |= r1 fetch
 
 post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...7].type=number", "s[4...7].svalue=7", "s[4...7].uvalue=7"]
 ---
 test-case: atomic 64-bit OR stack
 
 pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"]
 
@@ -432,14 +432,14 @@ code:
     lock *(u64 *)(r2 + 4) |= r1
 
 post: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...11].type=number", "s[4...11].svalue=7", "s[4...11].uvalue=7"]
 ---
 test-case: atomic 64-bit OR and fetch stack
 
 pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"]
 
@@ -448,14 +448,14 @@ code:
     lock *(u64 *)(r2 + 4) |= r1 fetch
 
 post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...11].type=number", "s[4...11].svalue=7", "s[4...11].uvalue=7"]
 ---
 test-case: atomic 32-bit XOR stack
 
 pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"]
 
@@ -464,14 +464,14 @@ code:
     lock *(u32 *)(r2 + 4) ^= r1
 
 post: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...7].type=number", "s[4...7].svalue=6", "s[4...7].uvalue=6"]
 ---
 test-case: atomic 32-bit XOR and fetch stack
 
 pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"]
 
@@ -480,14 +480,14 @@ code:
     lock *(u32 *)(r2 + 4) ^= r1 fetch
 
 post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...7].type=number", "s[4...7].svalue=6", "s[4...7].uvalue=6"]
 ---
 test-case: atomic 64-bit XOR stack
 
 pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"]
 
@@ -496,14 +496,14 @@ code:
     lock *(u64 *)(r2 + 4) ^= r1
 
 post: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...11].type=number", "s[4...11].svalue=6", "s[4...11].uvalue=6"]
 ---
 test-case: atomic 64-bit XOR and fetch stack
 
 pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"]
 
@@ -512,14 +512,14 @@ code:
     lock *(u64 *)(r2 + 4) ^= r1 fetch
 
 post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...11].type=number", "s[4...11].svalue=6", "s[4...11].uvalue=6"]
 ---
 test-case: atomic 32-bit XCHG stack
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"]
 
@@ -528,14 +528,14 @@ code:
     lock *(u32 *)(r2 + 4) x= r1
 
 post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...7].type=number", "s[4...7].svalue=2", "s[4...7].uvalue=2"]
 ---
 test-case: atomic 64-bit XCHG stack
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"]
 
@@ -544,7 +544,7 @@ code:
     lock *(u64 *)(r2 + 4) x= r1
 
 post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...11].type=number", "s[4...11].svalue=2", "s[4...11].uvalue=2"]
 ---
@@ -552,7 +552,7 @@ test-case: atomic 32-bit CMPXCHG stack
 
 pre: ["r0.type=number", "r0.svalue=1", "r0.uvalue=1",
       "r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...7].type=number", "s[4...7].svalue=1", "s[4...7].uvalue=1"]
 
@@ -562,7 +562,7 @@ code:
 
 post: ["r0.type=number", "r0.svalue=1", "r0.uvalue=1",
        "r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...7].type=number"]
 ---
@@ -570,7 +570,7 @@ test-case: atomic 64-bit CMPXCHG stack
 
 pre: ["r0.type=number", "r0.svalue=1", "r0.uvalue=1",
       "r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+      "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
       "r10.type=stack", "r10.stack_offset=512",
       "s[4...11].type=number", "s[4...11].svalue=1", "s[4...11].uvalue=1"]
 
@@ -580,21 +580,21 @@ code:
 
 post: ["r0.type=number", "r0.svalue=1", "r0.uvalue=1",
        "r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
+       "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue",
        "r10.type=stack", "r10.stack_offset=512",
        "s[4...11].type=number"]
 ---
 test-case: atomic 32-bit ADD to non-pointer space
 
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=number", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
     lock *(u32 *)(r2 + 4) += r1
 
 post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-       "r2.type=number", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=number", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 messages:
   - "0: Invalid type (r2.type in {ctx, stack, packet, shared})"
@@ -604,7 +604,7 @@ test-case: atomic 64-bit CMPXCHG comparing against non-number
 
 pre: ["r0.type=number", "r0.svalue=2", "r0.uvalue=2",
       "r1.type=shared", "r1.shared_region_size=16", "r1.shared_offset=4",
-      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 code:
   <start>: |
@@ -612,7 +612,7 @@ code:
 
 post: ["r0.type=number", "r0.svalue=2", "r0.uvalue=2",
        "r1.type=shared", "r1.shared_region_size=16", "r1.shared_offset=4",
-       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
 
 messages:
   - "0: Invalid type (r1.type == number)"
diff --git a/test-data/call.yaml b/test-data/call.yaml
index f75b4ecb9..fd5c312ee 100644
--- a/test-data/call.yaml
+++ b/test-data/call.yaml
@@ -16,7 +16,6 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
   - r0.svalue=r0.uvalue
   - s[504...511].type=number
 ---
@@ -34,7 +33,6 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
   - r0.svalue=r0.uvalue
 ---
 test-case: bpf_map_lookup_elem packet key
@@ -52,7 +50,6 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
   - r0.svalue=r0.uvalue
   - meta_offset=0
   - packet_size=4
@@ -71,7 +68,6 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
   - r0.svalue=r0.uvalue
 
 messages:
@@ -92,7 +88,6 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
   - r0.svalue=r0.uvalue
 
 messages:
@@ -112,7 +107,6 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
   - r0.svalue=r0.uvalue
 
 messages:
@@ -132,7 +126,6 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
   - r0.svalue=r0.uvalue
 
 messages:
diff --git a/test-data/callx.yaml b/test-data/callx.yaml
index 2af9e0a8e..7baf432aa 100644
--- a/test-data/callx.yaml
+++ b/test-data/callx.yaml
@@ -17,7 +17,6 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
   - r0.svalue=r0.uvalue
   - r8.type=number
   - r8.svalue=1
@@ -39,7 +38,6 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
   - r0.svalue=r0.uvalue
   - r8.type=number
   - r8.svalue=1
@@ -61,7 +59,6 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
   - r0.svalue=r0.uvalue
   - meta_offset=0
   - packet_size=4
@@ -84,7 +81,6 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
   - r0.svalue=r0.uvalue
   - r8.type=number
   - r8.svalue=1
@@ -108,7 +104,6 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
   - r0.svalue=r0.uvalue
   - r8.type=number
   - r8.svalue=1
@@ -132,7 +127,6 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
   - r0.svalue=r0.uvalue
   - r8.type=number
   - r8.svalue=1
@@ -204,7 +198,6 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
   - r0.svalue=r0.uvalue
   - r8.type=number
   - r8.svalue=1
diff --git a/test-data/full64.yaml b/test-data/full64.yaml
index b004151d9..84c82e71b 100644
--- a/test-data/full64.yaml
+++ b/test-data/full64.yaml
@@ -97,7 +97,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=9223372036854775807
-  - r1.uvalue=9223372036854775807
   - r1.svalue=r1.uvalue
 ---
 test-case: not equal 0
@@ -123,7 +122,6 @@ code:
 post:
   - r0.type=number
   - r0.svalue=0
-  - r0.uvalue=0
   - r0.svalue=r0.uvalue
 ---
 test-case: create unsigned infinite interval
@@ -149,7 +147,6 @@ code:
 post:
   - r0.type=number
   - r0.svalue=[1, 9223372036854775807]
-  - r0.uvalue=[1, 9223372036854775807]
   - r0.svalue=r0.uvalue
 ---
 test-case: addition with signed infinite interval
@@ -171,7 +168,7 @@ pre: ["r1.type=number", "r1.svalue=[-1, 2]"]
 
 code:
   <start>: |
-     assume r1 == 1
+    assume r1 == 1
 
 post:
   - r1.type=number
@@ -184,7 +181,7 @@ pre: ["r1.type=number", "r1.svalue=[-1, 2]", "r2.type=number", "r2.svalue=1", "r
 
 code:
   <start>: |
-     assume r1 == 1
+    assume r1 == 1
 
 post:
   - r1.type=number
@@ -201,18 +198,10 @@ pre: ["r1.type=number", "r1.svalue=[-1, 2]",
 
 code:
   <start>: |
-     assume r1 == r2
+    assume r1 == r2
 
 post:
+  - r1.svalue=r1.uvalue=r2.svalue=r2.uvalue
   - r1.type=number
   - r1.svalue=[1, 2]
-  - r1.uvalue=[1, 2]
-  - r1.svalue=r1.uvalue
   - r2.type=number
-  - r2.svalue=[1, 2]
-  - r2.uvalue=[1, 2]
-  - r2.svalue=r2.uvalue
-  - r1.svalue=r2.svalue
-  - r1.svalue=r2.uvalue
-  - r1.uvalue=r2.svalue
-  - r1.uvalue=r2.uvalue
diff --git a/test-data/jump.yaml b/test-data/jump.yaml
index a5ffb1746..f6b0df1e9 100644
--- a/test-data/jump.yaml
+++ b/test-data/jump.yaml
@@ -34,12 +34,8 @@ code:
 post:
   - r0.type=number
   - r0.svalue=[0, 1]
-  - r0.uvalue=[0, 1]
-  - r0.svalue=r0.uvalue
-  - r0.svalue-r1.uvalue<=0
-  - r0.uvalue-r1.uvalue<=0
+  - r0.svalue=r0.uvalue=r1.uvalue
   - r1.type=number
-  - r1.uvalue=[0, +oo]
 ---
 test-case: simple unconditional jump forward
 
@@ -304,7 +300,6 @@ post:
   - r1.type in {number, ctx}
   - r1.type=r2.type
   - r2.ctx_offset=0
-  - r2.type in {number, ctx}
   - r3.type=number
   - r8.ctx_offset=4
   - r8.type=ctx
@@ -413,88 +408,35 @@ code:
     r3 += r2; the domain does not currently store inequalities so we can't yet tell that this is safe
 
 post:
+  - r1.type=r3.type
+  - r1.svalue=r1.uvalue
+  - r2.svalue=r2.uvalue
+  - r2.ctx_offset=r3.ctx_offset
+  - r3.svalue=r3.uvalue
   - r0.type=number
   - r0.uvalue=[0, +oo]
   - r1.ctx_offset=0
   - r1.type in {number, ctx}
   - r1.type-r1.svalue<=-8
-  - r1.type-r1.uvalue<=-8
-  - r1.type-r3.ctx_offset<=-3
-  - r1.type-r3.type<=0
   - r1.type-r3.svalue<=-12
-  - r1.type-r3.uvalue<=-12
   - r1.svalue-r1.type<=1027
-  - r1.uvalue-r1.type<=1027
-  - r1.svalue-r3.ctx_offset<=1024
-  - r1.uvalue-r3.ctx_offset<=1024
-  - r1.svalue-r3.type<=1027
-  - r1.uvalue-r3.type<=1027
   - r1.svalue-r3.svalue<=-4
-  - r1.uvalue-r3.uvalue<=-4
-  - r1.svalue-r3.uvalue<=-4
-  - r1.uvalue-r3.svalue<=-4
   - r1.svalue=[4, 1024]
-  - r1.uvalue=[4, 1024]
-  - r1.svalue=r1.uvalue
   - r2.ctx_offset=0
   - r2.type in {number, ctx}
-  - r2.ctx_offset-r3.ctx_offset<=0
   - r2.type-r2.svalue<=-8
-  - r2.type-r2.uvalue<=-8
   - r2.type-r3.svalue<=-12
-  - r2.type-r3.uvalue<=-12
+  - r2.svalue-r0.uvalue<=1023
   - r2.svalue-r2.type<=1027
-  - r2.uvalue-r2.type<=1027
   - r2.svalue-r3.svalue<=-4
-  - r2.uvalue-r3.uvalue<=-4
-  - r2.svalue-r3.uvalue<=-4
-  - r2.uvalue-r3.svalue<=-4
   - r2.svalue=[4, 1024]
-  - r2.uvalue=[4, 1024]
-  - r2.svalue=r2.uvalue
-  - r2.svalue-r0.uvalue<=1023
   - r2.type-r0.uvalue<=-4
-  - r2.uvalue-r0.uvalue<=1023
-  - r3.ctx_offset-r0.uvalue<=2039
   - r3.svalue-r0.uvalue<=3071
-  - r3.uvalue-r0.uvalue<=3071
-  - r3.ctx_offset-r1.type<=1028
-  - r3.ctx_offset-r1.svalue<=1020
-  - r3.ctx_offset-r1.uvalue<=1020
-  - r3.ctx_offset-r2.ctx_offset<=1024
-  - r3.ctx_offset-r2.type<=2043
-  - r3.ctx_offset-r2.svalue<=1020
-  - r3.ctx_offset-r2.uvalue<=1020
-  - r3.ctx_offset-r3.type<=1027
-  - r3.ctx_offset-r3.svalue<=1016
-  - r3.ctx_offset-r3.uvalue<=1016
-  - r3.ctx_offset=[0, 1024]
-  - r3.type in {number, ctx}
-  - r3.type-r1.type<=1
-  - r3.type-r1.svalue<=-7
-  - r3.type-r1.uvalue<=-7
-  - r3.type-r3.ctx_offset<=-3
-  - r3.type-r3.svalue<=-11
-  - r3.type-r3.uvalue<=-11
   - r3.svalue-r1.type<=3075
-  - r3.uvalue-r1.type<=3075
   - r3.svalue-r1.svalue<=2048
-  - r3.uvalue-r1.uvalue<=2048
-  - r3.svalue-r1.uvalue<=2048
-  - r3.uvalue-r1.svalue<=2048
   - r3.svalue-r2.type<=3075
-  - r3.uvalue-r2.type<=3075
   - r3.svalue-r2.svalue<=2048
-  - r3.uvalue-r2.uvalue<=2048
-  - r3.svalue-r2.uvalue<=2048
-  - r3.uvalue-r2.svalue<=2048
-  - r3.svalue-r3.ctx_offset<=3072
-  - r3.uvalue-r3.ctx_offset<=3072
-  - r3.svalue-r3.type<=3075
-  - r3.uvalue-r3.type<=3075
   - r3.svalue=[8, 3072]
-  - r3.uvalue=[8, 3072]
-  - r3.svalue=r3.uvalue
   - r8.ctx_offset=0
   - r8.type=ctx
   - r8.svalue=1024
@@ -542,7 +484,6 @@ post:
   - r1.type=r2.type
   - r2.stack_offset=0
   - r2.packet_offset=0
-  - r2.type in {packet, stack}
   - r6.type=stack
   - r6.stack_offset=4
   - r7.type=stack
@@ -587,13 +528,9 @@ post:
   - r1.type=packet
   - r1.packet_offset=54
   - r1.packet_offset-packet_size<=18
-  - r1.packet_offset-r2.packet_offset<=18
   - r2.type=packet
-  - r2.packet_offset=[36, 65534]
-  - r2.packet_offset-r1.packet_offset<=65480
   - r4.type=number
   - r4.svalue=[0, 1]
-  - r4.uvalue=[0, 1]
   - r4.svalue=r4.uvalue
 
 messages:
diff --git a/test-data/loop.yaml b/test-data/loop.yaml
index 2aa159e81..2f4195b77 100644
--- a/test-data/loop.yaml
+++ b/test-data/loop.yaml
@@ -18,11 +18,9 @@ code:
 post:
   - "r0.type=number"
   - "r0.svalue=4"
-  - "r0.uvalue=4"
   - "r0.svalue=r0.uvalue"
   - "pc[1]=5"
   - "pc[1]=r0.svalue+1"
-  - "pc[1]=r0.uvalue+1"
 ---
 test-case: until loop, unsigned leq
 options: ["termination"]
@@ -38,13 +36,9 @@ code:
     exit
 
 post:
-  - "r0.type=number"
-  - "r0.svalue=4"
-  - "r0.uvalue=4"
-  - "r0.svalue=r0.uvalue"
-  - "pc[1]=4"
-  - "pc[1]=r0.svalue"
-  - "pc[1]=r0.uvalue"
+  - pc[1]=r0.svalue=r0.uvalue
+  - r0.type=number
+  - pc[1]=4
 ---
 test-case: while loop, signed gte
 options: ["termination"]
@@ -61,13 +55,11 @@ code:
     exit
 
 post:
-  - "r0.type=number"
-  - "r0.svalue=4"
-  - "r0.uvalue=4"
-  - "r0.svalue=r0.uvalue"
-  - "pc[1]=5"
-  - "pc[1]=r0.svalue+1"
-  - "pc[1]=r0.uvalue+1"
+  - r0.type=number
+  - r0.svalue=4
+  - r0.svalue=r0.uvalue
+  - pc[1]=5
+  - pc[1]=r0.svalue+1
 ---
 test-case: until loop, signed leq
 options: ["termination"]
@@ -84,13 +76,9 @@ code:
     exit
 
 post:
-  - "r0.type=number"
-  - "r0.svalue=4"
-  - "r0.uvalue=4"
-  - "r0.svalue=r0.uvalue"
-  - "pc[1]=4"
-  - "pc[1]=r0.svalue"
-  - "pc[1]=r0.uvalue"
+  - pc[1]=r0.svalue=r0.uvalue
+  - r0.type=number
+  - pc[1]=4
 ---
 test-case: loop with data dependence, unsigned leq
 options: ["termination"]
@@ -109,16 +97,12 @@ code:
     exit
 
 post:
-  - "r0.type=number"
-  - "r0.svalue=[1, 4]"
-  - "r0.uvalue=[1, 4]"
-  - "r0.svalue=r0.uvalue"
-  - "r1.type=number"
-  - "r2.type=number"
-  - "r3.type=number"
-  - "pc[1]=[1, 4]"
-  - "pc[1]=r0.svalue"
-  - "pc[1]=r0.uvalue"
+  - pc[1]=r0.svalue=r0.uvalue
+  - r0.type=number
+  - r1.type=number
+  - r2.type=number
+  - r3.type=number
+  - pc[1]=[1, 4]
 ---
 test-case: while loop, eq
 # options: ["termination"]
@@ -222,50 +206,18 @@ code:
     exit
 
 post:
+  - packet_size=r2.svalue=r2.uvalue
+  - pc[7]=r3.svalue=r3.uvalue=r4.svalue=r4.uvalue
   - meta_offset=[-oo, 0]
   - packet_size=[1, 65534]
-  - packet_size=r2.svalue
-  - packet_size=r2.uvalue
-  - pc[7]-packet_size<=0
-  - pc[7]-r2.svalue<=0
-  - pc[7]-r2.uvalue<=0
   - pc[7]=[1, 255]
-  - pc[7]=r3.svalue
-  - pc[7]=r3.uvalue
-  - pc[7]=r4.svalue
-  - pc[7]=r4.uvalue
   - r0.type=number
   - r1.packet_offset=0
   - r1.svalue=[4098, 2147418112]
   - r1.type=packet
-  - r2.svalue=[1, 65534]
-  - r2.svalue=r2.uvalue
   - r2.type=number
-  - r2.uvalue=[1, 65534]
-  - r3.svalue-packet_size<=0
-  - r3.svalue-r2.svalue<=0
-  - r3.svalue-r2.uvalue<=0
-  - r3.svalue=[1, 255]
-  - r3.svalue=r3.uvalue
-  - r3.svalue=r4.svalue
-  - r3.svalue=r4.uvalue
   - r3.type=number
-  - r3.uvalue-packet_size<=0
-  - r3.uvalue-r2.svalue<=0
-  - r3.uvalue-r2.uvalue<=0
-  - r3.uvalue=[1, 255]
-  - r3.uvalue=r4.svalue
-  - r3.uvalue=r4.uvalue
-  - r4.svalue-packet_size<=0
-  - r4.svalue-r2.svalue<=0
-  - r4.svalue-r2.uvalue<=0
-  - r4.svalue=[1, 255]
-  - r4.svalue=r4.uvalue
   - r4.type=number
-  - r4.uvalue-packet_size<=0
-  - r4.uvalue-r2.svalue<=0
-  - r4.uvalue-r2.uvalue<=0
-  - r4.uvalue=[1, 255]
 
 ---
 test-case: simple infinite loop, less than
@@ -386,13 +338,9 @@ code:
   <out>: |
     exit
 post:
-  - "pc[0]=1000001"
-  - "pc[0]=r0.svalue"
-  - "pc[0]=r0.uvalue"
-  - "r0.svalue=1000001"
-  - "r0.svalue=r0.uvalue"
-  - "r0.type=number"
-  - "r0.uvalue=1000001"
+  - pc[0]=1000001
+  - pc[0]=r0.svalue=r0.uvalue
+  - r0.type=number
 messages:
   - "0 (counter): Loop counter is too large (pc[0] < 100000)"
 
@@ -407,10 +355,10 @@ code:
     exit
 
 post:
-  - "pc[0]=[1, +oo]"
-  - "r0.svalue=0"
-  - "r0.uvalue=0"
-  - "r0.type=number"
+  - pc[0]=[1, +oo]
+  - r0.svalue=0
+  - r0.uvalue=0
+  - r0.type=number
 
 messages:
   - "0 (counter): Loop counter is too large (pc[0] < 100000)"
@@ -433,9 +381,9 @@ code:
     goto <one>
 
 post:
-  - "r0.svalue=3"
-  - "r0.uvalue=3"
-  - "r0.type=number"
+  - r0.svalue=3
+  - r0.uvalue=3
+  - r0.type=number
 
 messages: []
 
diff --git a/test-data/movsx.yaml b/test-data/movsx.yaml
index 6a3d3c835..23afd0ab5 100644
--- a/test-data/movsx.yaml
+++ b/test-data/movsx.yaml
@@ -12,7 +12,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=384
-  - r1.uvalue=384
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=4294967168
@@ -29,7 +28,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=98304
-  - r1.uvalue=98304
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=4294934528
@@ -46,7 +44,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=384
-  - r1.uvalue=384
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=-128
@@ -63,7 +60,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=98304
-  - r1.uvalue=98304
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=-32768
@@ -80,7 +76,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=2147483648
-  - r1.uvalue=2147483648
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=-2147483648
@@ -110,11 +105,9 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[128, 130]
-  - r1.uvalue=[128, 130]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[4294967168, 4294967170]
-  - r2.uvalue=[4294967168, 4294967170]
   - r2.svalue=r2.uvalue
 ---
 test-case: movsx8 register range to 32 bits with wrap
@@ -128,11 +121,9 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[255, 257]
-  - r1.uvalue=[255, 257]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[0, 4294967295]
-  - r2.uvalue=[0, 4294967295]
   - r2.svalue=r2.uvalue
 ---
 test-case: movsx16 register range to 32 bits without wrap
@@ -146,11 +137,9 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[32768, 32770]
-  - r1.uvalue=[32768, 32770]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[4294934528, 4294934530]
-  - r2.uvalue=[4294934528, 4294934530]
   - r2.svalue=r2.uvalue
 ---
 test-case: movsx16 register range to 32 bits with wrap
@@ -164,11 +153,9 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[65535, 65537]
-  - r1.uvalue=[65535, 65537]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[0, 4294967295]
-  - r2.uvalue=[0, 4294967295]
   - r2.svalue=r2.uvalue
 ---
 test-case: movsx8 register range to 64 bits
@@ -182,7 +169,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[255, 257]
-  - r1.uvalue=[255, 257]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[-1, 1]
@@ -198,7 +184,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[255, 511]
-  - r1.uvalue=[255, 511]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[-128, 127]
@@ -214,7 +199,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[65535, 65537]
-  - r1.uvalue=[65535, 65537]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[-1, 1]
@@ -230,7 +214,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[65535, 131071]
-  - r1.uvalue=[65535, 131071]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[-32768, 32767]
@@ -246,7 +229,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[4294967295, 4294967297]
-  - r1.uvalue=[4294967295, 4294967297]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[-1, 1]
@@ -262,7 +244,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[4294967295, 8589934591]
-  - r1.uvalue=[4294967295, 8589934591]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[-2147483648, 2147483647]
diff --git a/test-data/packet.yaml b/test-data/packet.yaml
index fd7e46bee..e0cf2abe0 100644
--- a/test-data/packet.yaml
+++ b/test-data/packet.yaml
@@ -43,7 +43,7 @@ code:
 
 post: ["meta_offset=0",
        "r1.type=packet", "r1.packet_offset=0", "r1.svalue=[4098, 2147418112]", "r1.uvalue=[4098, 2147418112]",
-       "r2.type=packet", "r2.packet_offset=[0, 65534]", "packet_size=r2.packet_offset",
+       "r2.type=packet", "packet_size=r2.packet_offset",
        "packet_size=[0, 65534]", "r4.type=number", "r4.svalue=0", "r4.uvalue=0"]
 messages:
   - "1: Upper bound must be at most packet_size (valid_access(r1.offset, width=8) for write)"
@@ -61,7 +61,7 @@ code:
 
 post: ["meta_offset=0",
        "r1.type=packet", "r1.packet_offset=0", "r1.svalue=[4098, 2147418112]", "r1.uvalue=[4098, 2147418112]",
-       "r2.type=packet", "r2.packet_offset=[0, 65534]", "packet_size=r2.packet_offset",
+       "r2.type=packet", "packet_size=r2.packet_offset",
        "packet_size=[0, 65534]", "r4.type=number"]
 messages:
   - "0: Upper bound must be at most packet_size (valid_access(r1.offset, width=8) for read)"
@@ -85,12 +85,11 @@ code:
 
 post: ["meta_offset=0",
        "r1.type=packet", "r1.packet_offset=0", "r1.svalue=[4098, 2147418112]", "r1.uvalue=[4098, 2147418112]",
-       "r2.type=packet", "r2.packet_offset=[0, 65534]", "packet_size=r2.packet_offset",
-       "r3.type=packet", "r3.packet_offset=4", "r3.svalue=[4102, 2147418116]", "r3.uvalue=[4102, 2147418116]",
+       "r2.type=packet", "packet_size=r2.packet_offset",
+       "r3.type=packet", "r3.packet_offset=4", "r3.svalue=[4102, 2147418116]",
        "r3.svalue=r3.uvalue",
        "packet_size-r3.packet_offset<=65530", "packet_size=[0, 65534]",
-       "r3.packet_offset-packet_size<=4", "r3.svalue=r1.svalue+4", "r3.uvalue=r1.svalue+4",
-       "r2.packet_offset-r3.packet_offset<=65530", "r3.packet_offset-r2.packet_offset<=4"]
+       "r3.packet_offset-packet_size<=4", "r3.svalue=r1.svalue+4"]
 messages:
   - "4: Upper bound must be at most packet_size (valid_access(r1.offset, width=8) for write)"
 
@@ -113,12 +112,11 @@ code:
 
 post: ["meta_offset=0",
        "r1.type=packet", "r1.packet_offset=0", "r1.svalue=[4098, 2147418112]", "r1.uvalue=[4098, 2147418112]",
-       "r2.type=packet", "r2.packet_offset=[0, 65534]", "packet_size=r2.packet_offset",
-       "r3.type=packet", "r3.packet_offset=8", "r3.svalue=[4106, 2147418120]", "r3.uvalue=[4106, 2147418120]",
+       "r2.type=packet", "packet_size=r2.packet_offset",
+       "r3.type=packet", "r3.packet_offset=8", "r3.svalue=[4106, 2147418120]",
        "packet_size-r3.packet_offset<=65526", "packet_size=[0, 65534]",
-       "r3.packet_offset-packet_size<=8", "r3.svalue=r1.svalue+8", "r3.uvalue=r1.svalue+8",
-       "r3.svalue=r3.uvalue",
-       "r2.packet_offset-r3.packet_offset<=65526", "r3.packet_offset-r2.packet_offset<=8"]
+       "r3.packet_offset-packet_size<=8", "r3.svalue=r1.svalue+8",
+       "r3.svalue=r3.uvalue"]
 ---
 test-case: legacy 1 byte packet access imm
 
diff --git a/test-data/pointer.yaml b/test-data/pointer.yaml
index c7ac78cd1..b24d3707a 100644
--- a/test-data/pointer.yaml
+++ b/test-data/pointer.yaml
@@ -63,7 +63,6 @@ code:
 post:
   - "r1.svalue=[0, 4294967295]"
   - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -89,7 +88,6 @@ code:
 post:
   - "r1.svalue=[0, 4294967295]"
   - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -115,7 +113,6 @@ code:
 post:
   - "r1.svalue=[0, 4294967295]"
   - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -130,7 +127,6 @@ pre:
   - "r1.svalue=[0, 4294967295]"
   - "r1.svalue=r1.uvalue"
   - "r1.type=ctx"
-  - "r1.uvalue=[0, 4294967295]"
 
 # Trigger 32-bit ALU operation without changing the value
 code:
@@ -141,7 +137,6 @@ code:
 post:
   - "r1.svalue=[0, 4294967295]"
   - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -167,7 +162,6 @@ code:
 post:
   - "r1.svalue=[0, 4294967295]"
   - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -193,7 +187,6 @@ code:
 post:
   - "r1.svalue=[0, 4294967295]"
   - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -219,7 +212,6 @@ code:
 post:
   - "r1.svalue=[0, 4294967295]"
   - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -245,7 +237,6 @@ code:
 post:
   - "r1.svalue=[0, 4294967295]"
   - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -271,7 +262,6 @@ code:
 post:
   - "r1.svalue=[0, 4294967295]"
   - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -297,7 +287,6 @@ code:
 post:
   - "r1.svalue=[0, 4294967295]"
   - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -323,7 +312,6 @@ code:
 post:
   - "r1.svalue=[0, 4294967295]"
   - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -363,11 +351,11 @@ pre:
   - r0.uvalue=[0, 4294967295]
   - r0.svalue=r0.uvalue
   - r0.type=number
-  - "r1.ctx_offset=0"
-  - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
-  - "r1.type=ctx"
-  - "r1.uvalue=[0, 4294967295]"
+  - r1.ctx_offset=0
+  - r1.svalue=[0, 4294967295]
+  - r1.svalue=r1.uvalue
+  - r1.type=ctx
+  - r1.uvalue=[0, 4294967295]
 
 code:
   <start>: |
@@ -375,20 +363,12 @@ code:
     exit
 
 post:
+  - r0.svalue=r0.uvalue=r1.svalue=r1.uvalue
   - r0.ctx_offset=0
   - r0.svalue=[0, 4294967295]
-  - r0.svalue=r0.uvalue
-  - r0.svalue=r1.svalue
-  - r0.svalue=r1.uvalue
   - r0.type=ctx
-  - r0.uvalue=[0, 4294967295]
-  - r0.uvalue=r1.svalue
-  - r0.uvalue=r1.uvalue
   - r1.ctx_offset=0
-  - r1.svalue=[0, 4294967295]
-  - r1.svalue=r1.uvalue
   - r1.type=ctx
-  - r1.uvalue=[0, 4294967295]
 
 messages:
   - "1: Invalid type (r0.type == number)"
@@ -401,11 +381,11 @@ pre:
   - r0.uvalue=0
   - r0.svalue=r0.uvalue
   - r0.type=number
-  - "r1.ctx_offset=0"
-  - "r1.svalue=1234567890"
-  - "r1.svalue=r1.uvalue"
-  - "r1.type=ctx"
-  - "r1.uvalue=1234567890"
+  - r1.ctx_offset=0
+  - r1.svalue=1234567890
+  - r1.svalue=r1.uvalue
+  - r1.type=ctx
+  - r1.uvalue=1234567890
 
 code:
   <start>: |
@@ -416,7 +396,6 @@ post:
   - r1.svalue=1234567890
   - r1.svalue=r1.uvalue
   - r1.type=ctx
-  - r1.uvalue=1234567890
   - r0.svalue=1234567890
   - r0.type=number
   - r0.uvalue=1234567890
diff --git a/test-data/sdivmod.yaml b/test-data/sdivmod.yaml
index 3e59e49cd..d0dd0efaf 100644
--- a/test-data/sdivmod.yaml
+++ b/test-data/sdivmod.yaml
@@ -162,11 +162,9 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[0, 5]
-  - r2.uvalue=[0, 5]
   - r2.svalue=r2.uvalue
 
 messages:
@@ -347,7 +345,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[-5, 5]
@@ -390,11 +387,9 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[0, 5]
-  - r2.uvalue=[0, 5]
   - r2.svalue=r2.uvalue
 
 messages:
@@ -435,7 +430,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
   - r1.svalue=r1.uvalue
   - r2.type=number
 
@@ -474,7 +468,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4]
-  - r1.uvalue=[0, 4]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[1, 5]
@@ -518,7 +511,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 2]
-  - r1.uvalue=[0, 2]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[-3, -2]
@@ -587,5 +579,4 @@ code:
 post:
   - r0.type=number
   - r0.svalue=[0, 2055]
-  - r0.uvalue=[0, 2055]
   - r0.svalue=r0.uvalue
diff --git a/test-data/sext.yaml b/test-data/sext.yaml
index 0846b4f0e..d2170dc1f 100644
--- a/test-data/sext.yaml
+++ b/test-data/sext.yaml
@@ -17,7 +17,6 @@ post:
   - r1.type=number
   - r1.uvalue=[0, 5]
   - r2.type=number
-  - r2.uvalue=[0, 5]
   - r1.uvalue=r2.uvalue
 ---
 test-case: small sext relational nop
@@ -34,7 +33,6 @@ post:
   - r1.type=number
   - r1.svalue=[-5, 5]
   - r2.type=number
-  - r2.svalue=[-5, 5]
   - r1.svalue=r2.svalue
 ---
 test-case: large zext relational is two shifts
@@ -51,7 +49,6 @@ post:
   - r1.type=number
   - r1.svalue=[0, 4294967295]
   - r1.svalue=r1.uvalue
-  - r1.uvalue=[0, 4294967295]
   - r2.type=number
   - r2.uvalue=[0, 4294967299]
 ---
diff --git a/test-data/shift.yaml b/test-data/shift.yaml
index 8d3b1c5f5..3471692c5 100644
--- a/test-data/shift.yaml
+++ b/test-data/shift.yaml
@@ -236,7 +236,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 65536]
-  - r1.uvalue=[0, 65536]
   - r1.svalue=r1.uvalue
 ---
 test-case: 64-bit signed right shift interval by imm
@@ -250,7 +249,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 65536]
-  - r1.uvalue=[0, 65536]
   - r1.svalue=r1.uvalue
 ---
 test-case: 64-bit unsigned right shift interval by reg
@@ -265,7 +263,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 65536]
-  - r1.uvalue=[0, 65536]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=16
@@ -283,7 +280,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 65536]
-  - r1.uvalue=[0, 65536]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=16
@@ -300,7 +296,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 255]
-  - r1.uvalue=[0, 255]
   - r1.svalue=r1.uvalue
 ---
 test-case: signed 32-bit right shift interval by imm
@@ -314,7 +309,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 255]
-  - r1.uvalue=[0, 255]
   - r1.svalue=r1.uvalue
 ---
 test-case: 32-bit unsigned right shift interval by reg
@@ -329,7 +323,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 255]
-  - r1.uvalue=[0, 255]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=8
@@ -347,7 +340,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 255]
-  - r1.uvalue=[0, 255]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=8
@@ -364,7 +356,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 255]
-  - r1.uvalue=[0, 255]
   - r1.svalue=r1.uvalue
 ---
 test-case: 32-bit signed right shift interval by imm with truncation
@@ -378,7 +369,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294967295]
-  - r1.uvalue=[0, 4294967295]
   - r1.svalue=r1.uvalue
 ---
 test-case: 32-bit unsigned right shift interval by reg with truncation
@@ -393,7 +383,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 255]
-  - r1.uvalue=[0, 255]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=24
@@ -411,7 +400,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294967295]
-  - r1.uvalue=[0, 4294967295]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=24
@@ -428,7 +416,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[16776960, 16777215]
-  - r1.uvalue=[16776960, 16777215]
   - r1.svalue=r1.uvalue
 ---
 test-case: 32-bit signed right shift interval by imm with negatives
@@ -442,7 +429,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[4294967040, 4294967295]
-  - r1.uvalue=[4294967040, 4294967295]
   - r1.svalue=r1.uvalue
 ---
 test-case: 32-bit unsigned right shift interval by reg with negatives
@@ -457,7 +443,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[16776960, 16777215]
-  - r1.uvalue=[16776960, 16777215]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=8
@@ -475,7 +460,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[4294967040, 4294967295]
-  - r1.uvalue=[4294967040, 4294967295]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=8
@@ -492,7 +476,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 16777215]
-  - r1.uvalue=[0, 16777215]
   - r1.svalue=r1.uvalue
 ---
 test-case: 32-bit signed right shift interval by imm crossing zero
@@ -506,7 +489,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294967295]
-  - r1.uvalue=[0, 4294967295]
   - r1.svalue=r1.uvalue
 ---
 test-case: 32-bit unsigned right shift interval by reg crossing zero
@@ -521,7 +503,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 16777215]
-  - r1.uvalue=[0, 16777215]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=8
@@ -539,7 +520,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294967295]
-  - r1.uvalue=[0, 4294967295]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=8
@@ -668,7 +648,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[65536, 4294967296]
-  - r1.uvalue=[65536, 4294967296]
   - r1.svalue=r1.uvalue
 ---
 test-case: 64-bit left shift interval by reg
@@ -683,7 +662,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[65536, 4294967296]
-  - r1.uvalue=[65536, 4294967296]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=16
@@ -728,7 +706,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[65536, 4294901760]
-  - r1.uvalue=[65536, 4294901760]
   - r1.svalue=r1.uvalue
 ---
 test-case: 32-bit left shift interval by reg
@@ -743,7 +720,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[65536, 4294901760]
-  - r1.uvalue=[65536, 4294901760]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=16
@@ -760,7 +736,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
   - r1.svalue=r1.uvalue
 ---
 test-case: 32-bit left shift interval by reg with wrap
@@ -775,7 +750,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=16
@@ -792,7 +766,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
   - r1.svalue=r1.uvalue
 ---
 test-case: 32-bit left shift interval by reg with another wrap
@@ -807,7 +780,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=16
@@ -850,7 +822,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
   - r1.svalue=r1.uvalue
 ---
 test-case: 32-bit left shift top by reg
@@ -865,7 +836,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=16
@@ -882,7 +852,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
   - r1.svalue=r1.uvalue
 ---
 test-case: 32-bit left shift interval by reg with longer wrap
@@ -897,7 +866,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=16
@@ -914,7 +882,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
   - r1.svalue=r1.uvalue
 ---
 test-case: 32-bit left shift interval by reg with another long wrap
@@ -929,7 +896,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=16
@@ -946,7 +912,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[4278190336, 4294967040]
-  - r1.uvalue=[4278190336, 4294967040]
   - r1.svalue=r1.uvalue
 ---
 test-case: 32-bit left shift interval by reg with negatives
@@ -961,7 +926,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[4278190336, 4294967040]
-  - r1.uvalue=[4278190336, 4294967040]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=8
@@ -978,7 +942,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294967040]
-  - r1.uvalue=[0, 4294967040]
   - r1.svalue=r1.uvalue
 ---
 test-case: 32-bit left shift interval by reg crossing zero
@@ -993,7 +956,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294967040]
-  - r1.uvalue=[0, 4294967040]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=8
@@ -1012,7 +974,6 @@ post:
   - r1.type=number
   - r2.type=number
   - r2.svalue=[1, 2]
-  - r2.uvalue=[1, 2]
   - r2.svalue=r2.uvalue
 ---
 test-case: unsigned right shift by interval
@@ -1028,7 +989,6 @@ post:
   - r1.type=number
   - r2.type=number
   - r2.svalue=[1, 2]
-  - r2.uvalue=[1, 2]
   - r2.svalue=r2.uvalue
 ---
 test-case: signed right shift by interval
@@ -1044,7 +1004,6 @@ post:
   - r1.type=number
   - r2.type=number
   - r2.svalue=[1, 2]
-  - r2.uvalue=[1, 2]
   - r2.svalue=r2.uvalue
 ---
 test-case: unsigned right shift TOP by 32 imm
@@ -1058,7 +1017,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294967295]
-  - r1.uvalue=[0, 4294967295]
   - r1.svalue=r1.uvalue
 ---
 test-case: signed right shift TOP by 32 imm
@@ -1084,7 +1042,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294967295]
-  - r1.uvalue=[0, 4294967295]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=32
diff --git a/test-data/stack.yaml b/test-data/stack.yaml
index 8df80ca1e..2870104d8 100644
--- a/test-data/stack.yaml
+++ b/test-data/stack.yaml
@@ -467,18 +467,14 @@ code:
     r3 = *(u64 *)(r10 - 16)
 
 post:
+  - r2.svalue=r3.svalue=s[496...503].svalue
+  - r2.uvalue=r3.uvalue=s[496...503].uvalue
   - r2.type=stack
   - r2.stack_offset=504
   - r2.stack_numeric_size=8
-  - r2.svalue=s[496...503].svalue
-  - r2.uvalue=s[496...503].uvalue
-  - r2.svalue=r3.svalue
-  - r2.uvalue=r3.uvalue
   - r3.type=stack
   - r3.stack_offset=504
   - r3.stack_numeric_size=8
-  - r3.svalue=s[496...503].svalue
-  - r3.uvalue=s[496...503].uvalue
   - r10.type=stack
   - r10.stack_offset=512
   - s[496...503].type=stack
diff --git a/test-data/subtract.yaml b/test-data/subtract.yaml
index a065a6b84..304ec4f76 100644
--- a/test-data/subtract.yaml
+++ b/test-data/subtract.yaml
@@ -25,7 +25,6 @@ code:
 post:
   - r0.type=number
   - r0.svalue=[2147483645, 2147483647]
-  - r0.uvalue=[2147483645, 2147483647]
   - r0.svalue=r0.uvalue
 ---
 test-case: subtract a register from itself
@@ -151,7 +150,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[3810, 3990]
-  - r1.uvalue=[3810, 3990]
   - r1.svalue=r1.uvalue
   - r2.type=stack
   - r2.stack_offset=[140, 230]
diff --git a/test-data/udivmod.yaml b/test-data/udivmod.yaml
index 85c833b86..bd1f7bd00 100644
--- a/test-data/udivmod.yaml
+++ b/test-data/udivmod.yaml
@@ -121,7 +121,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[-5, 5]
@@ -164,11 +163,9 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[0, 5]
-  - r2.uvalue=[0, 5]
   - r2.svalue=r2.uvalue
 
 messages:
@@ -209,7 +206,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
   - r1.svalue=r1.uvalue
   - r2.type=number
 
@@ -351,7 +347,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[-5, 5]
@@ -394,11 +389,9 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[0, 5]
-  - r2.uvalue=[0, 5]
   - r2.svalue=r2.uvalue
 
 messages:
@@ -439,7 +432,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
   - r1.svalue=r1.uvalue
   - r2.type=number
 
@@ -478,7 +470,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4]
-  - r1.uvalue=[0, 4]
   - r1.svalue=r1.uvalue
   - r2.type=number
   - r2.svalue=[1, 5]
@@ -591,5 +582,4 @@ code:
 post:
   - r0.type=number
   - r0.svalue=[0, 2055]
-  - r0.uvalue=[0, 2055]
   - r0.svalue=r0.uvalue
diff --git a/test-data/uninit.yaml b/test-data/uninit.yaml
index aada2a9d1..8e3d7285b 100644
--- a/test-data/uninit.yaml
+++ b/test-data/uninit.yaml
@@ -69,7 +69,6 @@ post:
   - "r0.svalue=[0, 1]"
   - "r0.svalue=r0.uvalue"
   - "r0.type=number"
-  - "r0.uvalue=[0, 1]"
 
 messages:
   - "0: Only numbers can be used as divisors (r3 != 0)"
@@ -109,7 +108,6 @@ post:
   - "r0.svalue=[0, 1]"
   - "r0.svalue=r0.uvalue"
   - "r0.type=number"
-  - "r0.uvalue=[0, 1]"
 
 messages:
   - "0: Only numbers can be used as divisors (r3 != 0)"
@@ -130,7 +128,6 @@ post:
   - "r0.svalue=[0, 1]"
   - "r0.svalue=r0.uvalue"
   - "r0.type=number"
-  - "r0.uvalue=[0, 1]"
 
 messages:
   - "0: Only numbers can be used as divisors (r3 != 0)"
diff --git a/test-data/unsigned.yaml b/test-data/unsigned.yaml
index 6fcc0369d..08a5c3d5a 100644
--- a/test-data/unsigned.yaml
+++ b/test-data/unsigned.yaml
@@ -566,28 +566,28 @@ pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.svalue=r1.uv
 code:
   <start>: |
     assume r1 < 2
-post: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=[0, 1]", "r1.svalue=r1.uvalue"]
 ---
 test-case: "assume [0, 1] w< 2 nop"
 pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.svalue=r1.uvalue"]
 code:
   <start>: |
     assume w1 < 2
-post: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=[0, 1]", "r1.svalue=r1.uvalue"]
 ---
 test-case: "assume [0, 1] < 1 narrows to 0"
 pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.svalue=r1.uvalue"]
 code:
   <start>: |
     assume r1 < 1
-post: ["r1.type=number", "r1.svalue=0", "r1.uvalue=0", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=0", "r1.svalue=r1.uvalue"]
 ---
 test-case: "assume [0, 1] w< 1 narrows to 0"
 pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.svalue=r1.uvalue"]
 code:
   <start>: |
     assume w1 < 1
-post: ["r1.type=number", "r1.svalue=0", "r1.uvalue=0", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=0", "r1.svalue=r1.uvalue"]
 ---
 test-case: "assume [0, 1] > 1 implies bottom"
 pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.svalue=r1.uvalue"]
@@ -612,28 +612,28 @@ pre: ["r1.type=number", "r1.svalue=[1, 2]", "r1.uvalue=[1, 2]", "r1.svalue=r1.uv
 code:
   <start>: |
     assume r1 > 1
-post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=2", "r1.svalue=r1.uvalue"]
 ---
 test-case: "assume [1, 2] w> 1 narrows to 2"
 pre: ["r1.type=number", "r1.svalue=[1, 2]", "r1.uvalue=[1, 2]", "r1.svalue=r1.uvalue"]
 code:
   <start>: |
     assume w1 > 1
-post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=2", "r1.svalue=r1.uvalue"]
 ---
 test-case: "assume [1, 3] > 1 narrows to [2, 3]"
 pre: ["r1.type=number", "r1.svalue=[1, 3]", "r1.uvalue=[1, 3]", "r1.svalue=r1.uvalue"]
 code:
   <start>: |
     assume r1 > 1
-post: ["r1.type=number", "r1.svalue=[2, 3]", "r1.uvalue=[2, 3]", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=[2, 3]", "r1.svalue=r1.uvalue"]
 ---
 test-case: "assume [1, 3] w> 1 narrows to [2, 3]"
 pre: ["r1.type=number", "r1.svalue=[1, 3]", "r1.uvalue=[1, 3]", "r1.svalue=r1.uvalue"]
 code:
   <start>: |
     assume w1 > 1
-post: ["r1.type=number", "r1.svalue=[2, 3]", "r1.uvalue=[2, 3]", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=[2, 3]", "r1.svalue=r1.uvalue"]
 ---
 test-case: "assume 1 > 0 nop"
 pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1"]
@@ -654,28 +654,28 @@ pre: ["r1.type=number", "r1.svalue=[1, 9223372036854775807]", "r1.uvalue=[1, 922
 code:
   <start>: |
     assume r1 > 0
-post: ["r1.type=number", "r1.svalue=[1, 9223372036854775807]", "r1.uvalue=[1, 9223372036854775807]", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=[1, 9223372036854775807]", "r1.svalue=r1.uvalue"]
 ---
 test-case: "assume [1, INT32_MAX] w> 0 nop"
 pre: ["r1.type=number", "r1.svalue=[1, 2147483646]", "r1.uvalue=[1, 2147483646]", "r1.svalue=r1.uvalue"]
 code:
   <start>: |
     assume w1 > 0
-post: ["r1.type=number", "r1.svalue=[1, 2147483646]", "r1.uvalue=[1, 2147483646]", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=[1, 2147483646]", "r1.svalue=r1.uvalue"]
 ---
 test-case: "assume [0, INT_MAX] > 1 narrows to [2, INT_MAX]"
 pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775807]", "r1.uvalue=[0, 9223372036854775807]", "r1.svalue=r1.uvalue"]
 code:
   <start>: |
     assume r1 > 1
-post: ["r1.type=number", "r1.svalue=[2, 9223372036854775807]", "r1.uvalue=[2, 9223372036854775807]", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=[2, 9223372036854775807]", "r1.svalue=r1.uvalue"]
 ---
 test-case: "assume [0, INT32_MAX] w> 1 narrows to [2, INT32_MAX]"
 pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]", "r1.svalue=r1.uvalue"]
 code:
   <start>: |
     assume w1 > 1
-post: ["r1.type=number", "r1.svalue=[2, 2147483647]", "r1.uvalue=[2, 2147483647]", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=[2, 2147483647]", "r1.svalue=r1.uvalue"]
 ---
 test-case: "assume [0, INT_MAX] > INT_MAX implies bottom"
 pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775807]", "r1.uvalue=[0, 9223372036854775807]", "r1.svalue=r1.uvalue"]
@@ -702,12 +702,8 @@ code:
   <start>: |
     r2 = 9223372036854775803ll
     assume r1 >= r2
-post: ["r1.type=number", "r1.svalue=9223372036854775803", "r1.uvalue=9223372036854775803", "r1.svalue=r1.uvalue",
-       "r2.type=number", "r2.svalue=9223372036854775803", "r2.uvalue=9223372036854775803",
-       "r2.uvalue-r1.svalue<=0",  # missing: r1.svalue-r2.uvalue<=0; probably avoiding overflow in SplitDBM
-       "r2.svalue-r1.svalue<=0",  # missing: r1.svalue-r2.svalue<=0; probably avoiding overflow in SplitDBM
-       "r2.svalue-r1.uvalue<=0",  # missing: r1.uvalue-r2.svalue<=0; probably avoiding overflow in SplitDBM
-       "r2.uvalue-r1.uvalue<=0"]  # missing: r1.uvalue-r2.uvalue<=0; probably avoiding overflow in SplitDBM
+post: ["r1.type=number", "r1.svalue=9223372036854775803", "r1.svalue=r1.uvalue",
+       "r2.type=number", "r2.svalue=9223372036854775803", "r2.uvalue=9223372036854775803"]
 ---
 test-case: "assume [0, INT32_MAX] w>= INT32_MAX narrows to INT32_MAX"
 pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]", "r1.svalue=r1.uvalue"]
@@ -715,10 +711,8 @@ code:
   <start>: |
     r2 = 2147483647
     assume w1 >= r2
-post: ["r1.type=number", "r1.svalue=2147483647", "r1.uvalue=2147483647", "r1.svalue=r1.uvalue",
-       "r2.type=number", "r2.svalue=2147483647", "r2.uvalue=2147483647",
-       "r2.uvalue-r1.svalue<=0",  # missing: r1.svalue-r2.uvalue<=0; probably avoiding overflow in SplitDBM
-       "r2.uvalue-r1.uvalue<=0"]  # missing: r1.uvalue-r2.uvalue<=0; probably avoiding overflow in SplitDBM
+post: ["r1.type=number", "r1.svalue=2147483647", "r1.svalue=r1.uvalue",
+       "r2.type=number", "r2.svalue=2147483647", "r2.uvalue=2147483647"]
 ---
 test-case: "assume 4294967301 w>= 5 nop"
 pre: ["r1.type=number", "r1.svalue=4294967301", "r1.uvalue=4294967301"]
@@ -754,8 +748,8 @@ code:
   <start>: |
     assume r1 > r2
 post: ["r1.type=number", "r1.svalue=-1", "r1.uvalue=18446744073709551615",
-       "r2.type=number", "r2.svalue=[1, 2]", "r2.uvalue=[1, 2]", "r2.svalue=r2.uvalue",
-       "r2.svalue-r1.uvalue<=-1", "r2.uvalue-r1.uvalue<=-1"]
+       "r2.type=number", "r2.svalue=[1, 2]", "r2.svalue=r2.uvalue",
+       "r2.svalue-r1.uvalue<=-1"]
 ---
 test-case: "assume [-1, 1] >= 2 narrows"
 pre: ["r1.type=number", "r1.svalue=[-1, 1]"]
@@ -771,8 +765,8 @@ code:
   <start>: |
     assume r1 > r2
 post: ["r1.type=number", "r1.svalue=-1", "r1.uvalue=18446744073709551615",
-       "r2.type=number", "r2.svalue=[2, 3]", "r2.uvalue=[2, 3]", "r2.svalue=r2.uvalue",
-       "r2.svalue-r1.uvalue<=-1", "r2.uvalue-r1.uvalue<=-1"]
+       "r2.type=number", "r2.svalue=[2, 3]", "r2.svalue=r2.uvalue",
+       "r2.svalue-r1.uvalue<=-1"]
 ---
 test-case: "assume [-1, 1] < -1 narrows"
 pre: ["r1.type=number", "r1.svalue=[-1, 1]"]
@@ -912,10 +906,9 @@ pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775807]", "r1.uvalue=[0, 922
 code:
   <start>: |
     assume r1 <= r2
-post: ["r1.type=number", "r1.svalue=[0, 9223372036854775807]", "r1.uvalue=[0, 9223372036854775807]", "r1.svalue=r1.uvalue",
-       "r2.type=number", "r2.svalue=[0, 9223372036854775807]", "r2.uvalue=[0, 9223372036854775807]", "r2.svalue=r2.uvalue",
-       "r1.svalue-r2.svalue<=0", "r1.svalue-r2.uvalue<=0",
-       "r1.uvalue-r2.svalue<=0", "r1.uvalue-r2.uvalue<=0"]
+post: ["r1.svalue=r1.uvalue=r2.svalue=r2.uvalue",
+       "r1.type=number", "r1.svalue=[0, 9223372036854775807]",
+       "r2.type=number"]
 ---
 test-case: "assume [0, INT32_MAX] w<= [0, INT32_MAX] implies relation"
 pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]", "r1.svalue=r1.uvalue",
@@ -923,10 +916,9 @@ pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]"
 code:
   <start>: |
     assume w1 <= r2
-post: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]", "r1.svalue=r1.uvalue",
-       "r2.type=number", "r2.svalue=[0, 2147483647]", "r2.uvalue=[0, 2147483647]", "r2.svalue=r2.uvalue",
-       "r1.svalue-r2.svalue<=0", "r1.svalue-r2.uvalue<=0",
-       "r1.uvalue-r2.svalue<=0", "r1.uvalue-r2.uvalue<=0"]
+post: ["r1.svalue=r1.uvalue=r2.svalue=r2.uvalue",
+       "r1.type=number", "r1.svalue=[0, 2147483647]",
+       "r2.type=number"]
 ---
 test-case: "assume [0, INT_MAX] >= [0, INT_MAX] implies relation"
 pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775807]", "r1.uvalue=[0, 9223372036854775807]", "r1.svalue=r1.uvalue",
@@ -934,10 +926,8 @@ pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775807]", "r1.uvalue=[0, 922
 code:
   <start>: |
     assume r1 >= r2
-post: ["r1.type=number", "r1.svalue=[0, 9223372036854775807]", "r1.uvalue=[0, 9223372036854775807]", "r1.svalue=r1.uvalue",
-       "r2.type=number", "r2.svalue=[0, 9223372036854775807]", "r2.uvalue=[0, 9223372036854775807]", "r2.svalue=r2.uvalue",
-       "r2.svalue-r1.svalue<=0", "r2.svalue-r1.uvalue<=0",
-       "r2.uvalue-r1.svalue<=0", "r2.uvalue-r1.uvalue<=0"]
+post: ["r1.type=number", "r1.svalue=[0, 9223372036854775807]", "r1.svalue=r1.uvalue",
+       "r2.type=number", "r2.svalue=[0, 9223372036854775807]", "r2.svalue=r2.uvalue"]
 ---
 test-case: "assume [0, INT32_MAX] w>= [0, INT32_MAX] implies relation"
 pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]", "r1.svalue=r1.uvalue",
@@ -945,10 +935,8 @@ pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]"
 code:
   <start>: |
     assume w1 >= r2
-post: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]", "r1.svalue=r1.uvalue",
-       "r2.type=number", "r2.svalue=[0, 2147483647]", "r2.uvalue=[0, 2147483647]", "r2.svalue=r2.uvalue",
-       "r2.svalue-r1.svalue<=0", "r2.svalue-r1.uvalue<=0",
-       "r2.uvalue-r1.svalue<=0", "r2.uvalue-r1.uvalue<=0"]
+post: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.svalue=r1.uvalue",
+       "r2.type=number", "r2.svalue=[0, 2147483647]", "r2.svalue=r2.uvalue"]
 ---
 test-case: "assume [INT_MIN, -1] >= [INT_MIN, -1] implies relation"
 pre: ["r1.type=number", "r1.svalue=[-9223372036854775807, -1]", "r1.uvalue=[9223372036854775809, 18446744073709551615]",
@@ -957,9 +945,7 @@ code:
   <start>: |
     assume r1 >= r2
 post: ["r1.type=number", "r1.svalue=[-9223372036854775807, -1]", "r1.uvalue=[9223372036854775809, 18446744073709551615]",
-       "r2.type=number", "r2.svalue=[-9223372036854775807, -1]", "r2.uvalue=[9223372036854775809, 18446744073709551615]",
-       "r2.svalue-r1.svalue<=0",
-       "r2.uvalue-r1.uvalue<=0"]
+       "r2.type=number", "r2.svalue=[-9223372036854775807, -1]", "r2.uvalue=[9223372036854775809, 18446744073709551615]"]
 ---
 test-case: "assume [INT32_MIN, -1] w>= [INT32_MIN, -1] implies relation"
 pre: ["r1.type=number", "r1.svalue=[-2147483648, -1]", "r1.uvalue=[18446744071562067968, 18446744073709551615]",
@@ -968,9 +954,7 @@ code:
   <start>: |
     assume w1 >= r2
 post: ["r1.type=number", "r1.svalue=[-2147483648, -1]", "r1.uvalue=[18446744071562067968, 18446744073709551615]",
-       "r2.type=number", "r2.svalue=[-2147483648, -1]", "r2.uvalue=[18446744071562067968, 18446744073709551615]",
-       "r2.svalue-r1.svalue<=0",
-       "r2.uvalue-r1.uvalue<=0"]
+       "r2.type=number", "r2.svalue=[-2147483648, -1]", "r2.uvalue=[18446744071562067968, 18446744073709551615]"]
 ---
 test-case: "assume [0, INT_MAX] < [0, INT_MAX] implies narrowing and relation"
 pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775807]", "r1.uvalue=[0, 9223372036854775807]", "r1.svalue=r1.uvalue",
@@ -978,10 +962,9 @@ pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775807]", "r1.uvalue=[0, 922
 code:
   <start>: |
     assume r1 < r2
-post: ["r1.type=number", "r1.svalue=[0, 9223372036854775806]", "r1.uvalue=[0, 9223372036854775806]", "r1.svalue=r1.uvalue",
-       "r2.type=number", "r2.svalue=[1, 9223372036854775807]", "r2.uvalue=[1, 9223372036854775807]", "r2.svalue=r2.uvalue",
-       "r1.svalue-r2.svalue<=-1", "r1.svalue-r2.uvalue<=-1",
-       "r1.uvalue-r2.svalue<=-1", "r1.uvalue-r2.uvalue<=-1"]
+post: ["r1.type=number", "r1.svalue=[0, 9223372036854775806]", "r1.svalue=r1.uvalue",
+       "r2.type=number", "r2.svalue=[1, 9223372036854775807]", "r2.svalue=r2.uvalue",
+       "r1.svalue-r2.svalue<=-1"]
 ---
 test-case: "assume [0, INT32_MAX] w< [0, INT32_MAX] implies narrowing and relation"
 pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]", "r1.svalue=r1.uvalue",
@@ -989,10 +972,9 @@ pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]"
 code:
   <start>: |
     assume w1 < r2
-post: ["r1.type=number", "r1.svalue=[0, 2147483646]", "r1.uvalue=[0, 2147483646]", "r1.svalue=r1.uvalue",
-       "r2.type=number", "r2.svalue=[1, 2147483647]", "r2.uvalue=[1, 2147483647]", "r2.svalue=r2.uvalue",
-       "r1.svalue-r2.svalue<=-1", "r1.svalue-r2.uvalue<=-1",
-       "r1.uvalue-r2.svalue<=-1", "r1.uvalue-r2.uvalue<=-1"]
+post: ["r1.type=number", "r1.svalue=[0, 2147483646]", "r1.svalue=r1.uvalue",
+       "r2.type=number", "r2.svalue=[1, 2147483647]", "r2.svalue=r2.uvalue",
+       "r1.svalue-r2.svalue<=-1"]
 ---
 test-case: "assume [INT_MIN+1, -1] < [INT_MIN+1, -1] implies narrowing and relation"
 pre: ["r1.type=number", "r1.svalue=[-9223372036854775807, -1]", "r1.uvalue=[9223372036854775809, 18446744073709551615]",
@@ -1002,8 +984,7 @@ code:
     assume r1 < r2
 post: ["r1.type=number", "r1.svalue=[-9223372036854775807, -2]", "r1.uvalue=[9223372036854775809, 18446744073709551614]",
        "r2.type=number", "r2.svalue=[-9223372036854775806, -1]", "r2.uvalue=[9223372036854775810, 18446744073709551615]",
-       "r1.svalue-r2.svalue<=-1",
-       "r1.uvalue-r2.uvalue<=-1"]
+       "r1.svalue-r2.svalue<=-1", "r1.uvalue-r2.uvalue<=-1"]
 ---
 test-case: "assume [INT32_MIN, -1] w< [INT_MIN32, -1] implies narrowing and relation"
 pre: ["r1.type=number", "r1.svalue=[-2147483648, -1]", "r1.uvalue=[18446744071562067968, 18446744073709551615]",
@@ -1013,8 +994,7 @@ code:
     assume w1 < r2
 post: ["r1.type=number", "r1.svalue=[-2147483648, -2]", "r1.uvalue=[18446744071562067968, 18446744073709551614]",
        "r2.type=number", "r2.svalue=[-2147483647, -1]", "r2.uvalue=[18446744071562067969, 18446744073709551615]",
-       "r1.svalue-r2.svalue<=-1",
-       "r1.uvalue-r2.uvalue<=-1"]
+       "r1.svalue-r2.svalue<=-1", "r1.uvalue-r2.uvalue<=-1"]
 ---
 test-case: "assume [0, INT_MAX] > [0, INT_MAX] implies narrowing and relation"
 pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775807]", "r1.uvalue=[0, 9223372036854775807]", "r1.svalue=r1.uvalue",
@@ -1022,10 +1002,9 @@ pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775807]", "r1.uvalue=[0, 922
 code:
   <start>: |
     assume r1 > r2
-post: ["r1.type=number", "r1.svalue=[1, 9223372036854775807]", "r1.uvalue=[1, 9223372036854775807]", "r1.svalue=r1.uvalue",
-       "r2.type=number", "r2.svalue=[0, 9223372036854775806]", "r2.uvalue=[0, 9223372036854775806]", "r2.svalue=r2.uvalue",
-       "r2.svalue-r1.svalue<=-1", "r2.svalue-r1.uvalue<=-1",
-       "r2.uvalue-r1.svalue<=-1", "r2.uvalue-r1.uvalue<=-1"]
+post: ["r1.type=number", "r1.svalue=[1, 9223372036854775807]", "r1.svalue=r1.uvalue",
+       "r2.type=number", "r2.svalue=[0, 9223372036854775806]", "r2.svalue=r2.uvalue",
+       "r2.svalue-r1.svalue<=-1"]
 ---
 test-case: "assume [0, INT32_MAX] w> [0, INT32_MAX] implies narrowing and relation"
 pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]", "r1.svalue=r1.uvalue",
@@ -1033,10 +1012,9 @@ pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]"
 code:
   <start>: |
     assume w1 > r2
-post: ["r1.type=number", "r1.svalue=[1, 2147483647]", "r1.uvalue=[1, 2147483647]", "r1.svalue=r1.uvalue",
-       "r2.type=number", "r2.svalue=[0, 2147483646]", "r2.uvalue=[0, 2147483646]", "r2.svalue=r2.uvalue",
-       "r2.svalue-r1.svalue<=-1", "r2.svalue-r1.uvalue<=-1",
-       "r2.uvalue-r1.svalue<=-1", "r2.uvalue-r1.uvalue<=-1"]
+post: ["r1.type=number", "r1.svalue=[1, 2147483647]", "r1.svalue=r1.uvalue",
+       "r2.type=number", "r2.svalue=[0, 2147483646]", "r2.svalue=r2.uvalue",
+       "r2.svalue-r1.svalue<=-1"]
 ---
 test-case: "assume [INT_MIN+1, -1] > [INT_MIN+1, -1] implies narrowing and relation"
 pre: ["r1.type=number", "r1.svalue=[-9223372036854775807, -1]", "r1.uvalue=[9223372036854775809, 18446744073709551615]",
@@ -1046,8 +1024,7 @@ code:
     assume r1 > r2
 post: ["r1.type=number", "r1.svalue=[-9223372036854775806, -1]", "r1.uvalue=[9223372036854775810, 18446744073709551615]",
        "r2.type=number", "r2.svalue=[-9223372036854775807, -2]", "r2.uvalue=[9223372036854775809, 18446744073709551614]",
-       "r2.svalue-r1.svalue<=-1",
-       "r2.uvalue-r1.uvalue<=-1"]
+       "r2.svalue-r1.svalue<=-1", "r2.uvalue-r1.uvalue<=-1"]
 ---
 test-case: "assume [INT32_MIN, -1] w> [INT32_MIN, -1] implies narrowing and relation"
 pre: ["r1.type=number", "r1.svalue=[-2147483648, -1]", "r1.uvalue=[18446744071562067968, 18446744073709551615]",
@@ -1057,8 +1034,7 @@ code:
     assume w1 > r2
 post: ["r1.type=number", "r1.svalue=[-2147483647, -1]", "r1.uvalue=[18446744071562067969, 18446744073709551615]",
        "r2.type=number", "r2.svalue=[-2147483648, -2]", "r2.uvalue=[18446744071562067968, 18446744073709551614]",
-       "r2.svalue-r1.svalue<=-1",
-       "r2.uvalue-r1.uvalue<=-1"]
+       "r2.svalue-r1.svalue<=-1", "r2.uvalue-r1.uvalue<=-1"]
 ---
 test-case: "assume [-1, 1] <= [-1, 1] nop"
 pre: ["r1.type=number", "r1.svalue=[-1, 1]",
@@ -1066,9 +1042,8 @@ pre: ["r1.type=number", "r1.svalue=[-1, 1]",
 code:
   <start>: |
     assume r1 <= r2
-post: ["r1.type=number", "r1.svalue=[-1, 1]",
-       "r2.type=number", "r2.svalue=[-1, 1]",
-       "r1.uvalue-r2.uvalue<=0"]
+post: ["r1.type=number", "r1.svalue=[-1, 1]", "r1.uvalue=r2.uvalue",
+       "r2.type=number", "r2.svalue=[-1, 1]"]
 ---
 test-case: "assume [-1, 1] w<= [-1, 1] nop"
 pre: ["r1.type=number", "r1.svalue=[-1, 1]",
@@ -1136,10 +1111,8 @@ post:
   - r1.type=number
   - r1.uvalue=[1, 4]
   - r1.uvalue-r2.svalue<=-1
-  - r1.uvalue-r2.uvalue<=-1
   - r2.type=number
   - r2.svalue=[2, 2147483652]
-  - r2.uvalue=[2, 2147483652]
   - r2.svalue=r2.uvalue
 ---
 test-case: signed 64-bit negative LT
@@ -1152,7 +1125,7 @@ test-case: signed 64-bit positive LT
 pre: ["r1.type=number", "r1.svalue=[1, 3]", "r1.uvalue=[1, 3]", "r1.svalue=r1.uvalue"]
 code:
   <start>: assume r1 s< 2
-post: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=1", "r1.svalue=r1.uvalue"]
 ---
 test-case: signed 64-bit LT
 pre: ["r1.type=number", "r1.svalue=[-1, 1]"]
@@ -1164,7 +1137,7 @@ test-case: signed 64-bit GT
 pre: ["r1.type=number", "r1.svalue=[-1, 2]"]
 code:
   <start>: assume r1 s> 0
-post: ["r1.type=number", "r1.svalue=[1, 2]", "r1.uvalue=[1, 2]", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=[1, 2]", "r1.svalue=r1.uvalue"]
 ---
 test-case: signed 32-bit negative LT
 pre: ["r1.type=number", "r1.svalue=[-3, -1]", "r1.uvalue=[18446744073709551613, 18446744073709551615]"]
@@ -1176,7 +1149,7 @@ test-case: signed 32-bit positive LT
 pre: ["r1.type=number", "r1.svalue=[1, 3]", "r1.uvalue=[1, 3]", "r1.svalue=r1.uvalue"]
 code:
   <start>: assume w1 s< 2
-post: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=1", "r1.svalue=r1.uvalue"]
 ---
 test-case: signed 32-bit LT
 pre: ["r1.type=number", "r1.svalue=[-1, 1]"]
@@ -1194,13 +1167,13 @@ test-case: signed 32-bit positive GT
 pre: ["r1.type=number", "r1.svalue=[1, 4]", "r1.uvalue=[1, 4]", "r1.svalue=r1.uvalue"]
 code:
   <start>: assume w1 s> 2
-post: ["r1.type=number", "r1.svalue=[3, 4]", "r1.uvalue=[3, 4]", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=[3, 4]", "r1.svalue=r1.uvalue"]
 ---
 test-case: signed 32-bit GT
 pre: ["r1.type=number", "r1.svalue=[-1, 2]"]
 code:
   <start>: assume w1 s> 0
-post: ["r1.type=number", "r1.svalue=[1, 2]", "r1.uvalue=[1, 2]", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=[1, 2]", "r1.svalue=r1.uvalue"]
 ---
 test-case: "assume TOP s> 0 narrows to [1, INT64_MAX]"
 pre: ["r1.type=number"]
@@ -1209,7 +1182,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[1, 9223372036854775807]
-  - r1.uvalue=[1, 9223372036854775807]
   - r1.svalue=r1.uvalue
 ---
 test-case: "assume [-2, 2] s> -2"
@@ -1222,13 +1194,13 @@ test-case: "assume [0, 3] s> 1"
 pre: ["r1.type=number", "r1.svalue=[0, 3]", "r1.uvalue=[0, 3]", "r1.svalue=r1.uvalue"]
 code:
   <start>: assume r1 s> 1
-post: ["r1.type=number", "r1.svalue=[2, 3]", "r1.uvalue=[2, 3]", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=[2, 3]", "r1.svalue=r1.uvalue"]
 ---
 test-case: "assume [0, 3] s> 1"
 pre: ["r1.type=number", "r1.svalue=[0, 3]", "r1.uvalue=[0, 3]", "r1.svalue=r1.uvalue"]
 code:
   <start>: assume r1 s> 1
-post: ["r1.type=number", "r1.svalue=[2, 3]", "r1.uvalue=[2, 3]", "r1.svalue=r1.uvalue"]
+post: ["r1.type=number", "r1.svalue=[2, 3]", "r1.svalue=r1.uvalue"]
 ---
 test-case: "assume [-4, -1] s> -3"
 pre: ["r1.type=number", "r1.svalue=[-4, -1]", "r1.uvalue=[18446744073709551612, 18446744073709551615]"]