diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml
index 66431a44b..e05e3c93f 100644
--- a/src/lib/reasoners/bitv.ml
+++ b/src/lib/reasoners/bitv.ml
@@ -355,6 +355,14 @@ let sign_extend n sts =
         (repeat n [ extract_st (sz - 1) (sz - 1) st ])
         (st :: sts)
 
+let zero_extend sz sts =
+  if sz < 0 then
+    Fmt.invalid_arg "zero_extend: got negative extension: %d" sz;
+  match sts with
+  | { bv = (Cte _ as bv) ; sz = sz' } :: sts' ->
+    { bv ; sz = sz + sz' } :: sts'
+  | _ -> { bv = Cte Z.zero ; sz } :: sts
+
 module type ALIEN = sig
   include Sig.X
   val embed : r abstract -> r
@@ -1322,8 +1330,17 @@ module Shostak(X : ALIEN) = struct
         let varsU = get_vars u in
         let varsV = get_vars v in
         if Compat.List.is_empty varsU && Compat.List.is_empty varsV
-        then raise Util.Unsolvable
-        else
+        then (
+          (* If either side is non-normalized (this is a bug!!), it would be
+             unsound to raise [Unsolvable] here. *)
+          Options.heavy_assert (fun () ->
+              not @@
+              equal_abstract X.equal
+                (Canon.normalize u) (Canon.normalize v)
+            );
+
+          raise Util.Unsolvable
+        ) else
           begin
             let st_sys = slice u v in
             if Options.get_debug_bitv () then
diff --git a/src/lib/reasoners/bitv.mli b/src/lib/reasoners/bitv.mli
index 77b68f080..aecf132a0 100644
--- a/src/lib/reasoners/bitv.mli
+++ b/src/lib/reasoners/bitv.mli
@@ -47,11 +47,14 @@ type 'a simple_term = ('a simple_term_aux) alpha_term
 
 type 'a abstract = 'a simple_term list
 
+val extract : int -> int -> int -> 'a abstract -> 'a abstract
 (** [extract size i j x] extracts [i..j] from a composition of size [size].
 
     An element of size [sz] at the head of the composition contains the bits
     [size - 1 .. size - sz] inclusive. *)
-val extract : int -> int -> int -> 'a abstract -> 'a abstract
+
+val zero_extend : int -> 'a abstract -> 'a abstract
+(** [zero_extract sz bv] adds [sz] zeros to the front (high bits) of [bv]. *)
 
 val lognot : 'a abstract -> 'a abstract
 
diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml
index bf1df3e07..0a1eec3ad 100644
--- a/src/lib/reasoners/bitv_rel.ml
+++ b/src/lib/reasoners/bitv_rel.ml
@@ -41,7 +41,7 @@ let bitwidth r =
 
 
 let const sz n =
-  Shostak.Bitv.is_mine [ { bv = Cte (Z.extract n 0 sz); sz } ]
+  Shostak.Bitv.is_mine @@ Bitv.int2bv_const sz n
 
 module BitvNormalForm = struct
   (** Normal form for bit-vector values.
@@ -167,19 +167,19 @@ module BV2Nat = struct
         Bitv.extract (bitwidth bv) ofs (ofs + len - 1) @@
         Shostak.Bitv.embed bv
 
-      let zero_extend sz r =
+      let zero_extend_to sz r =
         let r_sz = bitwidth r in
         if sz < r_sz then invalid_arg "zero_extend";
         if sz = r_sz then r
         else
           Shostak.Bitv.is_mine @@
-          { Bitv.bv = Bitv.Cte Z.zero ; sz = sz - r_sz } ::
+          Bitv.zero_extend (sz - r_sz) @@
           Shostak.Bitv.embed r
 
       let mkv_eq (r, ext) (r', ext') =
         let sz = max ext.len ext'.len in
         let r = extract r ext and r' = extract r' ext' in
-        Uf.LX.mkv_eq (zero_extend sz r) (zero_extend sz r')
+        Uf.LX.mkv_eq (zero_extend_to sz r) (zero_extend_to sz r')
     end
   end
 
@@ -391,9 +391,7 @@ module BV2Nat = struct
       let lit =
         Uf.LX.mkv_eq
           (T.BV.extract bv ext)
-          (Shostak.Bitv.is_mine [
-              { bv = Cte (Z.extract cte 0 ext.len) ; sz = ext.len }
-            ])
+          (const ext.len cte)
       in
       { t with eqs = (lit, ex) :: t.eqs }
     | None ->
@@ -503,7 +501,7 @@ module BV2Nat = struct
           (* bv_r is extension of bv' *)
           Uf.LX.mkv_eq
             bv_r
-            (T.BV.zero_extend sz @@ T.BV.extract bv' ext')
+            (T.BV.zero_extend_to sz @@ T.BV.extract bv' ext')
       in
       { t with eqs = (lit, Ex.union ex ex') :: t.eqs }
     | exception Not_found ->