fix(BV): Allow substituting constants

Substituting a constant should be a no-op (just like substituting a
variable that is not in the substitution). Somehow this case was missed
in the new version of `apply_sub`. It is fairly hard to trigger this
case however: it can only happen in `apply_subs`, and requires a
C-substitution to be created, which in turn requires a C-variable to be
split during B-variable slicing, and then the C-substitution must be
applied to an equation rooted in a distinct term that contains a
constant. This patch includes a test case where this happens.

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].

tests/bitv/testfile-bitv027.expected

@@ -0,0 +1,2 @@
+
+unknown

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)