diff --git a/CHANGES.md b/CHANGES.md
index 4bfc11ec..eefda965 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,7 +1,12 @@
 ## Unreleased
 
 ### Added
+
 ### Fixed
+
+- Fixes incorrect type calculation of bitv `*_extend` ops
+- Bumps bitwuzla 0.4.0 -> 0.6.0 to fix segmentation faults
+
 ### Changed
 
 ## v0.3.0
diff --git a/smtml.opam b/smtml.opam
index de0eb7b0..7b555581 100644
--- a/smtml.opam
+++ b/smtml.opam
@@ -68,7 +68,7 @@ available: arch != "arm32" & arch != "x86_32"
 pin-depends: [
   ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#1feba887bbb7980f27bbcec8137eb908caa8f0ce"]
   ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#1feba887bbb7980f27bbcec8137eb908caa8f0ce"]
-  ["alt-ergo-lib.dev" "git+https://github.com/OCamlPro/alt-ergo.git#7ee96296a5de9588a4d585b3b8abec35f4755425"]
+  ["alt-ergo-lib.2.6.0" "git+https://github.com/OCamlPro/alt-ergo.git#7ee96296a5de9588a4d585b3b8abec35f4755425"]
   ["cvc5.dev" "git+https://github.com/formalsec/ocaml-cvc5.git#b7aade52d49a19d646036d7e6aac09039c3e95cf"]
   ["benchpress.dev" "git+https://github.com/filipeom/benchpress.git#50355de32835b12f1b065a4700f493bc3d8c5342"]
 ]
diff --git a/smtml.opam.template b/smtml.opam.template
index 0c3ff732..e5fbd6a6 100644
--- a/smtml.opam.template
+++ b/smtml.opam.template
@@ -2,7 +2,7 @@ available: arch != "arm32" & arch != "x86_32"
 pin-depends: [
   ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#1feba887bbb7980f27bbcec8137eb908caa8f0ce"]
   ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#1feba887bbb7980f27bbcec8137eb908caa8f0ce"]
-  ["alt-ergo-lib.dev" "git+https://github.com/OCamlPro/alt-ergo.git#7ee96296a5de9588a4d585b3b8abec35f4755425"]
+  ["alt-ergo-lib.2.6.0" "git+https://github.com/OCamlPro/alt-ergo.git#7ee96296a5de9588a4d585b3b8abec35f4755425"]
   ["cvc5.dev" "git+https://github.com/formalsec/ocaml-cvc5.git#b7aade52d49a19d646036d7e6aac09039c3e95cf"]
   ["benchpress.dev" "git+https://github.com/filipeom/benchpress.git#50355de32835b12f1b065a4700f493bc3d8c5342"]
 ]
diff --git a/src/ast/expr.ml b/src/ast/expr.ml
index 67c9d368..f4519cb9 100644
--- a/src/ast/expr.ml
+++ b/src/ast/expr.ml
@@ -133,7 +133,8 @@ let rec ty (hte : t) : Ty.t =
     ty1
   | Triop (ty, _, _, _, _) -> ty
   | Relop (ty, _, _, _) -> ty
-  | Cvtop (Ty_bitv n, (Zero_extend m | Sign_extend m), _) -> Ty_bitv (n + m)
+  | Cvtop (_, (Zero_extend m | Sign_extend m), hte) -> (
+    match ty hte with Ty_bitv n -> Ty_bitv (n + m) | _ -> assert false )
   | Cvtop (ty, _, _) -> ty
   | Naryop (ty, _, _) -> ty
   | Extract (_, h, l) -> Ty_bitv ((h - l) * 8)
diff --git a/test/unit/dune b/test/unit/dune
index fadc38a4..0ef40dec 100644
--- a/test/unit/dune
+++ b/test/unit/dune
@@ -5,6 +5,7 @@
   test_unop
   test_binop
   test_triop
+  test_ty
   test_relop
   test_cvtop
   test_naryop
diff --git a/test/unit/test_ty.ml b/test/unit/test_ty.ml
new file mode 100644
index 00000000..210c6e88
--- /dev/null
+++ b/test/unit/test_ty.ml
@@ -0,0 +1,8 @@
+open Smtml
+
+let () =
+  let x = Expr.symbol (Symbol.make (Ty_bitv 32) "x") in
+  let x = Expr.extract x ~high:2 ~low:0 in
+  assert (Ty.equal (Expr.ty x) (Ty_bitv 16));
+  let x = Expr.cvtop (Ty_bitv 32) (Sign_extend 16) x in
+  assert (Ty.equal (Expr.ty x) (Ty_bitv 32))