diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml
index 54821c23f..07d254876 100644
--- a/src/lib/reasoners/bitv.ml
+++ b/src/lib/reasoners/bitv.ml
@@ -1324,24 +1324,26 @@ module Shostak(X : ALIEN) = struct
       let maybe_negate t =
         if negated then E.Ints.(~$$Z.(~$1 lsl sz - ~$1) - t) else t
       in
-      begin match E.term_view t with
-        | { f = Op Int2BV _; _ } ->
-          (* bv2nat will simplify: we must call [X.make] again *)
-          E.BV.bv2nat t |> maybe_negate |> X.make
-        | { ty = Tbitv n; _ } ->
-          assert (n = sz);
-          if negated then
-            (* if we are negated, we will simplify *)
-            E.BV.bv2nat t |> maybe_negate |> X.make
-          else
-            (* bv2nat will *not* simplify: become uninterpreted with interval
-               information *)
-            let t = E.BV.bv2nat t |> maybe_negate in
-            X.term_embed t,
-            [ E.Ints.(~$0 <= t) ; E.Ints.(t < ~$$Z.(~$1 lsl n)) ]
-        | { ty; _ } ->
-          Util.internal_error "expected bitv, got %a" Ty.print ty
-      end
+      let t', ctx =
+        begin match E.term_view t with
+          | { f = Op Int2BV _; _ } ->
+            (* bv2nat will simplify: we must call [X.make] again *)
+            E.BV.bv2nat t |> maybe_negate, []
+          | { ty = Tbitv n; _ } ->
+            assert (n = sz);
+            if negated then
+              (* if we are negated, we will simplify *)
+              E.BV.bv2nat t |> maybe_negate, []
+            else
+              (* bv2nat will *not* simplify: become uninterpreted with interval
+                 information *)
+              let t = E.BV.bv2nat t |> maybe_negate in
+              t, [ E.Ints.(~$0 <= t) ; E.Ints.(t < ~$$Z.(~$1 lsl n)) ]
+          | { ty; _ } ->
+            Util.internal_error "expected bitv, got %a" Ty.print ty
+        end
+      in
+      X.term_embed ot, E.Core.eq ot t' :: ctx
     | _ ->
       (* Note: we can't just call [X.make] on the result of [abstract_to_nat]
          because [X.make] should only be called on subterms. If we do it, it
diff --git a/tests/bitv/testfile-bitv025.expected b/tests/bitv/testfile-bitv025.expected
new file mode 100644
index 000000000..a6e005255
--- /dev/null
+++ b/tests/bitv/testfile-bitv025.expected
@@ -0,0 +1,2 @@
+
+unknown
diff --git a/tests/bitv/testfile-bitv025.smt2 b/tests/bitv/testfile-bitv025.smt2
new file mode 100644
index 000000000..0463dfef1
--- /dev/null
+++ b/tests/bitv/testfile-bitv025.smt2
@@ -0,0 +1,5 @@
+(set-logic QF_BV)
+(declare-fun s () (_ BitVec 32))
+(declare-fun t () (_ BitVec 32))
+(assert (= (bvshl s (bvnot (bvmul s t))) (_ bv0 32)))
+(check-sat)
diff --git a/tests/dune.inc b/tests/dune.inc
index fbfb00957..dad2dd8b3 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -120886,6 +120886,255 @@
      (package alt-ergo)
       (action
        (diff testfile-bv2nat-delayed.dolmen.expected testfile-bv2nat-delayed.dolmen_dolmen.output)))
+  (rule
+   (target testfile-bitv025_ci_cdcl_no_minimal_bj.output)
+   (deps (:input testfile-bitv025.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL
+             --no-minimal-bj
+             %{input})))))))
+  (rule
+   (deps testfile-bitv025_ci_cdcl_no_minimal_bj.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv025.expected testfile-bitv025_ci_cdcl_no_minimal_bj.output)))
+  (rule
+   (target testfile-bitv025_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input testfile-bitv025.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-minimal-bj
+             --no-tableaux-cdcl-in-theories
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (deps testfile-bitv025_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv025.expected testfile-bitv025_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target testfile-bitv025_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input testfile-bitv025.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-theories
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (deps testfile-bitv025_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv025.expected testfile-bitv025_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target testfile-bitv025_ci_no_tableaux_cdcl_in_instantiation.output)
+   (deps (:input testfile-bitv025.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (deps testfile-bitv025_ci_no_tableaux_cdcl_in_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv025.expected testfile-bitv025_ci_no_tableaux_cdcl_in_instantiation.output)))
+  (rule
+   (target testfile-bitv025_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+   (deps (:input testfile-bitv025.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-theories
+             %{input})))))))
+  (rule
+   (deps testfile-bitv025_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv025.expected testfile-bitv025_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+  (rule
+   (target testfile-bitv025_ci_tableaux_cdcl_no_minimal_bj.output)
+   (deps (:input testfile-bitv025.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-minimal-bj
+             %{input})))))))
+  (rule
+   (deps testfile-bitv025_ci_tableaux_cdcl_no_minimal_bj.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv025.expected testfile-bitv025_ci_tableaux_cdcl_no_minimal_bj.output)))
+  (rule
+   (target testfile-bitv025_cdcl.output)
+   (deps (:input testfile-bitv025.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL
+             %{input})))))))
+  (rule
+   (deps testfile-bitv025_cdcl.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv025.expected testfile-bitv025_cdcl.output)))
+  (rule
+   (target testfile-bitv025_tableaux_cdcl.output)
+   (deps (:input testfile-bitv025.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver Tableaux-CDCL
+             %{input})))))))
+  (rule
+   (deps testfile-bitv025_tableaux_cdcl.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv025.expected testfile-bitv025_tableaux_cdcl.output)))
+  (rule
+   (target testfile-bitv025_tableaux.output)
+   (deps (:input testfile-bitv025.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver Tableaux
+             %{input})))))))
+  (rule
+   (deps testfile-bitv025_tableaux.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv025.expected testfile-bitv025_tableaux.output)))
+  (rule
+   (target testfile-bitv025_dolmen.output)
+   (deps (:input testfile-bitv025.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps testfile-bitv025_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv025.expected testfile-bitv025_dolmen.output)))
+  (rule
+   (target testfile-bitv025_fpa.output)
+   (deps (:input testfile-bitv025.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --enable-theories fpa
+             %{input})))))))
+  (rule
+   (deps testfile-bitv025_fpa.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv025.expected testfile-bitv025_fpa.output)))
   (rule
    (target testfile-bitv024_ci_cdcl_no_minimal_bj.output)
    (deps (:input testfile-bitv024.smt2))