diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml
index d437765334..7e2abceb9f 100644
--- a/src/lib/reasoners/bitv.ml
+++ b/src/lib/reasoners/bitv.ml
@@ -213,6 +213,8 @@ module Shostak(X : ALIEN) = struct
         { descr = Vextract (t', i, j); size }
       | { f = Op BVnot; xs = [ t ]; ty = Tbitv size; _ } ->
         { descr = Vnot t; size }
+      | { f = Op BVZeroExtend n; xs = [ t ]; ty = Tbitv size; _ } when n = 0 ->
+        { descr = Vother t; size }
       | { f = Op BVZeroExtend n; xs = [ t ]; ty = Tbitv size; _ } when n > 0 ->
         { descr = Vconcat (E.BV.bvzero n, t); size = n + size }
       | { ty = Tbitv size; _ } ->
diff --git a/tests/dune.inc b/tests/dune.inc
index b94a3f7f24..a866b0ac78 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -123292,6 +123292,26 @@
 
 ; Auto-generated part begin
 (subdir bitv
+  (rule
+   (target testfile-bvze.dolmen_dolmen.output)
+   (deps (:input testfile-bvze.dolmen.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff testfile-bvze.dolmen.expected testfile-bvze.dolmen_dolmen.output)))
   (rule
    (target testfile-bvnot.dolmen_dolmen.output)
    (deps (:input testfile-bvnot.dolmen.smt2))