diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp
index 7d34ba9df..48ae3c265 100644
--- a/src/crab/ebpf_domain.cpp
+++ b/src/crab/ebpf_domain.cpp
@@ -2334,11 +2334,9 @@ void ebpf_domain_t::shl(const Reg& dst_reg, int imm, const int finite_width) {
                 ub_n = ub_n << imm & uint_max;
             }
             m_inv.set(dst.uvalue, interval_t{lb_n, ub_n});
-            if (to_signed(ub_n) >= to_signed(lb_n)) {
-                m_inv.assign(dst.svalue, dst.uvalue);
-            } else {
-                havoc(dst.svalue);
-            }
+            m_inv.assign(dst.svalue, dst.uvalue);
+            overflow_signed(m_inv, dst.svalue, finite_width);
+            overflow_unsigned(m_inv, dst.uvalue, finite_width);
             return;
         }
     }
@@ -2374,12 +2372,9 @@ void ebpf_domain_t::lshr(const Reg& dst_reg, int imm, int finite_width) {
             }
         }
         m_inv.set(dst.uvalue, interval_t{lb_n, ub_n});
-        if (ub_n.narrow<int64_t>() >= lb_n.narrow<int64_t>()) {
-            // ? m_inv.set(dst.svalue, crab::interval_t{number_t{(int64_t)lb_n}, number_t{(int64_t)ub_n}});
-            m_inv.assign(dst.svalue, dst.uvalue);
-        } else {
-            havoc(dst.svalue);
-        }
+        m_inv.assign(dst.svalue, dst.uvalue);
+        overflow_signed(m_inv, dst.svalue, finite_width);
+        overflow_unsigned(m_inv, dst.uvalue, finite_width);
         return;
     }
     havoc(dst.svalue);
@@ -2464,11 +2459,9 @@ void ebpf_domain_t::ashr(const Reg& dst_reg, const linear_expression_t& right_sv
                 }
             }
             m_inv.set(dst.svalue, interval_t{lb_n, ub_n});
-            if (to_unsigned(ub_n) >= to_unsigned(lb_n)) {
-                m_inv.assign(dst.uvalue, dst.svalue);
-            } else {
-                havoc(dst.uvalue);
-            }
+            m_inv.assign(dst.uvalue, dst.svalue);
+            overflow_signed(m_inv, dst.svalue, finite_width);
+            overflow_unsigned(m_inv, dst.uvalue, finite_width);
             return;
         }
     }
diff --git a/test-data/shift.yaml b/test-data/shift.yaml
index 2a78650a5..b9d0e1ac3 100644
--- a/test-data/shift.yaml
+++ b/test-data/shift.yaml
@@ -1104,3 +1104,563 @@ post:
   - r2.type=number
   - r2.svalue=32
   - r2.uvalue=32
+
+---
+test-case: check that unsigned right shift by 0 is idempotent - MIN_INT64
+
+pre:
+  - r0.type=number
+  - r0.svalue=-9223372036854775808
+  - r0.uvalue=9223372036854775808
+  - r1.type=number
+  - r1.svalue=-9223372036854775808
+  - r1.uvalue=9223372036854775808
+
+code:
+  <start>: |
+    r0 >>= 0
+    if r1 == r0 goto <one>
+    r2 = 0
+    exit
+  <one>: |
+    r2 = 1
+    exit
+
+post:
+  - r0.type=number
+  - r0.svalue=-9223372036854775808
+  - r0.uvalue=9223372036854775808
+  - r1.type=number
+  - r1.svalue=-9223372036854775808
+  - r1.uvalue=9223372036854775808
+  - r0.svalue=r1.svalue
+  - r0.uvalue=r1.uvalue
+  - r2.svalue=1
+  - r2.type=number
+  - r2.uvalue=1
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+
+---
+test-case: check that unsigned right shift by 0 is idempotent - MAX_INT64
+
+pre:
+  - r0.type=number
+  - r0.svalue=9223372036854775807
+  - r0.uvalue=9223372036854775807
+  - r1.type=number
+  - r1.svalue=9223372036854775807
+  - r1.uvalue=9223372036854775807
+
+code:
+  <start>: |
+    r0 >>= 0
+    if r1 == r0 goto <one>
+    r2 = 0
+    exit
+  <one>: |
+    r2 = 1
+    exit
+
+post:
+  - r0.svalue=9223372036854775807
+  - r0.svalue=r1.svalue
+  - r0.type=number
+  - r0.uvalue=9223372036854775807
+  - r0.uvalue=r1.uvalue
+  - r1.svalue=9223372036854775807
+  - r1.type=number
+  - r1.uvalue=9223372036854775807
+  - r2.svalue=1
+  - r2.type=number
+  - r2.uvalue=1
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+
+---
+test-case: check that unsigned right shift by 0 is idempotent - MIN_INT64 - via register
+
+pre:
+  - r0.type=number
+  - r0.svalue=-9223372036854775808
+  - r0.uvalue=9223372036854775808
+  - r1.type=number
+  - r1.svalue=-9223372036854775808
+  - r1.uvalue=9223372036854775808
+  - r3.type=number
+  - r3.uvalue=0
+  - r3.svalue=0
+
+code:
+  <start>: |
+    r0 >>= r3
+    if r1 == r0 goto <one>
+    r2 = 0
+    exit
+  <one>: |
+    r2 = 1
+    exit
+
+post:
+  - r0.type=number
+  - r0.svalue=-9223372036854775808
+  - r0.uvalue=9223372036854775808
+  - r1.type=number
+  - r1.svalue=-9223372036854775808
+  - r1.uvalue=9223372036854775808
+  - r0.svalue=r1.svalue
+  - r0.uvalue=r1.uvalue
+  - r2.svalue=1
+  - r2.type=number
+  - r2.uvalue=1
+  - r3.type=number
+  - r3.uvalue=0
+  - r3.svalue=0
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+
+---
+test-case: check that unsigned right shift by 0 is idempotent - MAX_INT64 - via register
+
+pre:
+  - r0.type=number
+  - r0.svalue=9223372036854775807
+  - r0.uvalue=9223372036854775807
+  - r1.type=number
+  - r1.svalue=9223372036854775807
+  - r1.uvalue=9223372036854775807
+  - r3.type=number
+  - r3.uvalue=0
+  - r3.svalue=0
+
+code:
+  <start>: |
+    r0 >>= r3
+    if r1 == r0 goto <one>
+    r2 = 0
+    exit
+  <one>: |
+    r2 = 1
+    exit
+
+post:
+  - r0.svalue=9223372036854775807
+  - r0.svalue=r1.svalue
+  - r0.type=number
+  - r0.uvalue=9223372036854775807
+  - r0.uvalue=r1.uvalue
+  - r1.svalue=9223372036854775807
+  - r1.type=number
+  - r1.uvalue=9223372036854775807
+  - r2.svalue=1
+  - r2.type=number
+  - r2.uvalue=1
+  - r3.type=number
+  - r3.uvalue=0
+  - r3.svalue=0
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+
+---
+test-case: check that signed right shift by 0 is idempotent - MIN_INT64
+
+pre:
+  - r0.type=number
+  - r0.svalue=-9223372036854775808
+  - r0.uvalue=9223372036854775808
+  - r1.type=number
+  - r1.svalue=-9223372036854775808
+  - r1.uvalue=9223372036854775808
+
+code:
+  <start>: |
+    r0 s>>= 0
+    if r1 == r0 goto <one>
+    r2 = 0
+    exit
+  <one>: |
+    r2 = 1
+    exit
+
+post:
+  - r0.type=number
+  - r0.svalue=-9223372036854775808
+  - r0.uvalue=9223372036854775808
+  - r1.type=number
+  - r1.svalue=-9223372036854775808
+  - r1.uvalue=9223372036854775808
+  - r0.svalue=r1.svalue
+  - r0.uvalue=r1.uvalue
+  - r2.svalue=1
+  - r2.type=number
+  - r2.uvalue=1
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+
+---
+test-case: check that signed right shift by 0 is idempotent - MAX_INT64
+
+pre:
+  - r0.type=number
+  - r0.svalue=9223372036854775807
+  - r0.uvalue=9223372036854775807
+  - r1.type=number
+  - r1.svalue=9223372036854775807
+  - r1.uvalue=9223372036854775807
+
+code:
+  <start>: |
+    r0 s>>= 0
+    if r1 == r0 goto <one>
+    r2 = 0
+    exit
+  <one>: |
+    r2 = 1
+    exit
+
+post:
+  - r0.svalue=9223372036854775807
+  - r0.svalue=r1.svalue
+  - r0.type=number
+  - r0.uvalue=9223372036854775807
+  - r0.uvalue=r1.uvalue
+  - r1.svalue=9223372036854775807
+  - r1.type=number
+  - r1.uvalue=9223372036854775807
+  - r2.svalue=1
+  - r2.type=number
+  - r2.uvalue=1
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+
+---
+test-case: check that signed right shift by 0 is idempotent - MAX_UINT64
+
+pre:
+  - r0.type=number
+  - r0.svalue=-1
+  - r0.uvalue=18446744073709551615
+  - r1.type=number
+  - r1.svalue=-1
+  - r1.uvalue=18446744073709551615
+
+code:
+  <start>: |
+    r0 s>>= 0
+    if r1 == r0 goto <one>
+    r2 = 0
+    exit
+  <one>: |
+    r2 = 1
+    exit
+
+post:
+  - r0.svalue=-1
+  - r0.svalue=r1.svalue
+  - r0.type=number
+  - r0.uvalue=18446744073709551615
+  - r0.uvalue=r1.uvalue
+  - r1.svalue=-1
+  - r1.type=number
+  - r1.uvalue=18446744073709551615
+  - r2.svalue=1
+  - r2.type=number
+  - r2.uvalue=1
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+
+---
+test-case: check that signed right shift by 0 is idempotent - MIN_INT64 - via register
+
+pre:
+  - r0.type=number
+  - r0.svalue=-9223372036854775808
+  - r0.uvalue=9223372036854775808
+  - r1.type=number
+  - r1.svalue=-9223372036854775808
+  - r1.uvalue=9223372036854775808
+  - r3.type=number
+  - r3.uvalue=0
+  - r3.svalue=0
+
+code:
+  <start>: |
+    r0 s>>= r3
+    if r1 == r0 goto <one>
+    r2 = 0
+    exit
+  <one>: |
+    r2 = 1
+    exit
+
+post:
+  - r0.type=number
+  - r0.svalue=-9223372036854775808
+  - r0.uvalue=9223372036854775808
+  - r1.type=number
+  - r1.svalue=-9223372036854775808
+  - r1.uvalue=9223372036854775808
+  - r0.svalue=r1.svalue
+  - r0.uvalue=r1.uvalue
+  - r2.svalue=1
+  - r2.type=number
+  - r2.uvalue=1
+  - r3.type=number
+  - r3.uvalue=0
+  - r3.svalue=0
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+
+---
+test-case: check that signed right shift by 0 is idempotent - MAX_INT64
+
+pre:
+  - r0.type=number
+  - r0.svalue=9223372036854775807
+  - r0.uvalue=9223372036854775807
+  - r1.type=number
+  - r1.svalue=9223372036854775807
+  - r1.uvalue=9223372036854775807
+  - r3.type=number
+  - r3.uvalue=0
+  - r3.svalue=0
+
+code:
+  <start>: |
+    r0 s>>= r3
+    if r1 == r0 goto <one>
+    r2 = 0
+    exit
+  <one>: |
+    r2 = 1
+    exit
+
+post:
+  - r0.svalue=9223372036854775807
+  - r0.svalue=r1.svalue
+  - r0.type=number
+  - r0.uvalue=9223372036854775807
+  - r0.uvalue=r1.uvalue
+  - r1.svalue=9223372036854775807
+  - r1.type=number
+  - r1.uvalue=9223372036854775807
+  - r2.svalue=1
+  - r2.type=number
+  - r2.uvalue=1
+  - r3.type=number
+  - r3.uvalue=0
+  - r3.svalue=0
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+
+---
+test-case: check that signed right shift by 0 is idempotent - MAX_UINT64 - via register
+
+pre:
+  - r0.type=number
+  - r0.svalue=-1
+  - r0.uvalue=18446744073709551615
+  - r1.type=number
+  - r1.svalue=-1
+  - r1.uvalue=18446744073709551615
+  - r3.type=number
+  - r3.uvalue=0
+  - r3.svalue=0
+
+code:
+  <start>: |
+    r0 s>>= r3
+    if r1 == r0 goto <one>
+    r2 = 0
+    exit
+  <one>: |
+    r2 = 1
+    exit
+
+post:
+  - r0.svalue=-1
+  - r0.svalue=r1.svalue
+  - r0.type=number
+  - r0.uvalue=18446744073709551615
+  - r0.uvalue=r1.uvalue
+  - r1.svalue=-1
+  - r1.type=number
+  - r1.uvalue=18446744073709551615
+  - r2.svalue=1
+  - r2.type=number
+  - r2.uvalue=1
+  - r3.type=number
+  - r3.uvalue=0
+  - r3.svalue=0
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+
+---
+test-case: check that left shift by 0 is idempotent - MIN_INT64
+
+pre:
+  - r0.type=number
+  - r0.svalue=-9223372036854775808
+  - r0.uvalue=9223372036854775808
+  - r1.type=number
+  - r1.svalue=-9223372036854775808
+  - r1.uvalue=9223372036854775808
+
+code:
+  <start>: |
+    r0 <<= 0
+    if r1 == r0 goto <one>
+    r2 = 0
+    exit
+  <one>: |
+    r2 = 1
+    exit
+
+post:
+  - r0.type=number
+  - r0.svalue=-9223372036854775808
+  - r0.uvalue=9223372036854775808
+  - r1.type=number
+  - r1.svalue=-9223372036854775808
+  - r1.uvalue=9223372036854775808
+  - r0.svalue=r1.svalue
+  - r0.uvalue=r1.uvalue
+  - r2.svalue=1
+  - r2.type=number
+  - r2.uvalue=1
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+
+---
+test-case: check that left shift by 0 is idempotent - MAX_INT64
+
+pre:
+  - r0.type=number
+  - r0.svalue=9223372036854775807
+  - r0.uvalue=9223372036854775807
+  - r1.type=number
+  - r1.svalue=9223372036854775807
+  - r1.uvalue=9223372036854775807
+
+code:
+  <start>: |
+    r0 <<= 0
+    if r1 == r0 goto <one>
+    r2 = 0
+    exit
+  <one>: |
+    r2 = 1
+    exit
+
+post:
+  - r0.svalue=9223372036854775807
+  - r0.svalue=r1.svalue
+  - r0.type=number
+  - r0.uvalue=9223372036854775807
+  - r0.uvalue=r1.uvalue
+  - r1.svalue=9223372036854775807
+  - r1.type=number
+  - r1.uvalue=9223372036854775807
+  - r2.svalue=1
+  - r2.type=number
+  - r2.uvalue=1
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+
+---
+test-case: check that left shift by 0 is idempotent - MIN_INT64 - via register
+
+pre:
+  - r0.type=number
+  - r0.svalue=-9223372036854775808
+  - r0.uvalue=9223372036854775808
+  - r1.type=number
+  - r1.svalue=-9223372036854775808
+  - r1.uvalue=9223372036854775808
+  - r3.type=number
+  - r3.uvalue=0
+  - r3.svalue=0
+
+code:
+  <start>: |
+    r0 <<= r3
+    if r1 == r0 goto <one>
+    r2 = 0
+    exit
+  <one>: |
+    r2 = 1
+    exit
+
+post:
+  - r0.type=number
+  - r0.svalue=-9223372036854775808
+  - r0.uvalue=9223372036854775808
+  - r1.type=number
+  - r1.svalue=-9223372036854775808
+  - r1.uvalue=9223372036854775808
+  - r0.svalue=r1.svalue
+  - r0.uvalue=r1.uvalue
+  - r2.svalue=1
+  - r2.type=number
+  - r2.uvalue=1
+  - r3.type=number
+  - r3.uvalue=0
+  - r3.svalue=0
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+
+---
+test-case: check that left shift by 0 is idempotent - MAX_INT64 - via register
+
+pre:
+  - r0.type=number
+  - r0.svalue=9223372036854775807
+  - r0.uvalue=9223372036854775807
+  - r1.type=number
+  - r1.svalue=9223372036854775807
+  - r1.uvalue=9223372036854775807
+  - r3.type=number
+  - r3.uvalue=0
+  - r3.svalue=0
+
+code:
+  <start>: |
+    r0 <<= r3
+    if r1 == r0 goto <one>
+    r2 = 0
+    exit
+  <one>: |
+    r2 = 1
+    exit
+
+post:
+  - r0.svalue=9223372036854775807
+  - r0.svalue=r1.svalue
+  - r0.type=number
+  - r0.uvalue=9223372036854775807
+  - r0.uvalue=r1.uvalue
+  - r1.svalue=9223372036854775807
+  - r1.type=number
+  - r1.uvalue=9223372036854775807
+  - r2.svalue=1
+  - r2.type=number
+  - r2.uvalue=1
+  - r3.type=number
+  - r3.uvalue=0
+  - r3.svalue=0
+
+messages:
+  - "1:2: Code is unreachable after 1:2"