diff --git a/src/lib/reasoners/bitlist.ml b/src/lib/reasoners/bitlist.ml
index 0d346257c..a663b106f 100644
--- a/src/lib/reasoners/bitlist.ml
+++ b/src/lib/reasoners/bitlist.ml
@@ -321,20 +321,19 @@ let mul a b =
     let low_a_known = Z.trailing_zeros @@ a.bits_unk in
     let low_b_known = Z.trailing_zeros @@ b.bits_unk in
     let low_known = min low_a_known low_b_known in
-    let mid_bits = exact Z.(value a * value b) ex in
+    let mid_bits = Z.(value a * value b) in
     let mid_bits =
       if low_known = max_int then mid_bits
-      else extract mid_bits 0 low_known
+      else if low_known = 0 then Z.zero
+      else Z.extract mid_bits 0 low_known
     in
     if low_known = max_int then
-      mid_bits lsl zeroes
+      exact Z.(mid_bits lsl zeroes) ex
     else
-      let high_bits =
-        { bits_set = Z.zero
-        ; bits_unk = Z.minus_one
-        ; ex = Ex.empty }
-      in
-      ((high_bits lsl low_known) lor mid_bits) lsl zeroes
+      (* High bits are unknown *)
+      { bits_set = Z.(mid_bits lsl zeroes)
+      ; bits_unk = Z.(minus_one lsl Stdlib.(low_known + zeroes))
+      ; ex }
 
 let bvshl ~size:sz a b =
   (* If the minimum value for [b] is larger than the bitwidth, the result is
diff --git a/tests/dune.inc b/tests/dune.inc
index fdb2e10f5..46f4bec79 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -180418,6 +180418,255 @@
      (package alt-ergo)
       (action
        (diff 340.expected 340_fpa.output)))
+  (rule
+   (target 1170_ci_cdcl_no_minimal_bj.output)
+   (deps (:input 1170.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 1170_ci_cdcl_no_minimal_bj.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff 1170.expected 1170_ci_cdcl_no_minimal_bj.output)))
+  (rule
+   (target 1170_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input 1170.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 1170_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff 1170.expected 1170_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target 1170_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input 1170.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 1170_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff 1170.expected 1170_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target 1170_ci_no_tableaux_cdcl_in_instantiation.output)
+   (deps (:input 1170.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 1170_ci_no_tableaux_cdcl_in_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff 1170.expected 1170_ci_no_tableaux_cdcl_in_instantiation.output)))
+  (rule
+   (target 1170_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+   (deps (:input 1170.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 1170_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff 1170.expected 1170_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+  (rule
+   (target 1170_ci_tableaux_cdcl_no_minimal_bj.output)
+   (deps (:input 1170.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 1170_ci_tableaux_cdcl_no_minimal_bj.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff 1170.expected 1170_ci_tableaux_cdcl_no_minimal_bj.output)))
+  (rule
+   (target 1170_cdcl.output)
+   (deps (:input 1170.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 1170_cdcl.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 1170.expected 1170_cdcl.output)))
+  (rule
+   (target 1170_tableaux_cdcl.output)
+   (deps (:input 1170.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 1170_tableaux_cdcl.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 1170.expected 1170_tableaux_cdcl.output)))
+  (rule
+   (target 1170_tableaux.output)
+   (deps (:input 1170.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 1170_tableaux.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 1170.expected 1170_tableaux.output)))
+  (rule
+   (target 1170_dolmen.output)
+   (deps (:input 1170.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 1170_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 1170.expected 1170_dolmen.output)))
+  (rule
+   (target 1170_fpa.output)
+   (deps (:input 1170.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 1170_fpa.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 1170.expected 1170_fpa.output)))
   (rule
    (target 1163.models_dolmen.output)
    (deps (:input 1163.models.smt2))
diff --git a/tests/issues/1170.expected b/tests/issues/1170.expected
new file mode 100644
index 000000000..a6e005255
--- /dev/null
+++ b/tests/issues/1170.expected
@@ -0,0 +1,2 @@
+
+unknown
diff --git a/tests/issues/1170.smt2 b/tests/issues/1170.smt2
new file mode 100644
index 000000000..94ab438f8
--- /dev/null
+++ b/tests/issues/1170.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_BV)
+(declare-const A (_ BitVec 2))
+(declare-const B (_ BitVec 1))
+(declare-const C (_ BitVec 3))
+(assert (= (bvmul (_ bv3 4) (concat A (concat #b0 B))) (concat C #b1)))
+(check-sat)