diff --git a/src/crab/split_dbm.cpp b/src/crab/split_dbm.cpp
index 1005a1272..db0d52e0c 100644
--- a/src/crab/split_dbm.cpp
+++ b/src/crab/split_dbm.cpp
@@ -1130,14 +1130,57 @@ 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::set<std::string> result;
-    // Intervals
+    for (const auto [vs, least] : equivalence_classes) {
+        if (vs == least) {
+            representatives.insert(least);
+        } else {
+            result.insert(vs.name() + "=" + least.name());
+        }
+    }
 
-    // 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 +1190,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 +1207,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 +1216,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..8918a435d 100644
--- a/test-data/add.yaml
+++ b/test-data/add.yaml
@@ -25,8 +25,7 @@ code:
 post:
   - r0.type=number
   - r0.svalue=[2147483649, 2147483651]
-  - r0.uvalue=[2147483649, 2147483651]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
 ---
 test-case: add immediate to unknown number
 
@@ -90,8 +89,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[10, 15]
-  - r1.uvalue=[10, 15]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 
 ---
 test-case: add constant register number to finite interval number
@@ -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.uvalue=r1.svalue
   - 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,20 +125,12 @@ post:
   - r2.type=packet
   - r2.packet_offset=[3, 5]
   - r2.svalue=[10, 16]
-  - r2.uvalue=[10, 16]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
   - 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
+  - r7.svalue=r2.packet_offset
 
 ---
 test-case: add constant register pointer to interval number
@@ -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
+  - r7.uvalue=r7.svalue
   - 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..a4498c02e 100644
--- a/test-data/assign.yaml
+++ b/test-data/assign.yaml
@@ -23,9 +23,9 @@ code:
     r1 = r2;
 
 post:
-  - r1.type=r2.type
-  - r1.svalue=r2.svalue
-  - r1.uvalue=r2.uvalue
+  - r2.type=r1.type
+  - r2.svalue=r1.svalue
+  - r2.uvalue=r1.uvalue
 
 ---
 test-case: re-assign immediate
@@ -98,8 +98,8 @@ code:
 post:
   - r1.type=packet
   - r1.packet_offset=0
-  - r1.svalue=s[504...511].svalue
-  - r1.uvalue=s[504...511].uvalue
+  - s[504...511].svalue=r1.svalue
+  - s[504...511].uvalue=r1.uvalue
   - r10.type=stack
   - r10.stack_offset=512
   - s[504...511].type=packet
@@ -131,8 +131,8 @@ code:
 post:
   - r1.type=packet
   - r1.packet_offset=0
-  - r1.svalue=s[504...511].svalue
-  - r1.uvalue=s[504...511].uvalue
+  - s[504...511].svalue=r1.svalue
+  - s[504...511].uvalue=r1.uvalue
   - r10.type=stack
   - r10.stack_offset=512
   - s[500...503].type=number
@@ -168,9 +168,9 @@ post:
   - r1.stack_offset=0
   - r2.type=stack
   - r2.stack_offset=0
-  - r1.svalue=r2.svalue
-  - r1.uvalue=r2.uvalue
-  - r1.stack_numeric_size=r2.stack_numeric_size
+  - r2.svalue=r1.svalue
+  - r2.uvalue=r1.uvalue
+  - r2.stack_numeric_size=r1.stack_numeric_size
 ---
 test-case: 32-bit assign register stack value
 
@@ -182,8 +182,7 @@ code:
 
 post:
   - r2.svalue=[0, 4294967295]
-  - r2.svalue=r2.uvalue
-  - r2.uvalue=[0, 4294967295]
+  - r2.uvalue=r2.svalue
   - r10.type=stack
   - r10.stack_offset=512
 
@@ -205,8 +204,8 @@ post:
   - r2.type=shared
   - r2.shared_offset=0
   - r2.shared_region_size=16
-  - r1.svalue=r2.svalue
-  - r1.uvalue=r2.uvalue
+  - r2.svalue=r1.svalue
+  - r2.uvalue=r1.uvalue
 ---
 test-case: 32-bit assign register shared value
 
@@ -221,8 +220,7 @@ post:
   - r1.shared_offset=0
   - r1.shared_region_size=16
   - r2.svalue=[0, 4294967295]
-  - r2.uvalue=[0, 4294967295]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -241,14 +239,13 @@ 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
   - r2.stack_numeric_size=16
-  - r1.type=r2.type
-  - r1.svalue=r2.svalue
-  - r1.uvalue=r2.uvalue
+  - r2.type=r1.type
+  - r2.svalue=r1.svalue
+  - r2.uvalue=r1.uvalue
 ---
 test-case: 32-bit indirect assignment from context
 
@@ -259,7 +256,7 @@ code:
     r2 = *(u32 *)(r1 + 4)
 
 post:
-  - packet_size=r2.packet_offset
+  - r2.packet_offset=packet_size
   - r1.ctx_offset=0
   - r1.type=ctx
   - r1.svalue=[1, 2147418112]
@@ -297,26 +294,24 @@ post:
 ---
 test-case: assign register packet value
 
-pre: ["packet_size=r2.packet_offset", "r2.type=packet", "r2.svalue=[4098, 2147418112]"]
+pre: ["r2.packet_offset=packet_size", "r2.type=packet", "r2.svalue=[4098, 2147418112]"]
 
 code:
   <start>: |
     r1 = r2
 
 post:
-  - packet_size=r1.packet_offset
+  - r1.packet_offset=packet_size
+  - r2.packet_offset=packet_size
+  - r2.svalue=r1.svalue
+  - r2.uvalue=r1.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
 
-pre: ["packet_size=r2.packet_offset", "r2.type=packet", "r2.svalue=[4098, 2147418112]"]
+pre: ["r2.packet_offset=packet_size", "r2.type=packet", "r2.svalue=[4098, 2147418112]"]
 
 code:
   <start>: |
@@ -324,9 +319,8 @@ code:
 
 post:
   - r1.svalue=[0, 4294967295]
-  - r1.uvalue=[0, 4294967295]
-  - r1.svalue=r1.uvalue
-  - packet_size=r2.packet_offset
+  - r1.uvalue=r1.svalue
+  - r2.packet_offset=packet_size
   - r2.type=packet
   - r2.svalue=[4098, 2147418112]
 
@@ -348,10 +342,8 @@ 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
+  - r2.svalue=r1.svalue
+  - r2.uvalue=r1.uvalue
 ---
 test-case: 32-bit assign register context value
 
@@ -367,8 +359,7 @@ post:
   - r1.svalue=[1, 2147418112]
   - r1.uvalue=[1, 2147418112]
   - r2.svalue=[1, 2147418112]
-  - r2.uvalue=[1, 2147418112]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -386,8 +377,8 @@ post:
   - r1.type=map_fd
   - r2.map_fd=1
   - r2.type=map_fd
-  - r1.svalue=r2.svalue
-  - r1.uvalue=r2.uvalue
+  - r2.svalue=r1.svalue
+  - r2.uvalue=r1.uvalue
 ---
 test-case: 32-bit assign register map value
 
@@ -401,8 +392,7 @@ post:
   - r1.map_fd=1
   - r1.type=map_fd
   - r2.svalue=[0, 4294967295]
-  - r2.uvalue=[0, 4294967295]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -420,8 +410,8 @@ post:
   - r1.type=map_fd_programs
   - r2.map_fd=1
   - r2.type=map_fd_programs
-  - r1.svalue=r2.svalue
-  - r1.uvalue=r2.uvalue
+  - r2.svalue=r1.svalue
+  - r2.uvalue=r1.uvalue
 ---
 test-case: 32-bit assign register map programs value
 
@@ -435,8 +425,7 @@ post:
   - r1.map_fd=1
   - r1.type=map_fd_programs
   - r2.svalue=[0, 4294967295]
-  - r2.uvalue=[0, 4294967295]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 
 messages:
   - "0: Invalid type (r1.type == number)"
diff --git a/test-data/atomic.yaml b/test-data/atomic.yaml
index c5f615d66..25f34c635 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 ---
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue",
       "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.uvalue=r2.svalue",
        "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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 
 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.uvalue=r2.svalue"]
 
 messages:
   - "0: Invalid type (r1.type == number)"
diff --git a/test-data/call.yaml b/test-data/call.yaml
index f75b4ecb9..6debd6db8 100644
--- a/test-data/call.yaml
+++ b/test-data/call.yaml
@@ -16,8 +16,7 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
   - s[504...511].type=number
 ---
 test-case: bpf_map_lookup_elem shared key
@@ -34,8 +33,7 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
 ---
 test-case: bpf_map_lookup_elem packet key
 
@@ -52,8 +50,7 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
   - meta_offset=0
   - packet_size=4
 ---
@@ -71,8 +68,7 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
 
 messages:
   - "0: Possible null access (within stack(r2:key_size(r1)))"
@@ -92,8 +88,7 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
 
 messages:
   - "0: Upper bound must be at most r2.shared_region_size (within stack(r2:key_size(r1)))"
@@ -112,8 +107,7 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
 
 messages:
   - "0: Lower bound must be at least 0 (within stack(r2:key_size(r1)))"
@@ -132,8 +126,7 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
 
 messages:
   - "0: Illegal map update with a non-numerical value [-oo-oo) (within stack(r2:key_size(r1)))"
diff --git a/test-data/callx.yaml b/test-data/callx.yaml
index 2af9e0a8e..b71b82e60 100644
--- a/test-data/callx.yaml
+++ b/test-data/callx.yaml
@@ -17,8 +17,7 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
   - r8.type=number
   - r8.svalue=1
   - r8.uvalue=1
@@ -39,8 +38,7 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
   - r8.type=number
   - r8.svalue=1
   - r8.uvalue=1
@@ -61,8 +59,7 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
   - meta_offset=0
   - packet_size=4
   - r8.type=number
@@ -84,8 +81,7 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
   - r8.type=number
   - r8.svalue=1
   - r8.uvalue=1
@@ -108,8 +104,7 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
   - r8.type=number
   - r8.svalue=1
   - r8.uvalue=1
@@ -132,8 +127,7 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
   - r8.type=number
   - r8.svalue=1
   - r8.uvalue=1
@@ -204,8 +198,7 @@ post:
   - r0.shared_offset=0
   - r0.shared_region_size=4
   - r0.svalue=[0, 2147418112]
-  - r0.uvalue=[0, 2147418112]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
   - r8.type=number
   - r8.svalue=1
   - r8.uvalue=1
diff --git a/test-data/full64.yaml b/test-data/full64.yaml
index b004151d9..08a9a0b33 100644
--- a/test-data/full64.yaml
+++ b/test-data/full64.yaml
@@ -97,8 +97,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=9223372036854775807
-  - r1.uvalue=9223372036854775807
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: not equal 0
 
@@ -114,7 +113,7 @@ post:
 ---
 test-case: equals 0
 
-pre: ["r0.type=number", "r0.svalue=[0, 1]", "r0.uvalue=[0, 1]", "r0.svalue=r0.uvalue"]
+pre: ["r0.type=number", "r0.svalue=[0, 1]", "r0.uvalue=[0, 1]", "r0.uvalue=r0.svalue"]
 
 code:
   <start>: |
@@ -123,8 +122,7 @@ code:
 post:
   - r0.type=number
   - r0.svalue=0
-  - r0.uvalue=0
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
 ---
 test-case: create unsigned infinite interval
 
@@ -149,8 +147,7 @@ code:
 post:
   - r0.type=number
   - r0.svalue=[1, 9223372036854775807]
-  - r0.uvalue=[1, 9223372036854775807]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
 ---
 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
@@ -197,22 +194,16 @@ post:
 test-case: equals positive interval
 
 pre: ["r1.type=number", "r1.svalue=[-1, 2]",
-      "r2.type=number", "r2.svalue=[1, 3]", "r2.uvalue=[1, 3]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[1, 3]", "r2.uvalue=[1, 3]", "r2.uvalue=r2.svalue"]
 
 code:
   <start>: |
-     assume r1 == r2
+    assume r1 == r2
 
 post:
+  - r1.uvalue=r1.svalue
+  - r2.svalue=r1.svalue
+  - r2.uvalue=r1.svalue
   - 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..cca7e43b6 100644
--- a/test-data/jump.yaml
+++ b/test-data/jump.yaml
@@ -34,12 +34,9 @@ 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.uvalue=r0.svalue
+  - r1.uvalue=r0.svalue
   - r1.type=number
-  - r1.uvalue=[0, +oo]
 ---
 test-case: simple unconditional jump forward
 
@@ -302,9 +299,8 @@ post:
   - r0.uvalue=[0, +oo]
   - r1.ctx_offset=4
   - r1.type in {number, ctx}
-  - r1.type=r2.type
+  - r2.type=r1.type
   - r2.ctx_offset=0
-  - r2.type in {number, ctx}
   - r3.type=number
   - r8.ctx_offset=4
   - r8.type=ctx
@@ -413,88 +409,35 @@ code:
     r3 += r2; the domain does not currently store inequalities so we can't yet tell that this is safe
 
 post:
+  - r1.uvalue=r1.svalue
+  - r2.uvalue=r2.svalue
+  - r3.type=r1.type
+  - r3.uvalue=r3.svalue
+  - r3.ctx_offset=r2.ctx_offset
   - 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
@@ -539,10 +482,9 @@ post:
   - r1.stack_offset=4
   - r1.packet_offset=4
   - r1.type in {packet, stack}
-  - r1.type=r2.type
+  - r2.type=r1.type
   - r2.stack_offset=0
   - r2.packet_offset=0
-  - r2.type in {packet, stack}
   - r6.type=stack
   - r6.stack_offset=4
   - r7.type=stack
@@ -581,20 +523,16 @@ code:
 post:
   - meta_offset=0
   - packet_size=[36, 65534]
-  - packet_size=r2.packet_offset
+  - r2.packet_offset=packet_size
   - packet_size-r1.packet_offset<=65480
   - r0.type=number
   - 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
+  - r4.uvalue=r4.svalue
 
 messages:
   - "7: Upper bound must be at most packet_size (valid_access(r1.offset-8, width=8) for read)"
diff --git a/test-data/loop.yaml b/test-data/loop.yaml
index 2aa159e81..a336353f1 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"
+  - "r0.uvalue=r0.svalue"
   - "pc[1]=5"
   - "pc[1]=r0.svalue+1"
-  - "pc[1]=r0.uvalue+1"
 ---
 test-case: until loop, unsigned leq
 options: ["termination"]
@@ -38,13 +36,10 @@ 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"
+  - r0.uvalue=pc[1]
+  - r0.svalue=pc[1]
+  - r0.type=number
+  - pc[1]=4
 ---
 test-case: while loop, signed gte
 options: ["termination"]
@@ -61,13 +56,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.uvalue=r0.svalue
+  - pc[1]=5
+  - pc[1]=r0.svalue+1
 ---
 test-case: until loop, signed leq
 options: ["termination"]
@@ -84,13 +77,10 @@ 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"
+  - r0.uvalue=pc[1]
+  - r0.svalue=pc[1]
+  - r0.type=number
+  - pc[1]=4
 ---
 test-case: loop with data dependence, unsigned leq
 options: ["termination"]
@@ -109,16 +99,13 @@ 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"
+  - r0.uvalue=pc[1]
+  - r0.svalue=pc[1]
+  - r0.type=number
+  - r1.type=number
+  - r2.type=number
+  - r3.type=number
+  - pc[1]=[1, 4]
 ---
 test-case: while loop, eq
 # options: ["termination"]
@@ -138,7 +125,7 @@ post:
   - "r0.type=number"
   - "r0.svalue=4"
   - "r0.uvalue=4"
-#  - "r0.svalue=r0.uvalue"
+#  - "r0.uvalue=r0.svalue"
 #  - "pc[1]=4"
 #  - "pc[1]=r0.value"
 ---
@@ -160,7 +147,7 @@ post:
   - "r0.type=number"
   - "r0.svalue=9"
   - "r0.uvalue=9"
-#  - "r0.svalue=r0.uvalue"
+#  - "r0.uvalue=r0.svalue"
 #  - "pc[1]=9"
 #  - "pc[1]=r0.value"
 ---
@@ -182,7 +169,7 @@ post:
   - "r0.type=number"
   - "r0.svalue=9"
   - "r0.uvalue=9"
-  # - "r0.svalue=r0.uvalue"
+  # - "r0.uvalue=r0.svalue"
   - "pc[1]=[1, +oo]"
 
 messages:
@@ -222,50 +209,22 @@ code:
     exit
 
 post:
+  - r2.uvalue=packet_size
+  - r2.svalue=packet_size
+  - r3.uvalue=pc[7]
+  - r3.svalue=pc[7]
+  - r4.svalue=pc[7]
+  - r4.uvalue=pc[7]
   - 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 +345,10 @@ 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
+  - r0.uvalue=pc[0]
+  - r0.svalue=pc[0]
+  - r0.type=number
 messages:
   - "0 (counter): Loop counter is too large (pc[0] < 100000)"
 
@@ -407,10 +363,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 +389,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..18189aca7 100644
--- a/test-data/movsx.yaml
+++ b/test-data/movsx.yaml
@@ -3,7 +3,7 @@
 ---
 test-case: movsx8 register to 32 bits
 
-pre: ["r1.svalue=384", "r1.uvalue=384", "r1.type=number", "r1.svalue=r1.uvalue"]
+pre: ["r1.svalue=384", "r1.uvalue=384", "r1.type=number", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -12,15 +12,14 @@ code:
 post:
   - r1.type=number
   - r1.svalue=384
-  - r1.uvalue=384
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=4294967168
   - r2.uvalue=4294967168
 ---
 test-case: movsx16 register to 32 bits
 
-pre: ["r1.svalue=98304", "r1.uvalue=98304", "r1.type=number", "r1.svalue=r1.uvalue"]
+pre: ["r1.svalue=98304", "r1.uvalue=98304", "r1.type=number", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -29,15 +28,14 @@ code:
 post:
   - r1.type=number
   - r1.svalue=98304
-  - r1.uvalue=98304
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=4294934528
   - r2.uvalue=4294934528
 ---
 test-case: movsx8 register to 64 bits
 
-pre: ["r1.svalue=384", "r1.uvalue=384", "r1.type=number", "r1.svalue=r1.uvalue"]
+pre: ["r1.svalue=384", "r1.uvalue=384", "r1.type=number", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -46,15 +44,14 @@ code:
 post:
   - r1.type=number
   - r1.svalue=384
-  - r1.uvalue=384
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=-128
   - r2.uvalue=18446744073709551488
 ---
 test-case: movsx16 register to 64 bits
 
-pre: ["r1.svalue=98304", "r1.uvalue=98304", "r1.type=number", "r1.svalue=r1.uvalue"]
+pre: ["r1.svalue=98304", "r1.uvalue=98304", "r1.type=number", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -63,15 +60,14 @@ code:
 post:
   - r1.type=number
   - r1.svalue=98304
-  - r1.uvalue=98304
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=-32768
   - r2.uvalue=18446744073709518848
 ---
 test-case: movsx32 register to 64 bits
 
-pre: ["r1.svalue=2147483648", "r1.uvalue=2147483648", "r1.type=number", "r1.svalue=r1.uvalue"]
+pre: ["r1.svalue=2147483648", "r1.uvalue=2147483648", "r1.type=number", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -80,8 +76,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=2147483648
-  - r1.uvalue=2147483648
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=-2147483648
   - r2.uvalue=18446744071562067968
@@ -101,7 +96,7 @@ messages:
 ---
 test-case: movsx8 register range to 32 bits without wrap
 
-pre: ["r1.svalue=[128, 130]", "r1.uvalue=[128, 130]", "r1.type=number", "r1.svalue=r1.uvalue"]
+pre: ["r1.svalue=[128, 130]", "r1.uvalue=[128, 130]", "r1.type=number", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -110,16 +105,14 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[128, 130]
-  - r1.uvalue=[128, 130]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[4294967168, 4294967170]
-  - r2.uvalue=[4294967168, 4294967170]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 ---
 test-case: movsx8 register range to 32 bits with wrap
 
-pre: ["r1.svalue=[255, 257]", "r1.uvalue=[255, 257]", "r1.type=number", "r1.svalue=r1.uvalue"]
+pre: ["r1.svalue=[255, 257]", "r1.uvalue=[255, 257]", "r1.type=number", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -128,16 +121,14 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[255, 257]
-  - r1.uvalue=[255, 257]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[0, 4294967295]
-  - r2.uvalue=[0, 4294967295]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 ---
 test-case: movsx16 register range to 32 bits without wrap
 
-pre: ["r1.svalue=[32768, 32770]", "r1.uvalue=[32768, 32770]", "r1.type=number", "r1.svalue=r1.uvalue"]
+pre: ["r1.svalue=[32768, 32770]", "r1.uvalue=[32768, 32770]", "r1.type=number", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -146,16 +137,14 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[32768, 32770]
-  - r1.uvalue=[32768, 32770]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[4294934528, 4294934530]
-  - r2.uvalue=[4294934528, 4294934530]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 ---
 test-case: movsx16 register range to 32 bits with wrap
 
-pre: ["r1.svalue=[65535, 65537]", "r1.uvalue=[65535, 65537]", "r1.type=number", "r1.svalue=r1.uvalue"]
+pre: ["r1.svalue=[65535, 65537]", "r1.uvalue=[65535, 65537]", "r1.type=number", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -164,16 +153,14 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[65535, 65537]
-  - r1.uvalue=[65535, 65537]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[0, 4294967295]
-  - r2.uvalue=[0, 4294967295]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 ---
 test-case: movsx8 register range to 64 bits
 
-pre: ["r1.svalue=[255, 257]", "r1.uvalue=[255, 257]", "r1.type=number", "r1.svalue=r1.uvalue"]
+pre: ["r1.svalue=[255, 257]", "r1.uvalue=[255, 257]", "r1.type=number", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -182,14 +169,13 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[255, 257]
-  - r1.uvalue=[255, 257]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[-1, 1]
 ---
 test-case: movsx8 register full range to 64 bits
 
-pre: ["r1.svalue=[255, 511]", "r1.uvalue=[255, 511]", "r1.type=number", "r1.svalue=r1.uvalue"]
+pre: ["r1.svalue=[255, 511]", "r1.uvalue=[255, 511]", "r1.type=number", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -198,14 +184,13 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[255, 511]
-  - r1.uvalue=[255, 511]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[-128, 127]
 ---
 test-case: movsx16 register range to 64 bits
 
-pre: ["r1.svalue=[65535, 65537]", "r1.uvalue=[65535, 65537]", "r1.type=number", "r1.svalue=r1.uvalue"]
+pre: ["r1.svalue=[65535, 65537]", "r1.uvalue=[65535, 65537]", "r1.type=number", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -214,14 +199,13 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[65535, 65537]
-  - r1.uvalue=[65535, 65537]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[-1, 1]
 ---
 test-case: movsx16 register full range to 64 bits
 
-pre: ["r1.svalue=[65535, 131071]", "r1.uvalue=[65535, 131071]", "r1.type=number", "r1.svalue=r1.uvalue"]
+pre: ["r1.svalue=[65535, 131071]", "r1.uvalue=[65535, 131071]", "r1.type=number", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -230,14 +214,13 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[65535, 131071]
-  - r1.uvalue=[65535, 131071]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[-32768, 32767]
 ---
 test-case: movsx32 register range to 64 bits
 
-pre: ["r1.svalue=[4294967295, 4294967297]", "r1.uvalue=[4294967295, 4294967297]", "r1.type=number", "r1.svalue=r1.uvalue"]
+pre: ["r1.svalue=[4294967295, 4294967297]", "r1.uvalue=[4294967295, 4294967297]", "r1.type=number", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -246,14 +229,13 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[4294967295, 4294967297]
-  - r1.uvalue=[4294967295, 4294967297]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[-1, 1]
 ---
 test-case: movsx32 register full range to 64 bits
 
-pre: ["r1.svalue=[4294967295, 8589934591]", "r1.uvalue=[4294967295, 8589934591]", "r1.type=number", "r1.svalue=r1.uvalue"]
+pre: ["r1.svalue=[4294967295, 8589934591]", "r1.uvalue=[4294967295, 8589934591]", "r1.type=number", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -262,7 +244,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[4294967295, 8589934591]
-  - r1.uvalue=[4294967295, 8589934591]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[-2147483648, 2147483647]
diff --git a/test-data/packet.yaml b/test-data/packet.yaml
index fd7e46bee..edba7c901 100644
--- a/test-data/packet.yaml
+++ b/test-data/packet.yaml
@@ -34,7 +34,7 @@ test-case: simple invalid write
 
 pre: ["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", "packet_size=[0, 65534]"]
+      "r2.type=packet", "r2.packet_offset=[0, 65534]", "r2.packet_offset=packet_size", "packet_size=[0, 65534]"]
 
 code:
   <start>: |
@@ -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", "r2.packet_offset=packet_size",
        "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)"
@@ -53,7 +53,7 @@ test-case: simple invalid read
 
 pre: ["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", "packet_size=[0, 65534]"]
+      "r2.type=packet", "r2.packet_offset=[0, 65534]", "r2.packet_offset=packet_size", "packet_size=[0, 65534]"]
 
 code:
   <start>: |
@@ -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", "r2.packet_offset=packet_size",
        "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)"
@@ -71,7 +71,7 @@ test-case: writing 8 bytes when packet size is 4
 
 pre: ["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", "r2.packet_offset=[0, 65534]", "r2.packet_offset=packet_size"]
 
 code:
   <start>: |
@@ -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]",
-       "r3.svalue=r3.uvalue",
+       "r2.type=packet", "r2.packet_offset=packet_size",
+       "r3.type=packet", "r3.packet_offset=4", "r3.svalue=[4102, 2147418116]",
+       "r3.uvalue=r3.svalue",
        "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)"
 
@@ -99,7 +98,7 @@ test-case: simple valid access
 
 pre: ["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", "r2.packet_offset=[0, 65534]", "r2.packet_offset=packet_size"]
 
 code:
   <start>: |
@@ -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", "r2.packet_offset=packet_size",
+       "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.uvalue=r3.svalue"]
 ---
 test-case: legacy 1 byte packet access imm
 
diff --git a/test-data/pointer.yaml b/test-data/pointer.yaml
index c7ac78cd1..7aab3c1ce 100644
--- a/test-data/pointer.yaml
+++ b/test-data/pointer.yaml
@@ -6,7 +6,7 @@ test-case: 32-bit pointer truncation - addition
 pre:
   - "r1.ctx_offset=0"
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
+  - "r1.uvalue=r1.svalue"
   - "r1.type=ctx"
   - "r1.uvalue=[0, 4294967295]"
 
@@ -28,7 +28,7 @@ test-case: 32-bit pointer truncation - subtraction
 pre:
   - "r1.ctx_offset=0"
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
+  - "r1.uvalue=r1.svalue"
   - "r1.type=ctx"
   - "r1.uvalue=[0, 4294967295]"
 
@@ -50,7 +50,7 @@ test-case: 32-bit pointer truncation - multiplication
 pre:
   - "r1.ctx_offset=0"
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
+  - "r1.uvalue=r1.svalue"
   - "r1.type=ctx"
   - "r1.uvalue=[0, 4294967295]"
 
@@ -62,8 +62,7 @@ code:
 
 post:
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
+  - "r1.uvalue=r1.svalue"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -76,7 +75,7 @@ test-case: 32-bit pointer truncation - division
 pre:
   - "r1.ctx_offset=0"
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
+  - "r1.uvalue=r1.svalue"
   - "r1.type=ctx"
   - "r1.uvalue=[0, 4294967295]"
 
@@ -88,8 +87,7 @@ code:
 
 post:
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
+  - "r1.uvalue=r1.svalue"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -102,7 +100,7 @@ test-case: 32-bit pointer truncation - modulo
 pre:
   - "r1.ctx_offset=0"
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
+  - "r1.uvalue=r1.svalue"
   - "r1.type=ctx"
   - "r1.uvalue=[0, 4294967295]"
 
@@ -114,8 +112,7 @@ code:
 
 post:
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
+  - "r1.uvalue=r1.svalue"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -128,9 +125,8 @@ test-case: 32-bit pointer truncation - signed division
 pre:
   - "r1.ctx_offset=0"
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
+  - "r1.uvalue=r1.svalue"
   - "r1.type=ctx"
-  - "r1.uvalue=[0, 4294967295]"
 
 # Trigger 32-bit ALU operation without changing the value
 code:
@@ -140,8 +136,7 @@ code:
 
 post:
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
+  - "r1.uvalue=r1.svalue"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -154,7 +149,7 @@ test-case: 32-bit pointer truncation - signed modulo
 pre:
   - "r1.ctx_offset=0"
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
+  - "r1.uvalue=r1.svalue"
   - "r1.type=ctx"
   - "r1.uvalue=[0, 4294967295]"
 
@@ -166,8 +161,7 @@ code:
 
 post:
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
+  - "r1.uvalue=r1.svalue"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -180,7 +174,7 @@ test-case: 32-bit pointer truncation - AND
 pre:
   - "r1.ctx_offset=0"
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
+  - "r1.uvalue=r1.svalue"
   - "r1.type=ctx"
   - "r1.uvalue=[0, 4294967295]"
 
@@ -192,8 +186,7 @@ code:
 
 post:
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
+  - "r1.uvalue=r1.svalue"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -206,7 +199,7 @@ test-case: 32-bit pointer truncation - OR
 pre:
   - "r1.ctx_offset=0"
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
+  - "r1.uvalue=r1.svalue"
   - "r1.type=ctx"
   - "r1.uvalue=[0, 4294967295]"
 
@@ -218,8 +211,7 @@ code:
 
 post:
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
+  - "r1.uvalue=r1.svalue"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -232,7 +224,7 @@ test-case: 32-bit pointer truncation - XOR
 pre:
   - "r1.ctx_offset=0"
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
+  - "r1.uvalue=r1.svalue"
   - "r1.type=ctx"
   - "r1.uvalue=[0, 4294967295]"
 
@@ -244,8 +236,7 @@ code:
 
 post:
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
+  - "r1.uvalue=r1.svalue"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -258,7 +249,7 @@ test-case: 32-bit pointer truncation - LSH
 pre:
   - "r1.ctx_offset=0"
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
+  - "r1.uvalue=r1.svalue"
   - "r1.type=ctx"
   - "r1.uvalue=[0, 4294967295]"
 
@@ -270,8 +261,7 @@ code:
 
 post:
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
+  - "r1.uvalue=r1.svalue"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -284,7 +274,7 @@ test-case: 32-bit pointer truncation - RSH
 pre:
   - "r1.ctx_offset=0"
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
+  - "r1.uvalue=r1.svalue"
   - "r1.type=ctx"
   - "r1.uvalue=[0, 4294967295]"
 
@@ -296,8 +286,7 @@ code:
 
 post:
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
+  - "r1.uvalue=r1.svalue"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -310,7 +299,7 @@ test-case: 32-bit pointer truncation - ARSH
 pre:
   - "r1.ctx_offset=0"
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
+  - "r1.uvalue=r1.svalue"
   - "r1.type=ctx"
   - "r1.uvalue=[0, 4294967295]"
 
@@ -322,8 +311,7 @@ code:
 
 post:
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
-  - "r1.uvalue=[0, 4294967295]"
+  - "r1.uvalue=r1.svalue"
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -336,7 +324,7 @@ test-case: 32-bit pointer truncation - NOT
 pre:
   - "r1.ctx_offset=0"
   - "r1.svalue=[0, 4294967295]"
-  - "r1.svalue=r1.uvalue"
+  - "r1.uvalue=r1.svalue"
   - "r1.type=ctx"
   - "r1.uvalue=[0, 4294967295]"
 
@@ -361,13 +349,13 @@ test-case: 64-bit return context pointer
 
 pre:
   - r0.uvalue=[0, 4294967295]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
   - 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.uvalue=r1.svalue
+  - r1.type=ctx
+  - r1.uvalue=[0, 4294967295]
 
 code:
   <start>: |
@@ -375,20 +363,14 @@ code:
     exit
 
 post:
+  - r0.uvalue=r0.svalue
+  - r1.uvalue=r0.svalue
+  - r1.svalue=r0.svalue
   - 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)"
@@ -399,13 +381,13 @@ test-case: 32-bit return context pointer
 
 pre:
   - r0.uvalue=0
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
   - 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.uvalue=r1.svalue
+  - r1.type=ctx
+  - r1.uvalue=1234567890
 
 code:
   <start>: |
@@ -414,9 +396,8 @@ code:
 post:
   - r1.ctx_offset=0
   - r1.svalue=1234567890
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - 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..556766d51 100644
--- a/test-data/sdivmod.yaml
+++ b/test-data/sdivmod.yaml
@@ -151,7 +151,7 @@ messages:
 test-case: non-zero divided by possibly zero register 2
 
 pre: ["r1.type=number", "r1.svalue=6", "r1.uvalue=6",
-      "r2.type=number", "r2.svalue=[0, 5]", "r2.uvalue=[0, 5]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[0, 5]", "r2.uvalue=[0, 5]", "r2.uvalue=r2.svalue"]
 
 options: ["!allow_division_by_zero"]
 
@@ -162,12 +162,10 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[0, 5]
-  - r2.uvalue=[0, 5]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 
 messages:
   - "0: Possible division by zero (r2 != 0)"
@@ -347,8 +345,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[-5, 5]
 
@@ -381,7 +378,7 @@ test-case: non-zero modulo possibly zero register 2
 options: ["!allow_division_by_zero"]
 
 pre: ["r1.type=number", "r1.svalue=6", "r1.uvalue=6",
-      "r2.type=number", "r2.svalue=[0, 5]", "r2.uvalue=[0, 5]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[0, 5]", "r2.uvalue=[0, 5]", "r2.uvalue=r2.svalue"]
 
 code:
   <start>: |
@@ -390,12 +387,10 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[0, 5]
-  - r2.uvalue=[0, 5]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 
 messages:
   - "0: Possible division by zero (r2 != 0)"
@@ -435,8 +430,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
 
 messages:
@@ -474,8 +468,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4]
-  - r1.uvalue=[0, 4]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[1, 5]
   - r2.uvalue=[1, 5]
@@ -518,8 +511,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 2]
-  - r1.uvalue=[0, 2]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[-3, -2]
   - r2.uvalue=[18446744073709551613, 18446744073709551614]
@@ -587,5 +579,4 @@ code:
 post:
   - r0.type=number
   - r0.svalue=[0, 2055]
-  - r0.uvalue=[0, 2055]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
diff --git a/test-data/sext.yaml b/test-data/sext.yaml
index 0846b4f0e..1089111d9 100644
--- a/test-data/sext.yaml
+++ b/test-data/sext.yaml
@@ -7,7 +7,7 @@ test-case: small zext relational nop
 
 pre: ["r1.type=number", "r1.uvalue=[0, 5]",
       "r2.type=number", "r2.uvalue=[0, 5]",
-      "r1.uvalue=r2.uvalue"]
+      "r2.uvalue=r1.uvalue"]
 
 code:
   <start>: |
@@ -17,14 +17,13 @@ post:
   - r1.type=number
   - r1.uvalue=[0, 5]
   - r2.type=number
-  - r2.uvalue=[0, 5]
-  - r1.uvalue=r2.uvalue
+  - r2.uvalue=r1.uvalue
 ---
 test-case: small sext relational nop
 
 pre: ["r1.type=number", "r1.svalue=[-5, 5]",
       "r2.type=number", "r2.svalue=[-5, 5]",
-      "r1.svalue=r2.svalue"]
+      "r2.svalue=r1.svalue"]
 
 code:
   <start>: |
@@ -34,14 +33,13 @@ post:
   - r1.type=number
   - r1.svalue=[-5, 5]
   - r2.type=number
-  - r2.svalue=[-5, 5]
-  - r1.svalue=r2.svalue
+  - r2.svalue=r1.svalue
 ---
 test-case: large zext relational is two shifts
 
 pre: ["r1.type=number", "r1.uvalue=[0, 4294967299]",
       "r2.type=number", "r2.uvalue=[0, 4294967299]",
-      "r1.uvalue=r2.uvalue"]
+      "r2.uvalue=r1.uvalue"]
 
 code:
   <start>: |
@@ -50,8 +48,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294967295]
-  - r1.svalue=r1.uvalue
-  - r1.uvalue=[0, 4294967295]
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.uvalue=[0, 4294967299]
 ---
@@ -59,7 +56,7 @@ test-case: large sext relational is two shifts
 
 pre: ["r1.type=number", "r1.svalue=[-5, 4294967299]",
       "r2.type=number", "r2.svalue=[-5, 4294967299]",
-      "r1.svalue=r2.svalue"]
+      "r2.svalue=r1.svalue"]
 
 code:
   <start>: |
diff --git a/test-data/shift.yaml b/test-data/shift.yaml
index 8d3b1c5f5..ec1a65aab 100644
--- a/test-data/shift.yaml
+++ b/test-data/shift.yaml
@@ -227,7 +227,7 @@ post:
 ---
 test-case: 64-bit unsigned right shift interval by imm
 
-pre: ["r1.type=number", "r1.svalue=[0, 4294967297]", "r1.uvalue=[0, 4294967297]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 4294967297]", "r1.uvalue=[0, 4294967297]", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -236,12 +236,11 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 65536]
-  - r1.uvalue=[0, 65536]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: 64-bit signed right shift interval by imm
 
-pre: ["r1.type=number", "r1.svalue=[0, 4294967297]", "r1.uvalue=[0, 4294967297]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 4294967297]", "r1.uvalue=[0, 4294967297]", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -250,12 +249,11 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 65536]
-  - r1.uvalue=[0, 65536]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: 64-bit unsigned right shift interval by reg
 
-pre: ["r1.type=number", "r1.svalue=[0, 4294967297]", "r1.uvalue=[0, 4294967297]", "r1.svalue=r1.uvalue",
+pre: ["r1.type=number", "r1.svalue=[0, 4294967297]", "r1.uvalue=[0, 4294967297]", "r1.uvalue=r1.svalue",
       "r2.type=number", "r2.svalue=16", "r2.uvalue=16"]
 
 code:
@@ -265,15 +263,14 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 65536]
-  - r1.uvalue=[0, 65536]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=16
   - r2.uvalue=16
 ---
 test-case: 64-bit signed right shift interval by reg
 
-pre: ["r1.type=number", "r1.svalue=[0, 4294967297]", "r1.uvalue=[0, 4294967297]", "r1.svalue=r1.uvalue",
+pre: ["r1.type=number", "r1.svalue=[0, 4294967297]", "r1.uvalue=[0, 4294967297]", "r1.uvalue=r1.svalue",
       "r2.type=number", "r2.svalue=16", "r2.uvalue=16"]
 
 code:
@@ -283,15 +280,14 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 65536]
-  - r1.uvalue=[0, 65536]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=16
   - r2.uvalue=16
 ---
 test-case: unsigned 32-bit right shift interval by imm
 
-pre: ["r1.type=number", "r1.svalue=[0, 65535]", "r1.uvalue=[0, 65535]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 65535]", "r1.uvalue=[0, 65535]", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -300,12 +296,11 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 255]
-  - r1.uvalue=[0, 255]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: signed 32-bit right shift interval by imm
 
-pre: ["r1.type=number", "r1.svalue=[0, 65535]", "r1.uvalue=[0, 65535]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 65535]", "r1.uvalue=[0, 65535]", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -314,12 +309,11 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 255]
-  - r1.uvalue=[0, 255]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: 32-bit unsigned right shift interval by reg
 
-pre: ["r1.type=number", "r1.svalue=[0, 65535]", "r1.uvalue=[0, 65535]", "r1.svalue=r1.uvalue",
+pre: ["r1.type=number", "r1.svalue=[0, 65535]", "r1.uvalue=[0, 65535]", "r1.uvalue=r1.svalue",
       "r2.type=number", "r2.svalue=8", "r2.uvalue=8"]
 
 code:
@@ -329,15 +323,14 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 255]
-  - r1.uvalue=[0, 255]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=8
   - r2.uvalue=8
 ---
 test-case: 32-bit signed right shift interval by reg
 
-pre: ["r1.type=number", "r1.svalue=[0, 65535]", "r1.uvalue=[0, 65535]", "r1.svalue=r1.uvalue",
+pre: ["r1.type=number", "r1.svalue=[0, 65535]", "r1.uvalue=[0, 65535]", "r1.uvalue=r1.svalue",
       "r2.type=number", "r2.svalue=8", "r2.uvalue=8"]
 
 code:
@@ -347,15 +340,14 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 255]
-  - r1.uvalue=[0, 255]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=8
   - r2.uvalue=8
 ---
 test-case: 32-bit unsigned right shift interval by imm with truncation
 
-pre: ["r1.type=number", "r1.svalue=[0, 4294967808]", "r1.uvalue=[0, 4294967808]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 4294967808]", "r1.uvalue=[0, 4294967808]", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -364,12 +356,11 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 255]
-  - r1.uvalue=[0, 255]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: 32-bit signed right shift interval by imm with truncation
 
-pre: ["r1.type=number", "r1.svalue=[0, 4294967808]", "r1.uvalue=[0, 4294967808]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 4294967808]", "r1.uvalue=[0, 4294967808]", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -378,12 +369,11 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294967295]
-  - r1.uvalue=[0, 4294967295]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: 32-bit unsigned right shift interval by reg with truncation
 
-pre: ["r1.type=number", "r1.svalue=[0, 4294967808]", "r1.uvalue=[0, 4294967808]", "r1.svalue=r1.uvalue",
+pre: ["r1.type=number", "r1.svalue=[0, 4294967808]", "r1.uvalue=[0, 4294967808]", "r1.uvalue=r1.svalue",
       "r2.type=number", "r2.svalue=24", "r2.uvalue=24"]
 
 code:
@@ -393,15 +383,14 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 255]
-  - r1.uvalue=[0, 255]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=24
   - r2.uvalue=24
 ---
 test-case: 32-bit signed right shift interval by reg with truncation
 
-pre: ["r1.type=number", "r1.svalue=[0, 4294967808]", "r1.uvalue=[0, 4294967808]", "r1.svalue=r1.uvalue",
+pre: ["r1.type=number", "r1.svalue=[0, 4294967808]", "r1.uvalue=[0, 4294967808]", "r1.uvalue=r1.svalue",
       "r2.type=number", "r2.svalue=24", "r2.uvalue=24"]
 
 code:
@@ -411,8 +400,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294967295]
-  - r1.uvalue=[0, 4294967295]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=24
   - r2.uvalue=24
@@ -428,8 +416,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[16776960, 16777215]
-  - r1.uvalue=[16776960, 16777215]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: 32-bit signed right shift interval by imm with negatives
 
@@ -442,8 +429,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[4294967040, 4294967295]
-  - r1.uvalue=[4294967040, 4294967295]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: 32-bit unsigned right shift interval by reg with negatives
 
@@ -457,8 +443,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[16776960, 16777215]
-  - r1.uvalue=[16776960, 16777215]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=8
   - r2.uvalue=8
@@ -475,8 +460,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[4294967040, 4294967295]
-  - r1.uvalue=[4294967040, 4294967295]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=8
   - r2.uvalue=8
@@ -492,8 +476,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 16777215]
-  - r1.uvalue=[0, 16777215]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: 32-bit signed right shift interval by imm crossing zero
 
@@ -506,8 +489,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294967295]
-  - r1.uvalue=[0, 4294967295]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: 32-bit unsigned right shift interval by reg crossing zero
 
@@ -521,8 +503,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 16777215]
-  - r1.uvalue=[0, 16777215]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=8
   - r2.uvalue=8
@@ -539,8 +520,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294967295]
-  - r1.uvalue=[0, 4294967295]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=8
   - r2.uvalue=8
@@ -659,7 +639,7 @@ post:
 ---
 test-case: 64-bit left shift interval by imm
 
-pre: ["r1.type=number", "r1.svalue=[1, 65536]", "r1.uvalue=[1, 65536]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[1, 65536]", "r1.uvalue=[1, 65536]", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -668,12 +648,11 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[65536, 4294967296]
-  - r1.uvalue=[65536, 4294967296]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: 64-bit left shift interval by reg
 
-pre: ["r1.type=number", "r1.svalue=[1, 65536]", "r1.uvalue=[1, 65536]", "r1.svalue=r1.uvalue",
+pre: ["r1.type=number", "r1.svalue=[1, 65536]", "r1.uvalue=[1, 65536]", "r1.uvalue=r1.svalue",
       "r2.type=number", "r2.svalue=16", "r2.uvalue=16"]
 
 code:
@@ -683,15 +662,14 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[65536, 4294967296]
-  - r1.uvalue=[65536, 4294967296]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=16
   - r2.uvalue=16
 ---
 test-case: 64-bit left shift interval by imm with wrap
 
-pre: ["r1.type=number", "r1.svalue=[0, 4294967296]", "r1.uvalue=[0, 4294967296]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 4294967296]", "r1.uvalue=[0, 4294967296]", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -703,7 +681,7 @@ post:
 ---
 test-case: 64-bit left shift interval by reg with wrap
 
-pre: ["r1.type=number", "r1.svalue=[0, 4294967296]", "r1.uvalue=[0, 4294967296]", "r1.svalue=r1.uvalue",
+pre: ["r1.type=number", "r1.svalue=[0, 4294967296]", "r1.uvalue=[0, 4294967296]", "r1.uvalue=r1.svalue",
       "r2.type=number", "r2.svalue=32", "r2.uvalue=32"]
 
 code:
@@ -728,8 +706,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[65536, 4294901760]
-  - r1.uvalue=[65536, 4294901760]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: 32-bit left shift interval by reg
 
@@ -743,15 +720,14 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[65536, 4294901760]
-  - r1.uvalue=[65536, 4294901760]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=16
   - r2.uvalue=16
 ---
 test-case: 32-bit left shift interval by imm with wrap
 
-pre: ["r1.type=number", "r1.svalue=[1, 65537]", "r1.uvalue=[1, 65537]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[1, 65537]", "r1.uvalue=[1, 65537]", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -760,12 +736,11 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: 32-bit left shift interval by reg with wrap
 
-pre: ["r1.type=number", "r1.svalue=[1, 65537]", "r1.uvalue=[1, 65537]", "r1.svalue=r1.uvalue",
+pre: ["r1.type=number", "r1.svalue=[1, 65537]", "r1.uvalue=[1, 65537]", "r1.uvalue=r1.svalue",
       "r2.type=number", "r2.svalue=16", "r2.uvalue=16"]
 
 code:
@@ -775,15 +750,14 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=16
   - r2.uvalue=16
 ---
 test-case: 32-bit left shift interval by imm with another wrap
 
-pre: ["r1.type=number", "r1.svalue=[2, 65537]", "r1.uvalue=[2, 65537]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[2, 65537]", "r1.uvalue=[2, 65537]", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -792,12 +766,11 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: 32-bit left shift interval by reg with another wrap
 
-pre: ["r1.type=number", "r1.svalue=[2, 65537]", "r1.uvalue=[2, 65537]", "r1.svalue=r1.uvalue",
+pre: ["r1.type=number", "r1.svalue=[2, 65537]", "r1.uvalue=[2, 65537]", "r1.uvalue=r1.svalue",
       "r2.type=number", "r2.svalue=16", "r2.uvalue=16"]
 
 code:
@@ -807,8 +780,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=16
   - r2.uvalue=16
@@ -850,8 +822,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: 32-bit left shift top by reg
 
@@ -865,15 +836,14 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=16
   - r2.uvalue=16
 ---
 test-case: 32-bit left shift interval by imm with longer wrap
 
-pre: ["r1.type=number", "r1.svalue=[1, 65538]", "r1.uvalue=[1, 65538]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[1, 65538]", "r1.uvalue=[1, 65538]", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -882,12 +852,11 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: 32-bit left shift interval by reg with longer wrap
 
-pre: ["r1.type=number", "r1.svalue=[1, 65538]", "r1.uvalue=[1, 65538]", "r1.svalue=r1.uvalue",
+pre: ["r1.type=number", "r1.svalue=[1, 65538]", "r1.uvalue=[1, 65538]", "r1.uvalue=r1.svalue",
       "r2.type=number", "r2.svalue=16", "r2.uvalue=16"]
 
 code:
@@ -897,15 +866,14 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=16
   - r2.uvalue=16
 ---
 test-case: 32-bit left shift interval by imm with another long wrap
 
-pre: ["r1.type=number", "r1.svalue=[1, 65539]", "r1.uvalue=[1, 65539]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[1, 65539]", "r1.uvalue=[1, 65539]", "r1.uvalue=r1.svalue"]
 
 code:
   <start>: |
@@ -914,12 +882,11 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: 32-bit left shift interval by reg with another long wrap
 
-pre: ["r1.type=number", "r1.svalue=[1, 65539]", "r1.uvalue=[1, 65539]", "r1.svalue=r1.uvalue",
+pre: ["r1.type=number", "r1.svalue=[1, 65539]", "r1.uvalue=[1, 65539]", "r1.uvalue=r1.svalue",
       "r2.type=number", "r2.svalue=16", "r2.uvalue=16"]
 
 code:
@@ -929,8 +896,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294901760]
-  - r1.uvalue=[0, 4294901760]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=16
   - r2.uvalue=16
@@ -946,8 +912,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[4278190336, 4294967040]
-  - r1.uvalue=[4278190336, 4294967040]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: 32-bit left shift interval by reg with negatives
 
@@ -961,8 +926,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[4278190336, 4294967040]
-  - r1.uvalue=[4278190336, 4294967040]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=8
   - r2.uvalue=8
@@ -978,8 +942,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294967040]
-  - r1.uvalue=[0, 4294967040]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: 32-bit left shift interval by reg crossing zero
 
@@ -993,8 +956,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294967040]
-  - r1.uvalue=[0, 4294967040]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=8
   - r2.uvalue=8
@@ -1002,7 +964,7 @@ post:
 test-case: left shift by interval
 
 pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1",
-      "r2.type=number", "r2.svalue=[1, 2]", "r2.uvalue=[1, 2]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[1, 2]", "r2.uvalue=[1, 2]", "r2.uvalue=r2.svalue"]
 
 code:
   <start>: |
@@ -1012,13 +974,12 @@ post:
   - r1.type=number
   - r2.type=number
   - r2.svalue=[1, 2]
-  - r2.uvalue=[1, 2]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 ---
 test-case: unsigned right shift by interval
 
 pre: ["r1.type=number", "r1.svalue=256", "r1.uvalue=256",
-      "r2.type=number", "r2.svalue=[1, 2]", "r2.uvalue=[1, 2]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[1, 2]", "r2.uvalue=[1, 2]", "r2.uvalue=r2.svalue"]
 
 code:
   <start>: |
@@ -1028,13 +989,12 @@ post:
   - r1.type=number
   - r2.type=number
   - r2.svalue=[1, 2]
-  - r2.uvalue=[1, 2]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 ---
 test-case: signed right shift by interval
 
 pre: ["r1.type=number", "r1.svalue=256", "r1.uvalue=256",
-      "r2.type=number", "r2.svalue=[1, 2]", "r2.uvalue=[1, 2]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[1, 2]", "r2.uvalue=[1, 2]", "r2.uvalue=r2.svalue"]
 
 code:
   <start>: |
@@ -1044,8 +1004,7 @@ post:
   - r1.type=number
   - r2.type=number
   - r2.svalue=[1, 2]
-  - r2.uvalue=[1, 2]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 ---
 test-case: unsigned right shift TOP by 32 imm
 
@@ -1058,8 +1017,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294967295]
-  - r1.uvalue=[0, 4294967295]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: signed right shift TOP by 32 imm
 
@@ -1084,8 +1042,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4294967295]
-  - r1.uvalue=[0, 4294967295]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=32
   - r2.uvalue=32
diff --git a/test-data/stack.yaml b/test-data/stack.yaml
index 8df80ca1e..bb18eca52 100644
--- a/test-data/stack.yaml
+++ b/test-data/stack.yaml
@@ -330,8 +330,8 @@ code:
 
 post:
   - r1.type=number
-  - r1.svalue=s[504...511].svalue
-  - r1.uvalue=s[504...511].uvalue
+  - s[504...511].svalue=r1.svalue
+  - s[504...511].uvalue=r1.uvalue
   - r2.type=stack
   - r2.stack_offset=504
   - r2.stack_numeric_size=8
@@ -353,7 +353,7 @@ code:
 post:
   - r2.type=stack
   - r2.stack_offset=504
-  - r3.type=s[504].type
+  - s[504].type=r3.type
   - r10.type=stack
   - r10.stack_offset=512
   - s[505...511].type=number
@@ -373,7 +373,7 @@ post:
   - r2.type=stack
   - r2.stack_offset=504
   - r2.stack_numeric_size=4
-  - r3.type=s[508...511].type
+  - s[508...511].type=r3.type
   - r10.type=stack
   - r10.stack_offset=512
   - s[504...507].type=number
@@ -392,8 +392,8 @@ code:
 
 post:
   - r1.type=number
-  - r1.svalue=s[508...511].svalue
-  - r1.uvalue=s[508...511].uvalue
+  - s[508...511].svalue=r1.svalue
+  - s[508...511].uvalue=r1.uvalue
   - r2.type=stack
   - r2.stack_offset=504
   - r2.stack_numeric_size=8
@@ -447,7 +447,7 @@ code:
     *(u8 *)(r10 - 16) = r0 ; this should reset r2.stack_numeric_size to 0
 
 post:
-  - r0.type=s[496].type
+  - s[496].type=r0.type
   - r2.type=stack
   - r2.stack_offset=[496, 504]
   - r10.type=stack
@@ -467,18 +467,16 @@ code:
     r3 = *(u64 *)(r10 - 16)
 
 post:
+  - r3.svalue=r2.svalue
+  - r3.uvalue=r2.uvalue
+  - s[496...503].uvalue=r2.uvalue
+  - s[496...503].svalue=r2.svalue
   - 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..09d3ef0d7 100644
--- a/test-data/subtract.yaml
+++ b/test-data/subtract.yaml
@@ -25,8 +25,7 @@ code:
 post:
   - r0.type=number
   - r0.svalue=[2147483645, 2147483647]
-  - r0.uvalue=[2147483645, 2147483647]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
 ---
 test-case: subtract a register from itself
 
@@ -151,8 +150,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[3810, 3990]
-  - r1.uvalue=[3810, 3990]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=stack
   - r2.stack_offset=[140, 230]
   - r10.type=stack
diff --git a/test-data/udivmod.yaml b/test-data/udivmod.yaml
index 85c833b86..b3455d52c 100644
--- a/test-data/udivmod.yaml
+++ b/test-data/udivmod.yaml
@@ -121,8 +121,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[-5, 5]
 
@@ -153,7 +152,7 @@ messages:
 test-case: non-zero divided by possibly zero register 2
 
 pre: ["r1.type=number", "r1.svalue=6", "r1.uvalue=6",
-      "r2.type=number", "r2.svalue=[0, 5]", "r2.uvalue=[0, 5]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[0, 5]", "r2.uvalue=[0, 5]", "r2.uvalue=r2.svalue"]
 
 options: ["!allow_division_by_zero"]
 
@@ -164,12 +163,10 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[0, 5]
-  - r2.uvalue=[0, 5]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 
 messages:
   - "0: Possible division by zero (r2 != 0)"
@@ -209,8 +206,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
 
 messages:
@@ -351,8 +347,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[-5, 5]
 
@@ -385,7 +380,7 @@ test-case: non-zero modulo possibly zero register 2
 options: ["!allow_division_by_zero"]
 
 pre: ["r1.type=number", "r1.svalue=6", "r1.uvalue=6",
-      "r2.type=number", "r2.svalue=[0, 5]", "r2.uvalue=[0, 5]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[0, 5]", "r2.uvalue=[0, 5]", "r2.uvalue=r2.svalue"]
 
 code:
   <start>: |
@@ -394,12 +389,10 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[0, 5]
-  - r2.uvalue=[0, 5]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 
 messages:
   - "0: Possible division by zero (r2 != 0)"
@@ -439,8 +432,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 6]
-  - r1.uvalue=[0, 6]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
 
 messages:
@@ -478,8 +470,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[0, 4]
-  - r1.uvalue=[0, 4]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r2.type=number
   - r2.svalue=[1, 5]
   - r2.uvalue=[1, 5]
@@ -591,5 +582,4 @@ code:
 post:
   - r0.type=number
   - r0.svalue=[0, 2055]
-  - r0.uvalue=[0, 2055]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
diff --git a/test-data/uninit.yaml b/test-data/uninit.yaml
index aada2a9d1..e2b340f09 100644
--- a/test-data/uninit.yaml
+++ b/test-data/uninit.yaml
@@ -67,9 +67,8 @@ code:
 
 post:
   - "r0.svalue=[0, 1]"
-  - "r0.svalue=r0.uvalue"
+  - "r0.uvalue=r0.svalue"
   - "r0.type=number"
-  - "r0.uvalue=[0, 1]"
 
 messages:
   - "0: Only numbers can be used as divisors (r3 != 0)"
@@ -107,9 +106,8 @@ code:
 
 post:
   - "r0.svalue=[0, 1]"
-  - "r0.svalue=r0.uvalue"
+  - "r0.uvalue=r0.svalue"
   - "r0.type=number"
-  - "r0.uvalue=[0, 1]"
 
 messages:
   - "0: Only numbers can be used as divisors (r3 != 0)"
@@ -128,9 +126,8 @@ code:
 
 post:
   - "r0.svalue=[0, 1]"
-  - "r0.svalue=r0.uvalue"
+  - "r0.uvalue=r0.svalue"
   - "r0.type=number"
-  - "r0.uvalue=[0, 1]"
 
 messages:
   - "0: Only numbers can be used as divisors (r3 != 0)"
@@ -312,9 +309,9 @@ code:
     r0 = r3
 
 post:
-  - "r0.svalue=r3.svalue"
-  - "r0.type=r3.type"
-  - "r0.uvalue=r3.uvalue"
+  - "r3.type=r0.type"
+  - "r3.svalue=r0.svalue"
+  - "r3.uvalue=r0.uvalue"
 
 ---
 test-case: Store uninitialized register to context - 8 bytes
@@ -510,16 +507,16 @@ code:
     r0 = *(u64 *)(r10 - 16)
 
 post:
-  - "r0.ctx_offset=s[496...503].ctx_offset"
-  - "r0.map_fd=s[496...503].map_fd"
-  - "r0.packet_offset=s[496...503].packet_offset"
-  - "r0.shared_offset=s[496...503].shared_offset"
-  - "r0.shared_region_size=s[496...503].shared_region_size"
-  - "r0.stack_numeric_size=s[496...503].stack_numeric_size"
-  - "r0.stack_offset=s[496...503].stack_offset"
-  - "r0.svalue=s[496...503].svalue"
-  - "r0.type=s[496...503].type"
-  - "r0.uvalue=s[496...503].uvalue"
+  - "s[496...503].ctx_offset=r0.ctx_offset"
+  - "s[496...503].map_fd=r0.map_fd"
+  - "s[496...503].packet_offset=r0.packet_offset"
+  - "s[496...503].shared_offset=r0.shared_offset"
+  - "s[496...503].shared_region_size=r0.shared_region_size"
+  - "s[496...503].stack_numeric_size=r0.stack_numeric_size"
+  - "s[496...503].stack_offset=r0.stack_offset"
+  - "s[496...503].svalue=r0.svalue"
+  - "s[496...503].type=r0.type"
+  - "s[496...503].uvalue=r0.uvalue"
   - "r10.stack_offset=512"
   - "r10.type=stack"
 
@@ -537,16 +534,16 @@ code:
     r0 = *(u64 *)(r10 - 8)
 
 post:
-  - "r0.ctx_offset=s[504...511].ctx_offset"
-  - "r0.map_fd=s[504...511].map_fd"
-  - "r0.packet_offset=s[504...511].packet_offset"
-  - "r0.shared_offset=s[504...511].shared_offset"
-  - "r0.shared_region_size=s[504...511].shared_region_size"
-  - "r0.stack_numeric_size=s[504...511].stack_numeric_size"
-  - "r0.stack_offset=s[504...511].stack_offset"
-  - "r0.svalue=s[504...511].svalue"
-  - "r0.type=s[504...511].type"
-  - "r0.uvalue=s[504...511].uvalue"
+  - "s[504...511].ctx_offset=r0.ctx_offset"
+  - "s[504...511].map_fd=r0.map_fd"
+  - "s[504...511].packet_offset=r0.packet_offset"
+  - "s[504...511].shared_offset=r0.shared_offset"
+  - "s[504...511].shared_region_size=r0.shared_region_size"
+  - "s[504...511].stack_numeric_size=r0.stack_numeric_size"
+  - "s[504...511].stack_offset=r0.stack_offset"
+  - "s[504...511].svalue=r0.svalue"
+  - "s[504...511].type=r0.type"
+  - "s[504...511].uvalue=r0.uvalue"
   - "r10.stack_offset=512"
   - "r10.type=stack"
 
@@ -563,16 +560,16 @@ code:
     r0 = *(u64 *)(r10 - 10)
 
 post:
-  - "r0.ctx_offset=s[502...509].ctx_offset"
-  - "r0.map_fd=s[502...509].map_fd"
-  - "r0.packet_offset=s[502...509].packet_offset"
-  - "r0.shared_offset=s[502...509].shared_offset"
-  - "r0.shared_region_size=s[502...509].shared_region_size"
-  - "r0.stack_numeric_size=s[502...509].stack_numeric_size"
-  - "r0.stack_offset=s[502...509].stack_offset"
-  - "r0.svalue=s[502...509].svalue"
-  - "r0.type=s[502...509].type"
-  - "r0.uvalue=s[502...509].uvalue"
+  - "s[502...509].ctx_offset=r0.ctx_offset"
+  - "s[502...509].map_fd=r0.map_fd"
+  - "s[502...509].packet_offset=r0.packet_offset"
+  - "s[502...509].shared_offset=r0.shared_offset"
+  - "s[502...509].shared_region_size=r0.shared_region_size"
+  - "s[502...509].stack_numeric_size=r0.stack_numeric_size"
+  - "s[502...509].stack_offset=r0.stack_offset"
+  - "s[502...509].svalue=r0.svalue"
+  - "s[502...509].type=r0.type"
+  - "s[502...509].uvalue=r0.uvalue"
   - "r10.stack_offset=512"
   - "r10.type=stack"
 
diff --git a/test-data/unop.yaml b/test-data/unop.yaml
index 124f33fe6..4e67124ff 100644
--- a/test-data/unop.yaml
+++ b/test-data/unop.yaml
@@ -115,7 +115,7 @@ post: ["r1.type=number", "r1.svalue=40926266145", "r1.uvalue=40926266145"]
 ---
 test-case: be16 range on little-endian
 
-pre: ["r1.type=number", "r1.svalue=[0, 2]", "r1.uvalue=[0, 2]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 2]", "r1.uvalue=[0, 2]", "r1.uvalue=r1.svalue"]
 
 options: ["!big_endian"]
 
@@ -127,7 +127,7 @@ post: ["r1.type=number"]
 ---
 test-case: be16 range on big-endian
 
-pre: ["r1.type=number", "r1.svalue=[0, 2]", "r1.uvalue=[0, 2]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 2]", "r1.uvalue=[0, 2]", "r1.uvalue=r1.svalue"]
 
 options: ["big_endian"]
 
@@ -211,7 +211,7 @@ post: ["r1.type=number", "r1.svalue=2396871057337221120", "r1.uvalue=23968710573
 ---
 test-case: le16 range on little-endian
 
-pre: ["r1.type=number", "r1.svalue=[0, 2]", "r1.uvalue=[0, 2]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 2]", "r1.uvalue=[0, 2]", "r1.uvalue=r1.svalue"]
 
 options: ["!big_endian"]
 
@@ -223,7 +223,7 @@ post: ["r1.type=number"]
 ---
 test-case: le16 range on big-endian
 
-pre: ["r1.type=number", "r1.svalue=[0, 2]", "r1.uvalue=[0, 2]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 2]", "r1.uvalue=[0, 2]", "r1.uvalue=r1.svalue"]
 
 options: ["!big_endian"]
 
@@ -307,7 +307,7 @@ post: ["r1.type=number", "r1.svalue=2396871057337221120", "r1.uvalue=23968710573
 ---
 test-case: swap16 range on little-endian
 
-pre: ["r1.type=number", "r1.svalue=[0, 2]", "r1.uvalue=[0, 2]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 2]", "r1.uvalue=[0, 2]", "r1.uvalue=r1.svalue"]
 
 options: ["!big_endian"]
 
@@ -319,7 +319,7 @@ post: ["r1.type=number"]
 ---
 test-case: swap16 range on big-endian
 
-pre: ["r1.type=number", "r1.svalue=[0, 2]", "r1.uvalue=[0, 2]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 2]", "r1.uvalue=[0, 2]", "r1.uvalue=r1.svalue"]
 
 options: ["big_endian"]
 
diff --git a/test-data/unsigned.yaml b/test-data/unsigned.yaml
index 6fcc0369d..fe8d4b15a 100644
--- a/test-data/unsigned.yaml
+++ b/test-data/unsigned.yaml
@@ -98,7 +98,7 @@ messages:
   - "0: Code becomes unreachable (assume r1 w< 1)"
 ---
 test-case: "assume [0, 1] < 0 implies bottom"
-pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.uvalue=r1.svalue"]
 code:
   <start>: assume r1 < 0
 post: []
@@ -106,7 +106,7 @@ messages:
   - "0: Code becomes unreachable (assume r1 < 0)"
 ---
 test-case: "assume [0, 1] w< 0 implies bottom"
-pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.uvalue=r1.svalue"]
 code:
   <start>: assume w1 < 0
 post: []
@@ -114,7 +114,7 @@ messages:
   - "0: Code becomes unreachable (assume r1 w< 0)"
 ---
 test-case: "assume [2, 3] < 1 implies bottom"
-pre: ["r1.type=number", "r1.svalue=[2, 3]", "r1.uvalue=[2, 3]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[2, 3]", "r1.uvalue=[2, 3]", "r1.uvalue=r1.svalue"]
 code:
   <start>: assume r1 < 1
 post: []
@@ -122,7 +122,7 @@ messages:
   - "0: Code becomes unreachable (assume r1 < 1)"
 ---
 test-case: "assume [2, 3] w< 1 implies bottom"
-pre: ["r1.type=number", "r1.svalue=[2, 3]", "r1.uvalue=[2, 3]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[2, 3]", "r1.uvalue=[2, 3]", "r1.uvalue=r1.svalue"]
 code:
   <start>: assume w1 < 1
 post: []
@@ -179,7 +179,7 @@ messages:
 ---
 test-case: "assume 1 < [0, 1] implies bottom"
 pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1",
-      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.uvalue=r2.svalue"]
 code:
   <start>: assume r1 < r2
 post: []
@@ -188,7 +188,7 @@ messages:
 ---
 test-case: "assume 1 w< [0, 1] implies bottom"
 pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1",
-      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.uvalue=r2.svalue"]
 code:
   <start>: assume w1 < r2
 post: []
@@ -197,7 +197,7 @@ messages:
 ---
 test-case: "assume -1 < [0, 1] implies bottom"
 pre: ["r1.type=number", "r1.svalue=-1", "r1.uvalue=18446744073709551615",
-      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.uvalue=r2.svalue"]
 code:
   <start>: assume r1 < r2
 post: []
@@ -206,7 +206,7 @@ messages:
 ---
 test-case: "assume -1 w< [0, 1] implies bottom"
 pre: ["r1.type=number", "r1.svalue=-1", "r1.uvalue=18446744073709551615",
-      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.uvalue=r2.svalue"]
 code:
   <start>: assume w1 < r2
 post: []
@@ -215,7 +215,7 @@ messages:
 ---
 test-case: "assume -1 < [1, 2] implies bottom"
 pre: ["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.type=number", "r2.svalue=[1, 2]", "r2.uvalue=[1, 2]", "r2.uvalue=r2.svalue"]
 code:
   <start>: assume r1 < r2
 post: []
@@ -224,7 +224,7 @@ messages:
 ---
 test-case: "assume -1 w< [1, 2] implies bottom"
 pre: ["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.type=number", "r2.svalue=[1, 2]", "r2.uvalue=[1, 2]", "r2.uvalue=r2.svalue"]
 code:
   <start>: assume w1 < r2
 post: []
@@ -233,7 +233,7 @@ messages:
 ---
 test-case: "assume 2 < [0, 1] implies bottom"
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.uvalue=r2.svalue"]
 code:
   <start>: assume r1 < r2
 post: []
@@ -242,7 +242,7 @@ messages:
 ---
 test-case: "assume 2 w< [0, 1] implies bottom"
 pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
-      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.uvalue=r2.svalue"]
 code:
   <start>: assume w1 < r2
 post: []
@@ -251,7 +251,7 @@ messages:
 ---
 test-case: "assume 1 < [0, 1] implies bottom"
 pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1",
-      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.uvalue=r2.svalue"]
 code:
   <start>: assume r1 < r2
 post: []
@@ -260,7 +260,7 @@ messages:
 ---
 test-case: "assume 1 w< [0, 1] implies bottom"
 pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1",
-      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.uvalue=r2.svalue"]
 code:
   <start>: assume w1 < r2
 post: []
@@ -269,7 +269,7 @@ messages:
 ---
 test-case: "assume 2 < [0, 1] implies bottom"
 pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1",
-      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.uvalue=r2.svalue"]
 code:
   <start>: assume r1 < r2
 post: []
@@ -278,7 +278,7 @@ messages:
 ---
 test-case: "assume 2 w< [0, 1] implies bottom"
 pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1",
-      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.uvalue=r2.svalue"]
 code:
   <start>: assume w1 < r2
 post: []
@@ -286,8 +286,8 @@ messages:
   - "0: Code becomes unreachable (assume r1 w< r2)"
 ---
 test-case: "assume [2, 3] < [1, 2] implies bottom"
-pre: ["r1.type=number", "r1.svalue=[2, 3]", "r1.uvalue=[2, 3]", "r1.svalue=r1.uvalue",
-      "r2.type=number", "r2.svalue=[1, 2]", "r2.uvalue=[1, 2]", "r2.svalue=r2.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[2, 3]", "r1.uvalue=[2, 3]", "r1.uvalue=r1.svalue",
+      "r2.type=number", "r2.svalue=[1, 2]", "r2.uvalue=[1, 2]", "r2.uvalue=r2.svalue"]
 code:
   <start>: assume r1 < r2
 post: []
@@ -295,8 +295,8 @@ messages:
   - "0: Code becomes unreachable (assume r1 < r2)"
 ---
 test-case: "assume [2, 3] w< [1, 2] implies bottom"
-pre: ["r1.type=number", "r1.svalue=[2, 3]", "r1.uvalue=[2, 3]", "r1.svalue=r1.uvalue",
-      "r2.type=number", "r2.svalue=[1, 2]", "r2.uvalue=[1, 2]", "r2.svalue=r2.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[2, 3]", "r1.uvalue=[2, 3]", "r1.uvalue=r1.svalue",
+      "r2.type=number", "r2.svalue=[1, 2]", "r2.uvalue=[1, 2]", "r2.uvalue=r2.svalue"]
 code:
   <start>: assume w1 < r2
 post: []
@@ -305,7 +305,7 @@ messages:
 ---
 test-case: "assume [-2, -1] < [0, 1] implies bottom"
 pre: ["r1.type=number", "r1.svalue=[-2, -1]", "r1.uvalue=[18446744073709551614, 18446744073709551615]",
-      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.uvalue=r2.svalue"]
 code:
   <start>: assume r1 < r2
 post: []
@@ -314,7 +314,7 @@ messages:
 ---
 test-case: "assume [-2, -1] w< [0, 1] implies bottom"
 pre: ["r1.type=number", "r1.svalue=[-2, -1]", "r1.uvalue=[18446744073709551614, 18446744073709551615]",
-      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[0, 1]", "r2.uvalue=[0, 1]", "r2.uvalue=r2.svalue"]
 code:
   <start>: assume w1 < r2
 post: []
@@ -498,7 +498,7 @@ messages:
   - "2: Code becomes unreachable (assume r1 w< r2)"
 ---
 test-case: "assume [1, INT_MAX] < 1 implies bottom"
-pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775806]", "r1.uvalue=[0, 9223372036854775806]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775806]", "r1.uvalue=[0, 9223372036854775806]", "r1.uvalue=r1.svalue"]
 code:
   <start>: |
     r1 += 1
@@ -508,7 +508,7 @@ messages:
   - "1: Code becomes unreachable (assume r1 < 1)"
 ---
 test-case: "assume [1, INT32_MAX] w< 1 implies bottom"
-pre: ["r1.type=number", "r1.svalue=[1, 2147483647]", "r1.uvalue=[1, 2147483647]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[1, 2147483647]", "r1.uvalue=[1, 2147483647]", "r1.uvalue=r1.svalue"]
 code:
   <start>: |
     assume w1 < 1
@@ -517,7 +517,7 @@ messages:
   - "0: Code becomes unreachable (assume r1 w< 1)"
 ---
 test-case: "assume [INT_MAX-1, INT_MAX] < 1 implies bottom"
-pre: ["r1.type=number", "r1.svalue=[9223372036854775803, 9223372036854775804]", "r1.uvalue=[9223372036854775803, 9223372036854775804]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[9223372036854775803, 9223372036854775804]", "r1.uvalue=[9223372036854775803, 9223372036854775804]", "r1.uvalue=r1.svalue"]
 code:
   <start>: |
     r1 += 3
@@ -527,7 +527,7 @@ messages:
   - "1: Code becomes unreachable (assume r1 < 1)"
 ---
 test-case: "assume [INT32_MAX-1, INT32_MAX] < 1 implies bottom"
-pre: ["r1.type=number", "r1.svalue=[2147483646, 2147483647]", "r1.uvalue=[2147483646, 2147483647]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[2147483646, 2147483647]", "r1.uvalue=[2147483646, 2147483647]", "r1.uvalue=r1.svalue"]
 code:
   <start>: |
     assume w1 < 1
@@ -536,7 +536,7 @@ messages:
   - "0: Code becomes unreachable (assume r1 w< 1)"
 ---
 test-case: "assume [INT_MAX, INT_MAX+1] < 1 implies bottom"
-pre: ["r1.type=number", "r1.svalue=[9223372036854775803, 9223372036854775804]", "r1.uvalue=[9223372036854775803, 9223372036854775804]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[9223372036854775803, 9223372036854775804]", "r1.uvalue=[9223372036854775803, 9223372036854775804]", "r1.uvalue=r1.svalue"]
 code:
   <start>: |
     r1 += 4
@@ -562,35 +562,35 @@ code:
 post: ["r1.type=number", "r1.svalue=0", "r1.uvalue=0"]
 ---
 test-case: "assume [0, 1] < 2 nop"
-pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue"]
 ---
 test-case: "assume [0, 1] w< 2 nop"
-pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue"]
 ---
 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"]
+pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue"]
 ---
 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"]
+pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue"]
 ---
 test-case: "assume [0, 1] > 1 implies bottom"
-pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.uvalue=r1.svalue"]
 code:
   <start>: |
     assume r1 > 1
@@ -599,7 +599,7 @@ messages:
   - "0: Code becomes unreachable (assume r1 > 1)"
 ---
 test-case: "assume [0, 1] w> 1 implies bottom"
-pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.uvalue=r1.svalue"]
 code:
   <start>: |
     assume w1 > 1
@@ -608,32 +608,32 @@ messages:
   - "0: Code becomes unreachable (assume r1 w> 1)"
 ---
 test-case: "assume [1, 2] > 1 narrows to 2"
-pre: ["r1.type=number", "r1.svalue=[1, 2]", "r1.uvalue=[1, 2]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[1, 2]", "r1.uvalue=[1, 2]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue"]
 ---
 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"]
+pre: ["r1.type=number", "r1.svalue=[1, 2]", "r1.uvalue=[1, 2]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue"]
 ---
 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"]
+pre: ["r1.type=number", "r1.svalue=[1, 3]", "r1.uvalue=[1, 3]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue"]
 ---
 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"]
+pre: ["r1.type=number", "r1.svalue=[1, 3]", "r1.uvalue=[1, 3]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue"]
 ---
 test-case: "assume 1 > 0 nop"
 pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1"]
@@ -650,35 +650,35 @@ code:
 post: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1"]
 ---
 test-case: "assume [1, INT_MAX] > 0 nop"
-pre: ["r1.type=number", "r1.svalue=[1, 9223372036854775807]", "r1.uvalue=[1, 9223372036854775807]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[1, 9223372036854775807]", "r1.uvalue=[1, 9223372036854775807]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue"]
 ---
 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"]
+pre: ["r1.type=number", "r1.svalue=[1, 2147483646]", "r1.uvalue=[1, 2147483646]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue"]
 ---
 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"]
+pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775807]", "r1.uvalue=[0, 9223372036854775807]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue"]
 ---
 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"]
+pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue"]
 ---
 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"]
+pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775807]", "r1.uvalue=[0, 9223372036854775807]", "r1.uvalue=r1.svalue"]
 code:
   <start>: |
     r2 = 9223372036854775807ll
@@ -688,7 +688,7 @@ messages:
   - "1: Code becomes unreachable (assume r1 > r2)"
 ---
 test-case: "assume [0, INT32_MAX] w> INT32_MAX implies bottom"
-pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]", "r1.uvalue=r1.svalue"]
 code:
   <start>: |
     assume w1 > 2147483647
@@ -697,28 +697,22 @@ messages:
   - "0: Code becomes unreachable (assume r1 w> 2147483647)"
 ---
 test-case: "assume [0, INT_MAX-4] >= INT_MAX-4 narrows to INT_MAX-4"
-pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775803]", "r1.uvalue=[0, 9223372036854775803]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775803]", "r1.uvalue=[0, 9223372036854775803]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue",
+       "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"]
+pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue",
+       "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"]
@@ -749,13 +743,13 @@ post: ["r1.type=number", "r1.svalue=-1", "r1.uvalue=18446744073709551615"]
 ---
 test-case: "assume [-1, 1] > [1, 2] narrows"
 pre: ["r1.type=number", "r1.svalue=[-1, 1]",
-      "r2.type=number", "r2.svalue=[1, 2]", "r2.uvalue=[1, 2]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[1, 2]", "r2.uvalue=[1, 2]", "r2.uvalue=r2.svalue"]
 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.uvalue=r2.svalue",
+       "r2.svalue-r1.uvalue<=-1"]
 ---
 test-case: "assume [-1, 1] >= 2 narrows"
 pre: ["r1.type=number", "r1.svalue=[-1, 1]"]
@@ -766,13 +760,13 @@ post: ["r1.type=number", "r1.svalue=-1", "r1.uvalue=18446744073709551615"]
 ---
 test-case: "assume [-1, 1] >= [2, 3] narrows"
 pre: ["r1.type=number", "r1.svalue=[-1, 1]",
-      "r2.type=number", "r2.svalue=[2, 3]", "r2.uvalue=[2, 3]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[2, 3]", "r2.uvalue=[2, 3]", "r2.uvalue=r2.svalue"]
 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.uvalue=r2.svalue",
+       "r2.svalue-r1.uvalue<=-1"]
 ---
 test-case: "assume [-1, 1] < -1 narrows"
 pre: ["r1.type=number", "r1.svalue=[-1, 1]"]
@@ -907,48 +901,42 @@ post: ["r1.type=number", "r1.svalue=[-2147483648, -1]", "r1.uvalue=[184467440715
        "r2.type=number", "r2.svalue=[0, 2147483647]", "r2.uvalue=[0, 2147483647]"]
 ---
 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",
-      "r2.type=number", "r2.svalue=[0, 9223372036854775807]", "r2.svalue=[0, 9223372036854775807]", "r2.svalue=r2.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775807]", "r1.uvalue=[0, 9223372036854775807]", "r1.uvalue=r1.svalue",
+      "r2.type=number", "r2.svalue=[0, 9223372036854775807]", "r2.svalue=[0, 9223372036854775807]", "r2.uvalue=r2.svalue"]
 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.uvalue=r1.svalue", "r2.uvalue=r1.svalue", "r2.svalue=r1.svalue",
+       "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",
-      "r2.type=number", "r2.svalue=[0, 2147483647]", "r2.uvalue=[0, 2147483647]", "r2.svalue=r2.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]", "r1.uvalue=r1.svalue",
+      "r2.type=number", "r2.svalue=[0, 2147483647]", "r2.uvalue=[0, 2147483647]", "r2.uvalue=r2.svalue"]
 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.uvalue=r1.svalue", "r2.uvalue=r1.svalue", "r2.svalue=r1.svalue",
+       "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",
-      "r2.type=number", "r2.svalue=[0, 9223372036854775807]", "r2.uvalue=[0, 9223372036854775807]", "r2.svalue=r2.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775807]", "r1.uvalue=[0, 9223372036854775807]", "r1.uvalue=r1.svalue",
+      "r2.type=number", "r2.svalue=[0, 9223372036854775807]", "r2.uvalue=[0, 9223372036854775807]", "r2.uvalue=r2.svalue"]
 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.uvalue=r1.svalue",
+       "r2.type=number", "r2.svalue=[0, 9223372036854775807]", "r2.uvalue=r2.svalue"]
 ---
 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",
-      "r2.type=number", "r2.svalue=[0, 2147483647]", "r2.uvalue=[0, 2147483647]", "r2.svalue=r2.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]", "r1.uvalue=r1.svalue",
+      "r2.type=number", "r2.svalue=[0, 2147483647]", "r2.uvalue=[0, 2147483647]", "r2.uvalue=r2.svalue"]
 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.uvalue=r1.svalue",
+       "r2.type=number", "r2.svalue=[0, 2147483647]", "r2.uvalue=r2.svalue"]
 ---
 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,31 +954,27 @@ 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",
-      "r2.type=number", "r2.svalue=[0, 9223372036854775807]", "r2.uvalue=[0, 9223372036854775807]", "r2.svalue=r2.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775807]", "r1.uvalue=[0, 9223372036854775807]", "r1.uvalue=r1.svalue",
+      "r2.type=number", "r2.svalue=[0, 9223372036854775807]", "r2.uvalue=[0, 9223372036854775807]", "r2.uvalue=r2.svalue"]
 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.uvalue=r1.svalue",
+       "r2.type=number", "r2.svalue=[1, 9223372036854775807]", "r2.uvalue=r2.svalue",
+       "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",
-      "r2.type=number", "r2.svalue=[0, 2147483647]", "r2.uvalue=[0, 2147483647]", "r2.svalue=r2.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]", "r1.uvalue=r1.svalue",
+      "r2.type=number", "r2.svalue=[0, 2147483647]", "r2.uvalue=[0, 2147483647]", "r2.uvalue=r2.svalue"]
 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.uvalue=r1.svalue",
+       "r2.type=number", "r2.svalue=[1, 2147483647]", "r2.uvalue=r2.svalue",
+       "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,30 +994,27 @@ 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",
-      "r2.type=number", "r2.svalue=[0, 9223372036854775807]", "r2.uvalue=[0, 9223372036854775807]", "r2.svalue=r2.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775807]", "r1.uvalue=[0, 9223372036854775807]", "r1.uvalue=r1.svalue",
+      "r2.type=number", "r2.svalue=[0, 9223372036854775807]", "r2.uvalue=[0, 9223372036854775807]", "r2.uvalue=r2.svalue"]
 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.uvalue=r1.svalue",
+       "r2.type=number", "r2.svalue=[0, 9223372036854775806]", "r2.uvalue=r2.svalue",
+       "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",
-      "r2.type=number", "r2.svalue=[0, 2147483647]", "r2.uvalue=[0, 2147483647]", "r2.svalue=r2.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]", "r1.uvalue=r1.svalue",
+      "r2.type=number", "r2.svalue=[0, 2147483647]", "r2.uvalue=[0, 2147483647]", "r2.uvalue=r2.svalue"]
 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.uvalue=r1.svalue",
+       "r2.type=number", "r2.svalue=[0, 2147483646]", "r2.uvalue=r2.svalue",
+       "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]", "r2.uvalue=r1.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]",
@@ -1129,18 +1104,16 @@ post: ["r1.type=number", "r1.uvalue=[4294967296, 4294967300]"]  # could be narro
 ---
 test-case: "assume [1, 4] w< INT32_MAX+5"
 pre: ["r1.type=number", "r1.uvalue=[1, 4]",
-      "r2.type=number", "r2.svalue=[1, 2147483652]", "r2.uvalue=[1, 2147483652]", "r2.svalue=r2.uvalue"]
+      "r2.type=number", "r2.svalue=[1, 2147483652]", "r2.uvalue=[1, 2147483652]", "r2.uvalue=r2.svalue"]
 code:
   <start>: assume w1 < r2
 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
+  - r2.uvalue=r2.svalue
 ---
 test-case: signed 64-bit negative LT
 pre: ["r1.type=number", "r1.svalue=[-3, -1]", "r1.uvalue=[18446744073709551613, 18446744073709551615]"]
@@ -1149,10 +1122,10 @@ code:
 post: ["r1.type=number", "r1.svalue=-3", "r1.uvalue=18446744073709551613"]
 ---
 test-case: signed 64-bit positive LT
-pre: ["r1.type=number", "r1.svalue=[1, 3]", "r1.uvalue=[1, 3]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[1, 3]", "r1.uvalue=[1, 3]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue"]
 ---
 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.uvalue=r1.svalue"]
 ---
 test-case: signed 32-bit negative LT
 pre: ["r1.type=number", "r1.svalue=[-3, -1]", "r1.uvalue=[18446744073709551613, 18446744073709551615]"]
@@ -1173,10 +1146,10 @@ code:
 post: ["r1.type=number", "r1.svalue=-3", "r1.uvalue=18446744073709551613"]
 ---
 test-case: signed 32-bit positive LT
-pre: ["r1.type=number", "r1.svalue=[1, 3]", "r1.uvalue=[1, 3]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[1, 3]", "r1.uvalue=[1, 3]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue"]
 ---
 test-case: signed 32-bit LT
 pre: ["r1.type=number", "r1.svalue=[-1, 1]"]
@@ -1191,16 +1164,16 @@ code:
 post: ["r1.type=number", "r1.svalue=[-2, -1]", "r1.uvalue=[18446744073709551614, 18446744073709551615]"]
 ---
 test-case: signed 32-bit positive GT
-pre: ["r1.type=number", "r1.svalue=[1, 4]", "r1.uvalue=[1, 4]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[1, 4]", "r1.uvalue=[1, 4]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue"]
 ---
 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.uvalue=r1.svalue"]
 ---
 test-case: "assume TOP s> 0 narrows to [1, INT64_MAX]"
 pre: ["r1.type=number"]
@@ -1209,8 +1182,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[1, 9223372036854775807]
-  - r1.uvalue=[1, 9223372036854775807]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 ---
 test-case: "assume [-2, 2] s> -2"
 pre: ["r1.type=number", "r1.svalue=[-2, 2]"]
@@ -1219,16 +1191,16 @@ code:
 post: ["r1.type=number", "r1.svalue=[-1, 2]"]
 ---
 test-case: "assume [0, 3] s> 1"
-pre: ["r1.type=number", "r1.svalue=[0, 3]", "r1.uvalue=[0, 3]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 3]", "r1.uvalue=[0, 3]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue"]
 ---
 test-case: "assume [0, 3] s> 1"
-pre: ["r1.type=number", "r1.svalue=[0, 3]", "r1.uvalue=[0, 3]", "r1.svalue=r1.uvalue"]
+pre: ["r1.type=number", "r1.svalue=[0, 3]", "r1.uvalue=[0, 3]", "r1.uvalue=r1.svalue"]
 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.uvalue=r1.svalue"]
 ---
 test-case: "assume [-4, -1] s> -3"
 pre: ["r1.type=number", "r1.svalue=[-4, -1]", "r1.uvalue=[18446744073709551612, 18446744073709551615]"]