diff --git a/soteria-c/test/cram/fixme.t/run.t b/soteria-c/test/cram/fixme.t/run.t
index 229dd08d6..a967efa74 100644
--- a/soteria-c/test/cram/fixme.t/run.t
+++ b/soteria-c/test/cram/fixme.t/run.t
@@ -6,8 +6,8 @@
       raw =
       { args = []; pre = [];
         pc =
-        [(0x0000000000000000 != V|1|); (0x0000000000000000 != V|2|);
-          (V|1| == V|2|)];
+        [(V|1| == V|2|); (0x0000000000000000 != V|1|);
+          (0x0000000000000000 != V|2|)];
         post =
         { heap =
           [(V|2|,
diff --git a/soteria-c/test/cram/simple_bi.t/run.t b/soteria-c/test/cram/simple_bi.t/run.t
index 9477bb36c..76de7c33d 100644
--- a/soteria-c/test/cram/simple_bi.t/run.t
+++ b/soteria-c/test/cram/simple_bi.t/run.t
@@ -23,7 +23,7 @@
                info = None })];
            globs = [] }
           ];
-        pc = [(0x0000000000000000 != V|1|); (V|2| <=u 0x7ffffffffffffffb)];
+        pc = [(V|2| <=u 0x7ffffffffffffffb); (0x0000000000000000 != V|1|)];
         post =
         { heap =
           [(V|1|,
@@ -122,7 +122,7 @@ NO_COLOR=true is necessary to avoid test output changing in CI. For some reason,
                info = None })];
            globs = [] }
           ];
-        pc = [(0x0000000000000000 != V|1|); (V|2| <=u 0x7ffffffffffffffb)];
+        pc = [(V|2| <=u 0x7ffffffffffffffb); (0x0000000000000000 != V|1|)];
         post =
         { heap =
           [(V|1|,
@@ -254,8 +254,8 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
            globs = [] }
           ];
         pc =
-        [(0x0000000000000000 != V|2|); (0x00000001 <=u V|1|);
-          (V|1| <=u 0x7fffffff); (V|3| <=u 0x7ffffffffffffffb)];
+        [(0x00000001 <=u V|1|); (V|1| <=u 0x7fffffff);
+          (V|3| <=u 0x7ffffffffffffffb); (0x0000000000000000 != V|2|)];
         post =
         { heap =
           [(V|2|,
@@ -308,8 +308,8 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
            globs = [] }
           ];
         pc =
-        [(0x0000000000000000 != V|1|); (V|3| == 0x00000001);
-          (V|2| <=u 0x7ffffffffffffffb); (V|3| == 0x00000001)];
+        [(V|3| == 0x00000001); (V|2| <=u 0x7ffffffffffffffb);
+          (V|3| == 0x00000001); (0x0000000000000000 != V|1|)];
         post =
         { heap =
           [(V|1|,
@@ -340,12 +340,9 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
             globs = [] }
           ];
         pc =
-        [(0x0000000000000000 != V|1|);
-          (0x0000000000000000 <=s (V|2| + 0x0000000000000004));
-          ((V|4| <s 0x00000000) != ((V|4| + V|5|) <s 0x00000000));
-          ((V|4| <s 0x00000000) == (V|5| <s 0x00000000));
-          (V|2| <=u 0x7ffffffffffffff7); (0x00000002 <=u V|3|);
-          (V|3| <=u 0x7fffffff)];
+        [(V|4| +s_ovf V|5|); (V|2| <=u 0x7ffffffffffffff7);
+          (0x00000002 <=u V|3|); (V|3| <=u 0x7fffffff);
+          (0x0000000000000000 != V|1|)];
         post =
         { heap =
           [(V|1|,
@@ -381,11 +378,9 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
             globs = [] }
           ];
         pc =
-        [(0x0000000000000000 != V|1|);
-          (0x0000000000000000 <=s (V|2| + 0x0000000000000004));
-          (((V|4| <s 0x00000000) == ((V|4| + V|5|) <s 0x00000000)) || ((V|4| <s 0x00000000) != (V|5| <s 0x00000000)));
-          (V|3| == 0x00000002); (V|2| <=u 0x7ffffffffffffff7);
-          (V|3| == 0x00000002)];
+        [!((V|4| +s_ovf V|5|)); (V|3| == 0x00000002);
+          (V|2| <=u 0x7ffffffffffffff7); (V|3| == 0x00000002);
+          (0x0000000000000000 != V|1|)];
         post =
         { heap =
           [(V|1|,
@@ -408,10 +403,7 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
   Summaries for add_561:
     Analysed {
       raw =
-      { args = [V|1|; V|2|]; pre = [];
-        pc =
-        [((V|1| <s 0x00000000) != ((V|1| + V|2|) <s 0x00000000));
-          ((V|1| <s 0x00000000) == (V|2| <s 0x00000000))];
+      { args = [V|1|; V|2|]; pre = []; pc = [(V|1| +s_ovf V|2|)];
         post = { heap = []; globs = [] };
         ret =
         (Error (Integer overflow,
@@ -420,10 +412,7 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
       manifest_bugs = []}
     Analysed {
       raw =
-      { args = [V|1|; V|2|]; pre = [];
-        pc =
-        [(((V|1| <s 0x00000000) == ((V|1| + V|2|) <s 0x00000000)) || ((V|1| <s 0x00000000) != (V|2| <s 0x00000000)))
-          ];
+      { args = [V|1|; V|2|]; pre = []; pc = [!((V|1| +s_ovf V|2|))];
         post = { heap = []; globs = [] }; ret = (Ok (V|1| +ck V|2|)) };
       manifest_bugs = []}
   
diff --git a/soteria-rust/lib/sptr.ml b/soteria-rust/lib/sptr.ml
index 6e2a3f573..25601bea9 100644
--- a/soteria-rust/lib/sptr.ml
+++ b/soteria-rust/lib/sptr.ml
@@ -78,7 +78,7 @@ module DecayMap : DecayMapS = struct
                   Rustsymex.assume
                     [
                       (addr %@ align ==@ Usize.(0s));
-                      Usize.(0s) <@ addr;
+                      align <=@ addr;
                       addr <@ Typed.BitVec.usize isize_max -!@ size;
                     ]
                 in
diff --git a/soteria-rust/test/cram/kani.t/run.t b/soteria-rust/test/cram/kani.t/run.t
index 41df9cf96..831905018 100644
--- a/soteria-rust/test/cram/kani.t/run.t
+++ b/soteria-rust/test/cram/kani.t/run.t
@@ -97,70 +97,70 @@ Test kani::vec::any_vec
   Compiling... done in <time>
   note: len_capacity_invariant: done in <time>, ran 17 branches
   PC 1: (extract[0-1](V|18|) == 0b00) /\ (0x0000000000000000 == V|1|) /\
-        (0x0000000000000000 == V|1|) /\ (0x0000000000000001 <=u V|18|) /\
+        (0x0000000000000000 == V|1|) /\ (0x0000000000000004 <=u V|18|) /\
         (V|18| <=u 0x7fffffffffffffbe)
   PC 2: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x000000000000000f) /\
         (0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x000000000000000f) /\
-        (0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
-        (0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffc2)
+        (0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
+        (0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffc2)
   PC 3: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x000000000000000e) /\
         (0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x000000000000000e) /\
-        (0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
-        (0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffc6)
+        (0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
+        (0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffc6)
   PC 4: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x000000000000000d) /\
         (0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x000000000000000d) /\
-        (0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
-        (0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffca)
+        (0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
+        (0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffca)
   PC 5: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x000000000000000c) /\
         (0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x000000000000000c) /\
-        (0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
-        (0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffce)
+        (0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
+        (0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffce)
   PC 6: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x000000000000000b) /\
         (0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x000000000000000b) /\
-        (0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
-        (0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffd2)
+        (0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
+        (0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffd2)
   PC 7: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x000000000000000a) /\
         (0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x000000000000000a) /\
-        (0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
-        (0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffd6)
+        (0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
+        (0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffd6)
   PC 8: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x0000000000000009) /\
         (0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x0000000000000009) /\
-        (0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
-        (0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffda)
+        (0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
+        (0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffda)
   PC 9: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x0000000000000008) /\
         (0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x0000000000000008) /\
-        (0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
-        (0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffde)
+        (0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
+        (0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffde)
   PC 10: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x0000000000000007) /\
          (0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x0000000000000007) /\
-         (0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
-         (0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffe2)
+         (0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
+         (0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffe2)
   PC 11: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x0000000000000006) /\
          (0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x0000000000000006) /\
-         (0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
-         (0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffe6)
+         (0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
+         (0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffe6)
   PC 12: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x0000000000000005) /\
          (0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x0000000000000005) /\
-         (0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
-         (0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffea)
+         (0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
+         (0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffea)
   PC 13: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x0000000000000004) /\
          (0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x0000000000000004) /\
-         (0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
-         (0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffee)
+         (0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
+         (0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffee)
   PC 14: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x0000000000000003) /\
          (0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x0000000000000003) /\
-         (0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
-         (0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7ffffffffffffff2)
+         (0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
+         (0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7ffffffffffffff2)
   PC 15: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x0000000000000002) /\
          (0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x0000000000000002) /\
-         (0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
-         (0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7ffffffffffffff6)
+         (0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
+         (0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7ffffffffffffff6)
   PC 16: (extract[0-1](V|18|) == 0b00) /\ (0x0000000000000001 == V|1|) /\
          (0b00 == extract[0-1](V|19|)) /\ (0x0000000000000001 == V|1|) /\
-         (0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
-         (0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7ffffffffffffffa)
+         (0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
+         (0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7ffffffffffffffa)
   PC 17: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x0000000000000010) /\
-         (V|1| == 0x0000000000000010) /\ (0x0000000000000001 <=u V|18|) /\
+         (V|1| == 0x0000000000000010) /\ (0x0000000000000004 <=u V|18|) /\
          (V|18| <=u 0x7fffffffffffffbe)
   
 Test our simple Kani demo works
@@ -175,11 +175,10 @@ Test our simple Kani demo works
    10 │      let b: u32 = kani::any();
    11 │      if a + b < u32::MAX {
       │          ^^^^^ Triggering memory operation
-  PC 1: (((0xffffffff -ck V|1|) <u V|2|) || ((0xffffffff -ck V|2|) <u V|1|))
+  PC 1: (V|1| +u_ovf V|2|)
   
   note: saturating_add: done in <time>, ran 2 branches
-  PC 1: (V|1| <u (0xffffffff -ck V|2|)) /\ (V|1| <=u (0xffffffff -ck V|2|)) /\
-        (V|2| <=u (0xffffffff -ck V|1|))
+  PC 1: (V|1| <u (0xffffffff -ck V|2|)) /\ !((V|1| +u_ovf V|2|))
   PC 2: ((0xffffffff -ck V|2|) <=u V|1|)
   
   error: memory_leak: found issues in <time>, errors in 1 branch (out of 1)
@@ -190,7 +189,7 @@ Test our simple Kani demo works
       │   │
       │   Leaking function
       │   1: Entry point
-  PC 1: (extract[0-1](V|1|) == 0b00) /\ (0x0000000000000001 <=u V|1|) /\
+  PC 1: (extract[0-1](V|1|) == 0b00) /\ (0x0000000000000004 <=u V|1|) /\
         (V|1| <=u 0x7ffffffffffffffa)
   
   error: uninit_access: found issues in <time>, errors in 1 branch (out of 2)
diff --git a/soteria-rust/test/cram/simple.t/run.t b/soteria-rust/test/cram/simple.t/run.t
index 4a0113e0e..3f60b065c 100644
--- a/soteria-rust/test/cram/simple.t/run.t
+++ b/soteria-rust/test/cram/simple.t/run.t
@@ -9,7 +9,7 @@ Test memory leaks
       │   │
       │   Leaking function
       │   1: Entry point
-  PC 1: (extract[0-1](V|1|) == 0b00) /\ (0x0000000000000001 <=u V|1|) /\
+  PC 1: (extract[0-1](V|1|) == 0b00) /\ (0x0000000000000004 <=u V|1|) /\
         (V|1| <=u 0x7ffffffffffffffa)
   
   [1]
@@ -57,9 +57,9 @@ Test that we properly handle the niche optimisation
   Compiling... done in <time>
   note: main: done in <time>, ran 1 branch
   PC 1: (extract[0-1](V|1|) == 0b00) /\ (0b00 == extract[0-1](V|2|)) /\
-        (0b00 == extract[0-1](V|3|)) /\ (0x0000000000000001 <=u V|1|) /\
-        (V|1| <=u 0x7ffffffffffffffa) /\ (0x0000000000000001 <=u V|2|) /\
-        (V|2| <=u 0x7ffffffffffffff6) /\ (0x0000000000000001 <=u V|3|) /\
+        (0b00 == extract[0-1](V|3|)) /\ (0x0000000000000004 <=u V|1|) /\
+        (V|1| <=u 0x7ffffffffffffffa) /\ (0x0000000000000004 <=u V|2|) /\
+        (V|2| <=u 0x7ffffffffffffff6) /\ (0x0000000000000004 <=u V|3|) /\
         (V|3| <=u 0x7ffffffffffffffa)
   
 Test function calls on function pointers
diff --git a/soteria/lib/bv_values/analyses.ml b/soteria/lib/bv_values/analyses.ml
index 83eec600e..302e8f5ae 100644
--- a/soteria/lib/bv_values/analyses.ml
+++ b/soteria/lib/bv_values/analyses.ml
@@ -16,6 +16,10 @@ module type S = sig
       data. *)
   val add_constraint : t -> Svalue.t -> Svalue.t * Var.Set.t
 
+  (** Filters the given iterator of symbolic values, keeping only those relevant
+      to the given variable according to the analysis. *)
+  val filter : t -> Var.t -> Svalue.ty -> Svalue.t Iter.t -> Svalue.t Iter.t
+
   (** Encode all the information relevant to the given variables and conjuncts
       them with the given accumulator. *)
   val encode : ?vars:Var.Hashset.t -> t -> Typed.sbool Typed.t Iter.t
@@ -45,6 +49,9 @@ module Merge (A1 : S) (A2 : S) : S = struct
     let v'', vars2 = A2.add_constraint a2 v' in
     (v'', Var.Set.union vars1 vars2)
 
+  let filter (a1, a2) var ty vs =
+    vs |> A1.filter a1 var ty |> A2.filter a2 var ty
+
   let encode ?vars (a1, a2) : Typed.sbool Typed.t Iter.t =
     Iter.append (A1.encode ?vars a1) (A2.encode ?vars a2)
 end
@@ -58,6 +65,7 @@ module None : S = struct
   let reset () = ()
   let simplify () v = v
   let add_constraint () v = (v, Var.Set.empty)
+  let filter () _ _ vs = vs
   let encode ?vars:_ () = Iter.empty
 end
 
@@ -87,9 +95,6 @@ module Interval : S = struct
 
   type sign = Pos | Neg
 
-  (** Sign multiplication *)
-  let ( ** ) l r = if l = r then Pos else Neg
-
   let pp_sign fmt = function
     | Pos -> Fmt.string fmt "+"
     | Neg -> Fmt.string fmt "-"
@@ -404,7 +409,8 @@ module Interval : S = struct
        a disjunction! *)
     | Unop (Not, v) ->
         Option.map
-          (fun (v1, size, (sign, range)) -> (v1, size, (Neg ** sign, range)))
+          (fun (v1, size, (sign, range)) ->
+            (v1, size, ((if sign = Neg then Pos else Neg), range)))
           (as_range v)
     | _ -> None
 
@@ -486,8 +492,35 @@ module Interval : S = struct
     else log (fun m -> m "No change.@.");
     ((v' &&@ learnt, vars), st')
 
+  let filter var ty vs st =
+    match ty with
+    | Svalue.TBitVector n -> (
+        let range_opt = Var.Map.find_opt var st in
+        match range_opt with
+        | None -> vs
+        | Some range ->
+            (* In sparsely populated ranges (e.g. [0, 1000] - [1, 999]), filtering
+               can be very slow since the odds of getting a valid integer is so low.
+               Because of this, we reset the iterator and generate values ourselves. *)
+            let l, h = range.Data.pos in
+            let rec iter z f =
+              f (Svalue.BitVec.mk n z);
+              (* if a negative range exists, update to next value *)
+              let z = Z.succ z in
+              let neg =
+                List.find_opt
+                  (fun (m, n) -> Z.Compare.(m <= z && z <= n))
+                  range.Data.negs
+              in
+              let z' = match neg with None -> z | Some (_, n) -> Z.succ n in
+              if Z.Compare.(z' <= h) then iter z' f
+            in
+            iter l)
+    | _ -> vs
+
   let simplify st v = wrap_read (simplify v) st
   let add_constraint st v = wrap (add_constraint v) st
+  let filter st var ty vs = wrap_read (filter var ty vs) st
 
   let encode ?vars st : Typed.sbool Typed.t Iter.t =
     let to_check =
@@ -594,20 +627,203 @@ module Equality : S = struct
     in
     Eval.eval ~eval_var:(eval_var st) v |> simplify ~fuel:3
 
+  let add_vars v s =
+    Svalue.iter_vars v |> Iter.fold (fun s (v, _) -> Var.Set.add v s) s
+
   let add_constraint (v : Svalue.t) st =
     match v.node.kind with
     | Binop (Eq, v1, v2) ->
+        let vars = Var.Set.empty |> add_vars v1 |> add_vars v2 in
         let v1, st = get_or_make v1 st in
         let v2, st = get_or_make v2 st in
         merge v1 v2 st;
-        (* Here we choose to pass down the equality (rather than simplifying to true),
-           so that the underlying solver can do trivial SAT checks using these equalities.
-           This also means this analysis is exempt from implementing [encode], since it
-           doesn't store anything. *)
-        ((v, Var.Set.empty), st)
+        ((Svalue.Bool.v_true, vars), st)
+    | Unop (Not, { node = { kind = Nop (Distinct, hd :: tl); _ }; _ }) ->
+        let vars = add_vars hd Var.Set.empty in
+        let v1, st = get_or_make hd st in
+        let rec aux vars st = function
+          | [] -> (vars, st)
+          | v2 :: rest ->
+              let vars = add_vars v2 vars in
+              let v2, st = get_or_make v2 st in
+              merge v1 v2 st;
+              aux vars st rest
+        in
+        let vars, st = aux vars st tl in
+        ((Svalue.Bool.v_true, vars), st)
     | _ -> ((v, Var.Set.empty), st)
 
+  (** In equality analysis we can be certain of the value of a variable, so we
+      can entirely replace the set of possible values [vs] with the
+      representative value (if any). *)
+  let filter var ty vs st =
+    let v = Svalue.mk_var var ty in
+    match find_cheaper_opt v st with
+    | None -> vs
+    | Some v_repr -> Iter.singleton v_repr
+
+  let encode ?vars (uf, refs) =
+    let is_relevant =
+      match vars with
+      | None -> fun _ -> true
+      | Some vars ->
+          fun v ->
+            Svalue.iter_vars v
+            |> Iter.exists (fun (v, _) -> Var.Hashset.mem vars v)
+    in
+    fun f ->
+      refs
+      |> VMap.iter @@ fun v ufref ->
+         if is_relevant v then
+           let v_repr = UnionFind.get uf ufref in
+           if not (Svalue.equal v v_repr) then
+             f (Typed.sem_eq (Typed.type_ v) (Typed.type_ v_repr))
+
   let simplify st v = wrap_read (simplify v) st
   let add_constraint st v = wrap (add_constraint v) st
-  let encode ?vars:_ _st = Iter.empty
+  let filter st var ty vs = wrap_read (filter var ty vs) st
+  let encode ?vars st = wrap_read (encode ?vars) st
+end
+
+module Disjoint = struct
+  module VSet = Set.Make (Svalue)
+  module VMap = Map.Make (Svalue)
+
+  include Reversible.Make_mutable (struct
+    type t = VSet.t VMap.t
+
+    let default = VMap.empty
+  end)
+
+  let pp ft st =
+    Fmt.(
+      iter_bindings VMap.iter
+        (pair ~sep:(any " -> ") Svalue.pp (iter VSet.iter Svalue.pp)))
+      ft st
+
+  let[@inline] sort (v1 : Svalue.t) (v2 : Svalue.t) =
+    if v1.tag < v2.tag then (v1, v2) else (v2, v1)
+
+  let var_set v =
+    Svalue.iter_vars v
+    |> Iter.map fst
+    |> Iter.fold (fun set x -> Var.Set.add x set) Var.Set.empty
+
+  let[@inline] is_relevant : Svalue.t -> bool = function
+    | { node = { ty = TLoc _; _ }; _ }
+    | { node = { kind = BitVec _ | Var _; _ }; _ } ->
+        true
+    | _ -> false
+
+  let[@inline] ineq_matters : Svalue.t -> bool = function
+    | { node = { kind = Var _; ty = TLoc _ }; _ } -> false
+    | _ -> true
+
+  (** Adds inequalities between all values in [vs] to the state [st], returning
+      the updated state along with the set of variables that are dirty (i.e.
+      something was learnt from this). *)
+  let add_inequalities vs st =
+    let dirty = ref VSet.empty in
+    let dirty_v v = if ineq_matters v then dirty := VSet.add v !dirty in
+    let vs = List.sort_uniq (fun v1 v2 -> Int.compare v1.Hc.tag v2.Hc.tag) vs in
+    let rec aux st = function
+      | [] | [ _ ] -> st
+      | v1 :: rest ->
+          let st =
+            VMap.update v1
+              (fun s ->
+                let s = Option.value s ~default:VSet.empty in
+                let s, is_new' =
+                  List.fold_left
+                    (fun (s, is_new) v2 ->
+                      assert (v1.Hc.tag < v2.Hc.tag);
+                      if VSet.mem v2 s then (s, is_new)
+                      else (
+                        dirty_v v2;
+                        (VSet.add v2 s, true)))
+                    (s, false) rest
+                in
+                if is_new' then dirty_v v1;
+                Some s)
+              st
+          in
+          aux st rest
+    in
+    let st = aux st vs in
+    let dirty =
+      VSet.fold (fun v -> Var.Set.union (var_set v)) !dirty Var.Set.empty
+    in
+    (dirty, st)
+
+  let add_constraint (v : Svalue.t) st =
+    match v.node.kind with
+    | Unop (Not, { node = { kind = Binop (Eq, l, r); _ }; _ })
+      when is_relevant l && is_relevant r ->
+        let l, r = sort l r in
+        let vars, st = add_inequalities [ l; r ] st in
+        ((Svalue.Bool.v_true, vars), st)
+    | Nop (Distinct, vs) when List.hd vs |> is_relevant ->
+        let vars, st = add_inequalities vs st in
+        ((Svalue.Bool.v_true, vars), st)
+    | _ -> ((v, Var.Set.empty), st)
+
+  let sure_neq l r st =
+    let l, r = sort l r in
+    match VMap.find_opt l st with None -> false | Some s -> VSet.mem r s
+
+  let simplify (v : Svalue.t) st =
+    match v.node.kind with
+    | Binop (Eq, l, r) when is_relevant l && is_relevant r && sure_neq l r st ->
+        Svalue.Bool.v_false
+    | Unop (Not, { node = { kind = Binop (Eq, l, r); _ }; _ })
+      when is_relevant l && is_relevant r && sure_neq l r st ->
+        Svalue.Bool.v_true
+    | Nop (Distinct, vs) ->
+        let cross_product = List.to_seq vs |> Seq.self_cross_product in
+        let rec aux seq =
+          match seq () with
+          | Seq.Nil -> Svalue.Bool.v_true
+          | Seq.Cons ((l, r), rest) when sure_neq l r st -> aux rest
+          | _ -> v
+        in
+        aux cross_product
+    | _ -> v
+
+  let filter v ty st =
+    let v1 = Svalue.mk_var v ty in
+    Iter.filter (fun v2 ->
+        let v1, v2 = sort v1 v2 in
+        match VMap.find_opt v1 st with
+        | None -> true
+        | Some s -> not (VSet.mem v2 s))
+
+  let simplify st v = wrap_read (simplify v) st
+  let add_constraint st v = wrap (add_constraint v) st
+  let filter st var ty = wrap_read (filter var ty) st
+  let mk_var n v = Typed.mk_var v (Typed.t_int n)
+  let uneq l r = Typed.not (Typed.sem_eq (Typed.type_ l) (Typed.type_ r))
+
+  let encode ?vars st : Typed.sbool Typed.t Iter.t =
+    let to_check, ineq_matters =
+      match vars with
+      | Some vars -> (Var.Hashset.mem vars, ineq_matters)
+      | None -> ((fun _ -> true), fun _ -> true)
+    in
+    let to_check v =
+      Iter.exists to_check (Svalue.iter_vars v |> Iter.map fst)
+    in
+    wrap_read
+      (fun m f ->
+        VMap.iter
+          (fun v s ->
+            if to_check v then
+              VSet.iter
+                (fun v2 -> if ineq_matters v2 || to_check v2 then f (uneq v v2))
+                s
+            else
+              VSet.iter
+                (fun v2 -> if ineq_matters v2 && to_check v2 then f (uneq v v2))
+                s)
+          m)
+      st
 end
diff --git a/soteria/lib/bv_values/bv_solver.ml b/soteria/lib/bv_values/bv_solver.ml
index 363cf04a0..413de903f 100644
--- a/soteria/lib/bv_values/bv_solver.ml
+++ b/soteria/lib/bv_values/bv_solver.ml
@@ -368,45 +368,9 @@ struct
       (to_encode, var_set)
   end
 
-  module Declared_vars = struct
-    module Var_counter = Var.Incr_counter_mut (struct
-      let start_at = 1
-    end)
-
-    (* Since we start addresses at one to improve trivial model hits, we need to offset to obtain an index. *)
-    let var_to_index v = Var.to_int v - 1
-
-    type t = {
-      counter : Var_counter.t;
-      types : Svalue.ty Dynarray.t;
-          (** The var_counter is keeping track of how many variables we actually
-              have in the context. We don't need to separate each bit of that
-              array by saved branch, we just fetch at the index for each
-              variable, and override when we change branch. *)
-    }
-
-    let init () = { counter = Var_counter.init (); types = Dynarray.create () }
-    let save t = Var_counter.save t.counter
-    let backtrack_n t n = Var_counter.backtrack_n t.counter n
-    let reset t = Var_counter.reset t.counter
-
-    let fresh t ty =
-      let next = Var_counter.get_next t.counter in
-      let next_i = var_to_index next in
-      let () =
-        if Dynarray.length t.types == next_i then Dynarray.add_last t.types ty
-        else if Dynarray.length t.types > next_i then
-          Dynarray.set t.types next_i ty
-        else failwith "Broke var-counter/declared-types invariant"
-      in
-      next
-
-    let get_ty t var = Dynarray.get t.types (var_to_index var)
-  end
-
   type t = {
     z3_exe : Intf.t;
-    vars : Declared_vars.t;
+    vars : Var_counter.t;
     save_counter : Save_counter.t;
     state : Solver_state.t;
     analysis : Analysis.t;
@@ -418,19 +382,19 @@ struct
     {
       z3_exe;
       save_counter = Save_counter.init ();
-      vars = Declared_vars.init ();
+      vars = Var_counter.init ();
       state = Solver_state.init ();
       analysis = Analysis.init ();
     }
 
   let save solver =
-    Declared_vars.save solver.vars;
+    Var_counter.save solver.vars;
     Save_counter.save solver.save_counter;
     Solver_state.save solver.state;
     Analysis.save solver.analysis
 
   let backtrack_n solver n =
-    Declared_vars.backtrack_n solver.vars n;
+    Var_counter.backtrack_n solver.vars n;
     Solver_state.backtrack_n solver.state n;
     Save_counter.backtrack_n solver.save_counter n;
     Analysis.backtrack_n solver.analysis n
@@ -442,12 +406,11 @@ struct
     let save_counter = !(solver.save_counter) in
     if save_counter < 0 then failwith "Solver reset: save_counter < 0???";
     Save_counter.reset solver.save_counter;
-    Declared_vars.reset solver.vars;
+    Var_counter.reset solver.vars;
     Solver_state.reset solver.state;
     Analysis.reset solver.analysis
 
-  let fresh_var solver ty =
-    Declared_vars.fresh solver.vars (Typed.untype_type ty)
+  let fresh_var solver _ = Var_counter.get_next solver.vars
 
   let simplify solver v : 'a Typed.t =
     v
@@ -469,59 +432,76 @@ struct
   let memo_sat_check_tbl : Symex.Solver_result.t Hashtbl.Hint.t =
     Hashtbl.Hint.create 1023
 
-  let trivial_model_works to_check =
-    (* We try a trivial model where replacing each variable with name
-    [|n|] with the corresponding integer [n]; except if an assertion
-    [|n| == v] exists, in which case we replace it with the value [v].
-    If the constraint evaluates to true, then it is satisfiable. *)
-    let v_eqs = Var.Hashtbl.create 8 in
-    Svalue.Bool.split_ands to_check (fun v ->
-        match v.node.kind with
-        | Binop
-            ( Eq,
-              { node = { kind = Var n; _ }; _ },
-              ({ node = { kind = BitVec _; _ }; _ } as x) )
-        | Binop
-            ( Eq,
-              ({ node = { kind = BitVec _; _ }; _ } as x),
-              { node = { kind = Var n; _ }; _ } ) ->
-            Var.Hashtbl.add v_eqs n x
-        | _ -> ());
-    let eval_var v_var v (ty : Svalue.ty) =
-      match ty with
-      | TBitVector n | TLoc n -> (
-          let i = Var.to_int v in
-          try Var.Hashtbl.find v_eqs v
-          with Not_found -> Svalue.BitVec.mk_masked n (Z.of_int i))
-      | _ -> v_var
+  let trivial_model_works solver to_check var_tys =
+    let exception No_model in
+    let value_generator : Svalue.ty -> unit -> Svalue.t = function
+      | TLoc n ->
+          let max = Z.(shift_left one n) in
+          fun () -> Svalue.Ptr.loc_of_z n (Z.random_int max)
+      | TBitVector n ->
+          let max = Z.(shift_left one n) in
+          fun () -> Svalue.BitVec.mk n (Z.random_int max)
+      | TBool -> fun () -> Svalue.Bool.bool (Random.bool ())
+      (* TODO: because we can't evaluate floats, we can never do a
+         trivial check for them. *)
+      | TFloat _ -> raise No_model
+      (* TODO: figure this out *)
+      | TPointer _ | TSeq _ -> raise No_model
     in
-    let res = Eval.eval ~eval_var to_check in
-    Svalue.equal res Svalue.Bool.v_true
+    let fuel = 3 in
+    try
+      let bindings =
+        Var.Map.fold
+          (fun v (ty : Svalue.ty) acc ->
+            let values =
+              Iter.forever (value_generator ty)
+              |> Analysis.filter solver.analysis v ty
+              |> Iter.take fuel
+              |> Iter.to_array
+            in
+            if Array.length values = 0 then raise No_model;
+            Var.Map.add v values acc)
+          var_tys Var.Map.empty
+      in
+      let rec aux i =
+        let rec eval_var _ v _ =
+          let values = Var.Map.find v bindings in
+          let index = i mod Array.length values in
+          match values.(index) with
+          | { node = { kind = Var var; ty }; _ } as v -> eval_var v var ty
+          | v -> v
+        in
+        let res = Eval.eval ~eval_var to_check in
+        if Svalue.equal res Svalue.Bool.v_true then true
+        else if i >= fuel then false
+        else aux (i + 1)
+      in
+      aux 0
+    with No_model -> false
 
-  let check_sat_raw solver relevant_vars to_check =
+  let check_sat_raw solver to_check =
     (* TODO: we shouldn't wait for ack for each command individually... *)
-    if trivial_model_works to_check then Symex.Solver_result.Sat
+    let var_tys =
+      Svalue.iter_vars to_check
+      |> Iter.fold (fun acc (v, ty) -> Var.Map.add v ty acc) Var.Map.empty
+    in
+    if trivial_model_works solver to_check var_tys then Symex.Solver_result.Sat
     else (
       (* We need to reset the state, so we can push the new constraints *)
       Intf.reset solver.z3_exe;
-
       (* Declare all relevant variables *)
-      Var.Hashset.iter
-        (fun v ->
-          let ty = Declared_vars.get_ty solver.vars v in
-          Intf.declare_var solver.z3_exe v ty)
-        relevant_vars;
+      Var.Map.iter (Intf.declare_var solver.z3_exe) var_tys;
       (* Declare the constraint *)
       Intf.add_constraint solver.z3_exe to_check;
       (* Actually check sat *)
       Intf.check_sat solver.z3_exe)
 
-  let check_sat_raw_memo solver relevant_vars to_check =
+  let check_sat_raw_memo solver to_check =
     let to_check = Typed.untyped to_check in
     match Hashtbl.Hint.find_opt memo_sat_check_tbl to_check.Hc.tag with
     | Some result -> result
     | None ->
-        let result = check_sat_raw solver relevant_vars to_check in
+        let result = check_sat_raw solver to_check in
         Hashtbl.Hint.add memo_sat_check_tbl to_check.Hc.tag result;
         result
 
@@ -539,7 +519,7 @@ struct
           Iter.fold Typed.and_ to_check
             (Analysis.encode ~vars:relevant_vars solver.analysis)
         in
-        let answer = check_sat_raw_memo solver relevant_vars to_check in
+        let answer = check_sat_raw_memo solver to_check in
         if answer = Sat then Solver_state.mark_checked solver.state;
         answer
 
@@ -550,8 +530,8 @@ struct
     |> Iter.to_list
 end
 
+open Analyses
+module Analysis = Merge (Merge (Interval) (Equality)) (Disjoint)
 module Z3 = Solvers.Z3.Make (Encoding)
-module Z3_incremental_solver = Make_incremental (Analyses.None) (Z3)
-
-module Z3_solver =
-  Make (Analyses.Merge (Analyses.Interval) (Analyses.Equality)) (Z3)
+module Z3_incremental_solver = Make_incremental (Analysis) (Z3)
+module Z3_solver = Make (Analysis) (Z3)
diff --git a/soteria/lib/bv_values/encoding.ml b/soteria/lib/bv_values/encoding.ml
index 679a3f67a..90fcd1b49 100644
--- a/soteria/lib/bv_values/encoding.ml
+++ b/soteria/lib/bv_values/encoding.ml
@@ -82,6 +82,8 @@ let smt_of_binop : Svalue.Binop.t -> sexp -> sexp -> sexp = function
   | Rem true -> bv_srem
   | Rem false -> bv_urem
   | Mod -> bv_smod
+  | AddOvf true -> bv_saddo
+  | AddOvf false -> bv_uaddo
   | MulOvf true -> bv_smulo
   | MulOvf false -> bv_umulo
   | Lt true -> bv_slt
diff --git a/soteria/lib/bv_values/eval.ml b/soteria/lib/bv_values/eval.ml
index 8d7003c1c..e83c05d88 100644
--- a/soteria/lib/bv_values/eval.ml
+++ b/soteria/lib/bv_values/eval.ml
@@ -19,6 +19,7 @@ let eval_binop : Binop.t -> t -> t -> t = function
   | Div signed -> BitVec.div ~signed
   | Rem signed -> BitVec.rem ~signed
   | Mod -> BitVec.mod_
+  | AddOvf signed -> BitVec.add_overflows ~signed
   | MulOvf signed -> BitVec.mul_overflows ~signed
   | Lt signed -> BitVec.lt ~signed
   | Leq signed -> BitVec.leq ~signed
diff --git a/soteria/lib/bv_values/svalue.ml b/soteria/lib/bv_values/svalue.ml
index 4ca99b63e..965f03f26 100644
--- a/soteria/lib/bv_values/svalue.ml
+++ b/soteria/lib/bv_values/svalue.ml
@@ -140,6 +140,7 @@ module Binop = struct
     | Div of bool (* signed *)
     | Rem of bool (* signed *)
     | Mod
+    | AddOvf of bool (* signed *)
     | MulOvf of bool (* signed *)
     | Lt of bool (* signed *)
     | Leq of bool (* signed *)
@@ -174,6 +175,7 @@ module Binop = struct
     | Div s -> Fmt.pf ft "/%a" pp_signed s
     | Rem s -> Fmt.pf ft "rem%a" pp_signed s
     | Mod -> Fmt.string ft "mod"
+    | AddOvf s -> Fmt.pf ft "+%a_ovf" pp_signed s
     | MulOvf s -> Fmt.pf ft "*%a_ovf" pp_signed s
     | Lt s -> Fmt.pf ft "<%a" pp_signed s
     | Leq s -> Fmt.pf ft "<=%a" pp_signed s
@@ -308,6 +310,14 @@ let mk_var v ty = Var v <| ty
 let mk_commut_binop op l r =
   if l.tag <= r.tag then Binop (op, l, r) else Binop (op, r, l)
 
+(** We put commutative n-ary operators in some sort of normal form where
+    elements are sorted by ud, to increase cache hits. If [idem] is true, will
+    also remove duplicates. *)
+let mk_commut_nop ?(idem = true) op vs =
+  let sort = if idem then List.sort_uniq else List.sort in
+  let vs = sort (fun l r -> Int.compare l.tag r.tag) vs in
+  Nop (op, vs)
+
 (* TODO: substitution will break normal forms. *)
 let rec subst subst_var sv =
   match sv.node.kind with
@@ -537,6 +547,7 @@ module rec Bool : Bool = struct
       | Binop (Eq, { node = { kind = BitVec bv; ty = TBitVector 1 }; _ }, v)
       | Binop (Eq, v, { node = { kind = BitVec bv; ty = TBitVector 1 }; _ }) ->
           sem_eq (BitVec.mk 1 Z.(one - bv)) v
+      | Nop (Distinct, [ l; r ]) -> sem_eq l r
       | _ -> Unop (Not, sv) <| TBool
 
   and ite guard if_ else_ =
@@ -686,7 +697,7 @@ module rec Bool : Bool = struct
     | _ when is_bv v1.node.ty && is_bv v2.node.ty ->
         let current_size = size_of v1.node.ty in
         let msb = max (BitVec.msb_of v1) (BitVec.msb_of v2) in
-        if 0 < msb && msb < current_size - 1 then
+        if 0 <= msb && msb < current_size - 1 then
           let v1' = BitVec.extract 0 msb v1 in
           let v2' = BitVec.extract 0 msb v2 in
           sem_eq v1' v2'
@@ -717,12 +728,21 @@ module rec Bool : Bool = struct
     (* [Distinct l] when l is empty or of size 1 is always true *)
     match l with
     | [] | [ _ ] -> v_true
-    | l ->
+    | l -> (
         let cross_product = List.to_seq l |> Seq.self_cross_product in
-        let sure_distinct =
-          Seq.for_all (fun (a, b) -> sure_neq a b) cross_product
+        let rec aux seq =
+          match seq () with
+          | Seq.Nil -> Some true
+          | Seq.Cons ((a, b), rest) ->
+              if equal a b then Some false
+              else if sure_neq a b then aux rest
+              else None
         in
-        if sure_distinct then v_true else Nop (Distinct, l) <| TBool
+        let res = aux cross_product in
+        match res with
+        | Some true -> v_true
+        | Some false -> v_false
+        | None -> mk_commut_nop Distinct l <| TBool)
 end
 
 (** {2 Bit vectors} *)
@@ -773,8 +793,8 @@ and BitVec : BitVec = struct
 
   let rec msb_of v =
     match v.node.kind with
-    | BitVec v when Z.(v > zero) -> Z.log2 v
-    | BitVec v when Z.(equal v zero) -> 0
+    | BitVec z when Z.(z > zero) -> Z.log2 z
+    | BitVec z when Z.(equal z zero) -> size_of v.node.ty - 1
     | Binop (BitAnd, bv1, bv2) -> min (msb_of bv1) (msb_of bv2)
     | Ite (_, l, r) -> max (msb_of l) (msb_of r)
     | Unop (BvExtend (false, __), v) -> msb_of v
@@ -1166,12 +1186,11 @@ and BitVec : BitVec = struct
     assert (extend_by > 0);
     match v.node.kind with
     | BitVec bv ->
-        if signed && Z.testbit bv (n - 1) then
+        if signed then
           (* Sign extend: replicate the MSB *)
-          let mask = Z.(pred (one lsl extend_by) lsl n) in
-          mk to_ Z.(bv lor mask)
+          mk_masked to_ (Z.signed_extract bv 0 n)
         else
-          (* Zero extend: just mask to ensure no extra bits *)
+          (* Zero extend: do nothing *)
           mk to_ bv
     | Ite (b, l, r) ->
         let l = extend ~signed extend_by l in
@@ -1246,7 +1265,9 @@ and BitVec : BitVec = struct
 
   and ashr v1 v2 =
     match (v1.node.kind, v2.node.kind) with
-    | BitVec l, BitVec r -> mk_masked (size_of v1.node.ty) Z.(l asr to_int r)
+    | BitVec l, BitVec r ->
+        let n = size_of v1.node.ty in
+        mk_masked n Z.(Z.signed_extract l 0 n asr to_int r)
     | _, BitVec s when Z.equal s Z.zero -> v1
     | Binop (AShr, v, { node = { kind = BitVec s1; _ }; _ }), BitVec s2 ->
         let n = size_of v1.node.ty in
@@ -1279,6 +1300,7 @@ and BitVec : BitVec = struct
     | _ -> mk_commut_binop (Mul { checked }) v1 v2 <| v1.node.ty
 
   let rec div ~signed v1 v2 =
+    assert (equal_ty v1.node.ty v2.node.ty);
     match (v1.node.kind, v2.node.kind) with
     | BitVec l, BitVec r ->
         let size = size_of v1.node.ty in
@@ -1315,6 +1337,11 @@ and BitVec : BitVec = struct
       ->
         (* (x / n) / d = x / (n * d) (if n * d doesn't overflow) *)
         div ~signed x (mk (size_of v1.node.ty) Z.(n * d))
+    | Unop (BvExtend (false, by), x), BitVec z
+      when Stdlib.not signed && msb_of v2 < size_of x.node.ty ->
+        (* extend[uN](X) / N when msb(N) < size(X) <=> extend[uN](X / N) *)
+        let v2 = mk (size_of x.node.ty) z in
+        extend ~signed:false by (div ~signed x v2)
     | _ -> Binop (Div signed, v1, v2) <| v1.node.ty
 
   let rec lt ~signed v1 v2 =
@@ -1702,14 +1729,24 @@ and BitVec : BitVec = struct
     | _, BitVec z when Z.equal z Z.zero -> Bool.v_false
     | BitVec z, _ when Stdlib.not signed ->
         let n = size_of v1.node.ty in
-        let z = bv_to_z signed n z in
         let m = max_for signed n in
-        gt ~signed v2 (mk_masked n Z.(m - z))
+        gt ~signed v2 (mk n Z.(m - z))
     | _, BitVec z when Stdlib.not signed ->
         let n = size_of v1.node.ty in
-        let z = bv_to_z signed n z in
         let m = max_for signed n in
-        gt ~signed v1 (mk_masked n Z.(m - z))
+        gt ~signed v1 (mk n Z.(m - z))
+    | (BitVec z, x | x, BitVec z) when signed ->
+        let x = if x == v1.node.kind then v1 else v2 in
+        let n = size_of v1.node.ty in
+        let z = bv_to_z signed n z in
+        if Z.gt z Z.zero then
+          (* z > 0 so overflows if  max - z < x *)
+          let max = max_for signed n in
+          gt ~signed x (mk n (Z.sub max z))
+        else
+          (* z < 0 so overflows if x < min - z *)
+          let min = min_for signed n in
+          lt ~signed x (mk_masked n (Z.sub min z))
     | Unop (BvOfBool _, _), Unop (BvOfBool _, _) -> Bool.v_false
     | Unop (BvOfBool _, b), other | other, Unop (BvOfBool _, b) ->
         (* ite(b, 1, 0) + x only overflows if b && x == max *)
@@ -1717,22 +1754,7 @@ and BitVec : BitVec = struct
         let max = max_for signed n in
         let other = other <| t_bv n in
         Bool.and_ b (Bool.sem_eq other (mk n max))
-    | _ ->
-        let size = size_of v1.node.ty in
-        if signed then
-          let sign_of v = lt ~signed v (zero size) in
-          let sign_l = sign_of v1 in
-          let sign_r = sign_of v2 in
-          let msb_res = sign_of (add v1 v2) in
-          Bool.and_
-            (Bool.sem_eq sign_l sign_r)
-            (Bool.not (Bool.sem_eq sign_l msb_res))
-        else
-          let max = max_for signed size in
-          let max = mk size max in
-          Bool.or_
-            (gt ~signed v1 (sub ~checked:true max v2))
-            (gt ~signed v2 (sub ~checked:true max v1))
+    | _ -> mk_commut_binop (AddOvf signed) v1 v2 <| TBool
 
   let mul_overflows ~signed v1 v2 =
     match (v1.node.kind, v2.node.kind) with
@@ -1781,7 +1803,7 @@ and BitVec : BitVec = struct
             let maxn = Z.pred (Z.shift_left Z.one n) in
             let bound = Z.(maxn / z) in
             gt ~signed (x <| v1.node.ty) (mk n bound)
-    | _ -> Binop (MulOvf signed, v1, v2) <| TBool
+    | _ -> mk_commut_binop (MulOvf signed) v1 v2 <| TBool
 
   let neg_overflows v =
     let n = size_of v.node.ty in