Fix machine words again

1 files changed, 4 insertions, 5 deletions

diff --git a/src/toFromInterp_lib_mword.ml b/src/toFromInterp_lib_mword.ml
index 928a56a0..21d3a38c 100644
--- a/src/toFromInterp_lib_mword.ml
+++ b/src/toFromInterp_lib_mword.ml
@@ -116,12 +116,12 @@ let bitToInterpValue = zbitToInterpValue
 let zbitvectorFromInterpValue typq_'n typq_'ord v = match v with
   | V_vector vs ->
      assert (Big_int.of_int (List.length vs) = typq_'n);
-     List.map bitFromInterpValue vs
-  | _ -> failwith "invalid interpreter value for vector"
+     Lem.wordFromBitlist (List.map (fun b -> bitFromInterpValue b |> Sail_lib.bool_of_bit) vs)
+  | _ -> failwith "invalid interpreter value for bitvector"
 
 let zbitvectorToInterpValue typq_'n typq_'ord v =
-  assert (Big_int.of_int (List.length v) = typq_'n);
-  V_vector (List.map bitToInterpValue v)
+  let bs = Lem.bitlistFromWord v in
+  V_vector (List.map (fun b -> Sail_lib.bit_of_bool b |> bitToInterpValue) bs)
 
 let bitvectorFromInterpValue = zbitvectorFromInterpValue
 let bitvectorToInterpValue = zbitvectorToInterpValue
@@ -135,7 +135,6 @@ let optionToInterpValue typq_'a v = match v with
   | None -> V_ctor ("None", [(unitToInterpValue ())])
   | Some (v0) -> V_ctor ("Some", [(typq_'a v0)])
 
-
 let bitsFromInterpValue v = match v with
   | V_vector vs ->
      Lem.wordFromBitlist (List.map (fun b -> bitFromInterpValue b |> Sail_lib.bool_of_bit) vs)