diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml
index 4eab14800a..9732eb51ef 100644
--- a/src/lib/reasoners/bitv.ml
+++ b/src/lib/reasoners/bitv.ml
@@ -250,15 +250,13 @@ module Shostak(X : ALIEN) = struct
     let other ~neg t sz ctx =
       let r, ctx' = X.make t in
       let ctx = List.rev_append ctx' ctx in
-      match X.extract r with
-      | Some bv ->
-        if neg then
-          try negate_abstract bv, ctx with
-          | Failure _ ->
-            [ { bv = Other (X.term_embed (E.BV.bvnot t)); sz } ], ctx
-        else
-          bv, ctx
-      | None -> [ { bv = Other r; sz } ], ctx
+      let bv = embed r in
+      if neg then
+        try negate_abstract bv, ctx with
+        | Failure _ ->
+          [ { bv = Other (X.term_embed (E.BV.bvnot t)); sz } ], ctx
+      else
+        bv, ctx
 
     let extract_st i j ({ bv; sz } as st) =
       match bv with
diff --git a/tests/bitv/testfile-bvnot-term.dolmen.expected b/tests/bitv/testfile-bvnot-term.dolmen.expected
new file mode 100644
index 0000000000..a6e005255c
--- /dev/null
+++ b/tests/bitv/testfile-bvnot-term.dolmen.expected
@@ -0,0 +1,2 @@
+
+unknown
diff --git a/tests/bitv/testfile-bvnot-term.dolmen.smt2 b/tests/bitv/testfile-bvnot-term.dolmen.smt2
new file mode 100644
index 0000000000..fe478a5775
--- /dev/null
+++ b/tests/bitv/testfile-bvnot-term.dolmen.smt2
@@ -0,0 +1,7 @@
+(set-logic BV)
+
+(declare-const x (_ BitVec 4))
+(declare-const y (_ BitVec 4))
+(assert (= x (bvnot y)))
+(assert (distinct y x))
+(check-sat)
diff --git a/tests/dune.inc b/tests/dune.inc
index a73f233788..b94a3f7f24 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -123314,6 +123314,28 @@
       (diff
         testfile-bvnot.dolmen.expected
         testfile-bvnot.dolmen_dolmen.output)))
+  (rule
+   (target testfile-bvnot-term.dolmen_dolmen.output)
+   (deps (:input testfile-bvnot-term.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-bvnot-term.dolmen.expected
+        testfile-bvnot-term.dolmen_dolmen.output)))
   (rule
    (target testfile-bitv023_ci_cdcl_no_minimal_bj.output)
    (deps (:input testfile-bitv023.ae))