diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml
index 968ed2337d..2b1c2d7b31 100644
--- a/src/lib/reasoners/bitv.ml
+++ b/src/lib/reasoners/bitv.ml
@@ -921,11 +921,15 @@ module Shostak(X : ALIEN) = struct
 
     (* [assoc_var v sub] is the same as [assoc_var_id] but takes a variable.
 
-       Requires: [v] is an unconstrained root variable.
+
+       Requires: [v] is an unconstrainted root variable or a constant.
+       Raises: [Not_found] if [v] is not in the substitution, or if [v] is a
+         constant.
        Requires: the variables in [sub] are unconstrained root variables. *)
     let assoc_var v sub =
       match v.bv.defn with
       | Droot { id; _ } -> assoc_var_id id sub
+      | Dcte _ -> raise Not_found
       | _ -> (* Can only substitute [Droot] variables *) assert false
 
     (* This is a helper function for [slice_vars].
diff --git a/tests/bitv/testfile-bitv027.expected b/tests/bitv/testfile-bitv027.expected
new file mode 100644
index 0000000000..a6e005255c
--- /dev/null
+++ b/tests/bitv/testfile-bitv027.expected
@@ -0,0 +1,2 @@
+
+unknown
diff --git a/tests/bitv/testfile-bitv027.smt2 b/tests/bitv/testfile-bitv027.smt2
new file mode 100644
index 0000000000..d84e292c9d
--- /dev/null
+++ b/tests/bitv/testfile-bitv027.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_BV)
+(declare-const x (_ BitVec 8))
+(declare-const y (_ BitVec 8))
+; This used to crash
+(assert (= (concat #b00000000 (concat x (concat ((_ extract 6 5) x) ((_ extract 3 1) x)))) (concat y (concat y (concat #b00 ((_ extract 6 4) x)))
+)))
+(check-sat)
diff --git a/tests/dune.inc b/tests/dune.inc
index 4204abd93c..6c5a651a44 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-bitv027_ci_cdcl_no_minimal_bj.output)
+   (deps (:input testfile-bitv027.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-bitv027_ci_cdcl_no_minimal_bj.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv027.expected testfile-bitv027_ci_cdcl_no_minimal_bj.output)))
+  (rule
+   (target testfile-bitv027_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input testfile-bitv027.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-bitv027_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv027.expected testfile-bitv027_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target testfile-bitv027_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input testfile-bitv027.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-bitv027_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv027.expected testfile-bitv027_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target testfile-bitv027_ci_no_tableaux_cdcl_in_instantiation.output)
+   (deps (:input testfile-bitv027.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-bitv027_ci_no_tableaux_cdcl_in_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv027.expected testfile-bitv027_ci_no_tableaux_cdcl_in_instantiation.output)))
+  (rule
+   (target testfile-bitv027_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+   (deps (:input testfile-bitv027.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-bitv027_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv027.expected testfile-bitv027_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+  (rule
+   (target testfile-bitv027_ci_tableaux_cdcl_no_minimal_bj.output)
+   (deps (:input testfile-bitv027.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-bitv027_ci_tableaux_cdcl_no_minimal_bj.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv027.expected testfile-bitv027_ci_tableaux_cdcl_no_minimal_bj.output)))
+  (rule
+   (target testfile-bitv027_cdcl.output)
+   (deps (:input testfile-bitv027.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-bitv027_cdcl.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv027.expected testfile-bitv027_cdcl.output)))
+  (rule
+   (target testfile-bitv027_tableaux_cdcl.output)
+   (deps (:input testfile-bitv027.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-bitv027_tableaux_cdcl.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv027.expected testfile-bitv027_tableaux_cdcl.output)))
+  (rule
+   (target testfile-bitv027_tableaux.output)
+   (deps (:input testfile-bitv027.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-bitv027_tableaux.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv027.expected testfile-bitv027_tableaux.output)))
+  (rule
+   (target testfile-bitv027_dolmen.output)
+   (deps (:input testfile-bitv027.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-bitv027_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv027.expected testfile-bitv027_dolmen.output)))
+  (rule
+   (target testfile-bitv027_fpa.output)
+   (deps (:input testfile-bitv027.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-bitv027_fpa.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-bitv027.expected testfile-bitv027_fpa.output)))
   (rule
    (target testfile-bitv026_ci_cdcl_no_minimal_bj.output)
    (deps (:input testfile-bitv026.smt2))