add support for Bv of size 16

Author: redianthus

src/smtml/bitvector.ml

@@ -17,6 +17,10 @@ let of_int8 v =
   (* TODO: add a check on v to make sure it is not too big ? *)
   make (Z.of_int v) 8
 
+let of_int16 v =
+  (* TODO: add a check on v to make sure it is not too big ? *)
+  make (Z.of_int v) 16
+
 let of_int32 v = make (Z.of_int32 v) 32
 
 let of_int64 v = make (Z.of_int64 v) 64

src/smtml/bitvector.mli

@@ -4,6 +4,8 @@ val make : Z.t -> int -> t
 
 val of_int8 : int -> t
 
+val of_int16 : int -> t
+
 val of_int32 : Int32.t -> t
 
 val of_int64 : Int64.t -> t

src/smtml/mappings.ml

@@ -813,6 +813,9 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty_bitv 8 ->
         let i8 = M.Interp.to_bitv v 8 in
         Value.Bitv (Bitvector.of_int8 (Int64.to_int i8))
+      | Ty_bitv 16 ->
+        let i16 = M.Interp.to_bitv v 16 in
+        Value.Bitv (Bitvector.of_int16 (Int64.to_int i16))
       | Ty_bitv 32 ->
         let i32 = M.Interp.to_bitv v 32 in
         Value.Bitv (Bitvector.of_int32 (Int64.to_int32 i32))