fix(BV): Do not lose explanations in bvmul (OCamlPro#1170)

* fix(BV): Do not lose explanations in bvmul

The implementation of bvmul from OCamlPro#1144 introduced a soundness bug: when
we do not know anything about the result, the explanation is dropped.

This is because the implementation was performing mixing bitlist
computation and creation of raw bitlist values. This patch fixes the
implementation by performing all computations in [Z] and only adding the
explanation at the end.

* Add a test

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

tests/issues/1170.expected

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

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)