diff --git a/benchmarks/BV/cegar2.sl b/benchmarks/BV/cegar2.sl
new file mode 100644
index 0000000..aac3326
--- /dev/null
+++ b/benchmarks/BV/cegar2.sl
@@ -0,0 +1,19 @@
+(set-logic BV)
+
+(synth-inv inv-f ((x (_ BitVec 32))(n (_ BitVec 32))(m (_ BitVec 32)))
+ )
+
+(define-fun pre-f ((x (_ BitVec 32))(n (_ BitVec 32))(m (_ BitVec 32))) Bool
+    (and (= x #x00000000) (= m #x00000000))
+)
+
+(define-fun trans-f ((x (_ BitVec 32))(n (_ BitVec 32))(m (_ BitVec 32))(x! (_ BitVec 32))(n! (_ BitVec 32))(m! (_ BitVec 32))) Bool
+    (or (and (and (and (bvult x n) (= x! (bvadd x #x00000001))) (= n! n)) (= m! m)) (and (and (and (bvult x n) (= x! (bvadd x #x00000001))) (= n! n)) (= m! x)))
+)
+
+(define-fun post-f ((x (_ BitVec 32))(n (_ BitVec 32))(m (_ BitVec 32))) Bool
+    (not (and (and (bvuge x n) (bvugt n #x00000000)) (or (bvule n m) (bvult m #x00000000))))
+)
+
+(inv-constraint inv-f pre-f trans-f post-f)
+(check-synth)
diff --git a/src/BitVecComponents.ml b/src/BitVecComponents.ml
new file mode 100644
index 0000000..fb5b640
--- /dev/null
+++ b/src/BitVecComponents.ml
@@ -0,0 +1,95 @@
+open Base
+open Exceptions
+open Expr
+
+let all = [
+    {
+      name = "bv-eq";
+      codomain = Type.BOOL;
+      domain = [Type.BITVEC (-1); Type.BITVEC (-1)];
+      is_argument_valid = (function
+                           | _ -> true);
+      evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] ->
+                    Value.Bool ((BitarrayExt.compare v1 v2) = 0));
+      to_string = (fun [@warning "-8"] [v1;v2] -> "(= " ^ v1 ^ " " ^ v2 ^ ")");
+      global_constraints = (fun _ -> []);
+    } ;
+    {
+      name = "bvnot";
+      codomain = Type.BITVEC (-1);
+      domain = [Type.BITVEC (-1)];
+      is_argument_valid = (function
+                             | _ -> true);
+      evaluate = (function [@warning "-8"] [Value.BitVec v] -> Value.BitVec (BitarrayExt.bvnot v));
+      to_string = (fun [@warning "-8"] [a] -> "(bvnot " ^ a ^ ")");
+      global_constraints = (fun _ -> []);
+    } ;
+    {
+      name = "bvult";
+      codomain = Type.BOOL;
+      domain = [Type.BITVEC (-1); Type.BITVEC (-1)];
+      is_argument_valid = (function
+                           | _ -> true);
+      evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] ->
+                    Value.Bool (BitarrayExt.bvult v1 v2));
+      to_string = (fun [@warning "-8"] [a ; b] -> "(bvult " ^ a ^ " " ^ b ^ ")");
+      global_constraints = (fun _ -> []);
+    } ;
+    {
+      name = "bvadd";
+      codomain = Type.BITVEC (-1);
+      domain = [Type.BITVEC (-1); Type.BITVEC (-1)];
+      is_argument_valid = (function
+                           | _ -> true);
+      evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] ->
+                    Value.BitVec (BitarrayExt.add v1 v2));
+      to_string = (fun [@warning "-8"] [a ; b] -> "(bvadd " ^ a ^ " " ^ b ^ ")");
+      global_constraints = (fun _ -> []);
+    } ;
+    {
+      name = "bvuge";
+      codomain = Type.BOOL;
+      domain = [Type.BITVEC (-1); Type.BITVEC (-1)];
+      is_argument_valid = (function
+                           | _ -> true);
+      evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] ->
+                    Value.Bool (BitarrayExt.bvuge v1 v2));
+      to_string = (fun [@warning "-8"] [a ; b] -> "(bvuge " ^ a ^ " " ^ b ^ ")");
+      global_constraints = (fun _ -> []);
+    } ;
+    {
+      name = "bvugt";
+      codomain = Type.BOOL;
+      domain = [Type.BITVEC (-1); Type.BITVEC (-1)];
+      is_argument_valid = (function
+                           | _ -> true);
+      evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] ->
+                    Value.Bool (BitarrayExt.bvugt v1 v2));
+      to_string = (fun [@warning "-8"] [a ; b] -> "(bvugt " ^ a ^ " " ^ b ^ ")");
+      global_constraints = (fun _ -> []);
+    } ;
+    {
+      name = "bvule";
+      codomain = Type.BOOL;
+      domain = [Type.BITVEC (-1); Type.BITVEC (-1)];
+      is_argument_valid = (function
+                           | _ -> true);
+      evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] ->
+                    Value.Bool (BitarrayExt.bvule v1 v2));
+      to_string = (fun [@warning "-8"] [a ; b] -> "(bvule " ^ a ^ " " ^ b ^ ")");
+      global_constraints = (fun _ -> []);
+    } ;
+    {
+      name = "bvsub";
+      codomain = Type.BITVEC (-1);
+      domain = [Type.BITVEC (-1); Type.BITVEC (-1)];
+      is_argument_valid = (function
+                           | _ -> true);
+      evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] ->
+                    Value.BitVec (BitarrayExt.bvsub v1 v2));
+      to_string = (fun [@warning "-8"] [a ; b] -> "(bvsub " ^ a ^ " " ^ b ^ ")");
+      global_constraints = (fun _ -> []);
+    }
+  ]
+
+let levels = [| all |]
\ No newline at end of file
diff --git a/src/Bitarray.ml b/src/Bitarray.ml
index b18b400..990a5a8 100644
--- a/src/Bitarray.ml
+++ b/src/Bitarray.ml
@@ -6,11 +6,10 @@
  *  - https://discuss.ocaml.org/t/ann-v0-12-release-of-jane-street-packages/3499/7
  *  - https://github.com/janestreet/core_extended/issues/22
  *)
-
 open Core
 
-(* a single 63 bit chunk of the array, bounds checking is left to the main module.
-   We can only use 62 bits, because of the sign bit *)
+(* a single 63 bit chunk of the array, bounds checking is left to the main module. We can
+   only use 62 bits, because of the sign bit *)
 module Int63_chunk : sig
   type t
 
@@ -23,34 +22,37 @@ end = struct
   type t = Int63.t
 
   let empty = zero
-
   let get t i = bit_and t (shift_left one i) > zero
 
   let set t i v =
-    if v then bit_or t (shift_left one i)
+    if v
+    then bit_or t (shift_left one i)
     else bit_and t (bit_xor minus_one (shift_left one i))
+  ;;
 end
 
-type t = {
-  data: Int63_chunk.t Array.t;
-  length: int
-}
+type t =
+  { data : Int63_chunk.t Array.t
+  ; length : int
+  }
 
 (* We can't use the sign bit, so we only get to use 62 bits *)
 let bits_per_bucket = 62
 
 let create sz =
-  if sz < 0 || sz > (Array.max_length * bits_per_bucket) then
-    invalid_argf "invalid size" ();
-  { data = Array.create ~len:(1 + (sz / bits_per_bucket)) Int63_chunk.empty;
-    length = sz }
+  if sz < 0 || sz > Array.max_length * bits_per_bucket
+  then invalid_argf "invalid size" ();
+  { data = Array.create ~len:(1 + (sz / bits_per_bucket)) Int63_chunk.empty
+  ; length = sz
+  }
 ;;
 
+let length t = t.length
 let bucket i = i / bits_per_bucket
 let index i = i mod bits_per_bucket
+
 let bounds_check t i =
-  if i < 0 || i >= t.length then
-    invalid_argf "Bitarray: out of bounds" ();
+  if i < 0 || i >= t.length then invalid_argf "Bitarray: out of bounds" ()
 ;;
 
 let get t i =
@@ -64,16 +66,11 @@ let set t i v =
   t.data.(bucket) <- Int63_chunk.set t.data.(bucket) (index i) v
 ;;
 
-let clear t =
-  Array.fill t.data ~pos:0 ~len:(Array.length t.data) Int63_chunk.empty
-;;
+let clear t = Array.fill t.data ~pos:0 ~len:(Array.length t.data) Int63_chunk.empty
 
 let fold =
   let rec loop t n ~init ~f =
-    if n < t.length then
-      loop t (n + 1) ~init:(f init (get t n)) ~f
-    else
-      init
+    if n < t.length then loop t (n + 1) ~init:(f init (get t n)) ~f else init
   in
   fun t ~init ~f -> loop t 0 ~init ~f
 ;;
@@ -81,8 +78,7 @@ let fold =
 let iter t ~f = fold t ~init:() ~f:(fun _ v -> f v)
 
 let sexp_of_t t =
-  Array.sexp_of_t Bool.sexp_of_t
-    (Array.init t.length ~f:(fun i -> get t i))
+  Array.sexp_of_t Bool.sexp_of_t (Array.init t.length ~f:(fun i -> get t i))
 ;;
 
 let t_of_sexp sexp =
diff --git a/src/BitarrayExt.ml b/src/BitarrayExt.ml
new file mode 100644
index 0000000..757cb55
--- /dev/null
+++ b/src/BitarrayExt.ml
@@ -0,0 +1,196 @@
+open Core
+include Bitarray
+
+let fold2 =
+  let rec loop t1 t2 n ~init ~f =
+    if n < (Bitarray.length t1) then
+      loop t1 t2 (n + 1) ~init:(f init (get t1 n) (get t2 n)) ~f
+    else
+      init
+  in
+  fun t1 t2 ~init ~f -> loop t1 t2 0 ~init ~f
+;;
+
+(* A bitarray created from the string "#b00011" will be represented by
+   the bitarray with index 0 set to true, index 1 to true, index 2 to
+   false, etc.*)
+let of_string s =
+  let prefix = String.prefix s 2 in
+  let numeral = String.drop_prefix s 2 in
+  let bvsize = String.length numeral in
+  match prefix with
+  | "#b" ->
+     let bv = create bvsize in
+     let rec loop s bv i = if i >= 0
+                           then match s with
+                                | '0'::t -> set bv i false; loop t bv (i - 1)
+                                | '1'::t -> set bv i true; loop t bv (i - 1)
+                           else
+                             bv in
+     loop (String.to_list numeral) bv (bvsize - 1)
+  | "#x" ->
+     let bv = create (bvsize * 4) in
+     let n = (bvsize - 1) in
+     let rec loop s bv i = if i <= n
+                           then match s with
+                                | '0'::t -> set bv (i * 4) false;
+                                            set bv ((i * 4) + 1) false;
+                                            set bv ((i * 4) + 2) false;
+                                            set bv ((i * 4) + 3) false;
+                                            loop t bv (i + 1)
+                                | '1'::t -> set bv (i * 4) true;
+                                            set bv ((i * 4) + 1) false;
+                                            set bv ((i * 4) + 2) false;
+                                            set bv ((i * 4) + 3) false;
+                                            loop t bv (i + 1)
+                                | '2'::t -> set bv (i * 4) false;
+                                            set bv ((i * 4) + 1) true;
+                                            set bv ((i * 4) + 2) false;
+                                            set bv ((i * 4) + 3) false;
+                                            loop t bv (i + 1)
+                                | '3'::t -> set bv (i * 4) true;
+                                            set bv ((i * 4) + 1) true;
+                                            set bv ((i * 4) + 2) false;
+                                            set bv ((i * 4) + 3) false;
+                                            loop t bv (i + 1)
+                                | '4'::t -> set bv (i * 4) false;
+                                            set bv ((i * 4) + 1) false;
+                                            set bv ((i * 4) + 2) true;
+                                            set bv ((i * 4) + 3) false;
+                                            loop t bv (i + 1)
+                                | '5'::t -> set bv (i * 4) true;
+                                            set bv ((i * 4) + 1) false;
+                                            set bv ((i * 4) + 2) true;
+                                            set bv ((i * 4) + 3) false;
+                                            loop t bv (i + 1)
+                                | '6'::t -> set bv (i * 4) false;
+                                            set bv ((i * 4) + 1) true;
+                                            set bv ((i * 4) + 2) true;
+                                            set bv ((i * 4) + 3) false;
+                                            loop t bv (i + 1)
+                                | '7'::t -> set bv (i * 4) true;
+                                            set bv ((i * 4) + 1) true;
+                                            set bv ((i * 4) + 2) true;
+                                            set bv ((i * 4) + 3) false;
+                                            loop t bv (i + 1)
+                                | '8'::t -> set bv (i * 4) false;
+                                            set bv ((i * 4) + 1) false;
+                                            set bv ((i * 4) + 2) false;
+                                            set bv ((i * 4) + 3) true;
+                                            loop t bv (i + 1)
+                                | '9'::t -> set bv (i * 4) true;
+                                            set bv ((i * 4) + 1) false;
+                                            set bv ((i * 4) + 2) false;
+                                            set bv ((i * 4) + 3) true;
+                                            loop t bv (i + 1)
+                                | 'a'::t -> set bv (i * 4) false;
+                                            set bv ((i * 4) + 1) true;
+                                            set bv ((i * 4) + 2) false;
+                                            set bv ((i * 4) + 3) true;
+                                            loop t bv (i + 1)
+                                | 'b'::t -> set bv (i * 4) true;
+                                            set bv ((i * 4) + 1) true;
+                                            set bv ((i * 4) + 2) false;
+                                            set bv ((i * 4) + 3) true;
+                                            loop t bv (i + 1)
+                                | 'c'::t -> set bv (i * 4) false;
+                                            set bv ((i * 4) + 1) false;
+                                            set bv ((i * 4) + 2) true;
+                                            set bv ((i * 4) + 3) true;
+                                            loop t bv (i + 1)
+                                | 'd'::t -> set bv (i * 4) true;
+                                            set bv ((i * 4) + 1) false;
+                                            set bv ((i * 4) + 2) true;
+                                            set bv ((i * 4) + 3) true;
+                                            loop t bv (i + 1)
+                                | 'e'::t -> set bv (i * 4) false;
+                                            set bv ((i * 4) + 1) true;
+                                            set bv ((i * 4) + 2) true;
+                                            set bv ((i * 4) + 3) true;
+                                            loop t bv (i + 1)
+                                | 'f'::t -> set bv (i * 4) true;
+                                            set bv ((i * 4) + 1) true;
+                                            set bv ((i * 4) + 2) true;
+                                            set bv ((i * 4) + 3) true;
+                                            loop t bv (i + 1)
+                           else
+                             bv in
+     loop (String.to_list (String.rev numeral)) bv 0
+;;
+
+(* TODO: If the length of the bitvector is a multiple of 4, represent with hex.*)
+let to_string bv = "#b" ^ (fold bv ~init:"" ~f:(fun acc -> function
+                               | false -> "0" ^ acc
+                               | true -> "1" ^ acc))
+;;
+
+let rec add bv1 bv2 =
+  let sum = create bv1.length in
+  let s, _, _ = fold2 bv1 bv2 ~init:(sum, 0, 0) ~f:(fun (sum, carry, ind) v1 v2 ->
+                    match v1, v2 with
+                    | true, true -> if phys_equal carry 1
+                                    then (set sum ind true; (sum, 1, ind + 1))
+                                    else (set sum ind false; (sum, 1, ind + 1))
+                    | false, true
+                      | true, false -> if phys_equal carry 1
+                                       then (set sum ind false; (sum, 1, ind + 1))
+                                       else (set sum ind true; (sum, 0, ind + 1))
+                    | false, false -> if phys_equal carry 1
+                                      then (set sum ind true; (sum, 0, ind + 1))
+                                      else (set sum ind false; (sum, 0, ind + 1))) in
+  s
+;;
+
+let bvnot bv =
+  let bv_new = create bv.length in
+  fold bv ~init:(bv, 0) ~f:(fun (bv, i) v ->
+      if phys_equal v true then (set bv_new i false; (bv, i + 1))
+      else (set bv_new i true; (bv, i + 1)))
+  ;
+    bv_new
+;;
+
+let compare bv1 bv2 =
+  let rec helper ind bv1 bv2 =
+    if ind >= 0 then
+      let v1 = get bv1 ind in
+      let v2 = get bv2 ind in
+      if phys_equal v1 v2 then helper (ind - 1) bv1 bv2
+      else if phys_equal v1 false then -1 else 1
+    else
+      0
+  in
+  helper (bv1.length - 1) bv1 bv2
+;;
+
+let bvult bv1 bv2 =
+  let c = compare bv1 bv2 in
+  if c >= 0 then false else true
+;;
+
+let bvule bv1 bv2 =
+  (bvult bv1 bv2) || ((compare bv1 bv2) = 0)
+;;
+
+let concat bv1 bv2 =
+  let bv3 = create (bv1.length + bv2.length) in
+  let bv1_, _ = fold bv1 ~init:(bv3, bv2.length) ~f:(fun (bv, i) v ->
+                       set bv i v; (bv, i+1)) in
+  let bv12, _ = fold bv2 ~init:(bv1_, 0) ~f:(fun (bv, i) v ->
+                    set bv i v; (bv, i+1)) in
+  bv12
+;;
+
+let bvuge bv1 bv2 =
+  (bvult bv2 bv1) || ((compare bv1 bv2) = 0)
+;;
+
+let bvugt bv1 bv2 =
+  bvult bv2 bv1
+;;
+
+let bvsub bv1 bv2 =
+  let const_one = create bv2.length in
+  set const_one 0 true;
+  (add bv1 (add (bvnot bv2) const_one))
+;;
\ No newline at end of file
diff --git a/src/Logic.ml b/src/Logic.ml
index 5fb9d38..81f0ec9 100644
--- a/src/Logic.ml
+++ b/src/Logic.ml
@@ -37,6 +37,10 @@ let all_supported =
                    components_per_level = ArrayComponents.levels ++ BooleanComponents.levels ++ IntegerComponents.non_linear_levels ;
                    sample_set_size_multiplier = 8
                  } ; {
+                     name = "BV";
+                     components_per_level = BooleanComponents.levels ++ BitVecComponents.levels;
+                     sample_set_size_multiplier = 1
+                } ; {
                    name = "ALL" ;
                    (* FIXME: The verification side for lists, especially with transformed components,
                              doesn't work as of now -- we need to emit valid SMTLIB expressions for them *)
diff --git a/src/Synthesizer.ml b/src/Synthesizer.ml
index b9df624..6244563 100644
--- a/src/Synthesizer.ml
+++ b/src/Synthesizer.ml
@@ -153,6 +153,7 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) =
                             | ARRAY _ , ARRAY _ -> true
                             | LIST _ , LIST _ -> true
                             | TVAR _, _ -> true
+                            | BITVEC _, BITVEC _ -> true
                             | cod, t_type -> equal cod t_type)
      in Array.(append
           (create ~len:1 [])
@@ -170,6 +171,7 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) =
   let string_components = typed_components Type.STRING in
   let poly_list_components = typed_components Type.(LIST (TVAR "_")) in
   let poly_array_components = typed_components Type.(ARRAY (TVAR "_", TVAR "_")) in
+  let bitvec_components = typed_components Type.(BITVEC (-1)) in
 
   let empty_candidates () =
     Array.(init ((length config.logic.components_per_level) + 1)
@@ -182,6 +184,7 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) =
   let string_candidates = empty_candidates () in
   let list_candidates = empty_candidates () in
   let array_candidates = empty_candidates () in
+  let bitvec_candidates = empty_candidates () in
 
   let typed_candidates ?(no_tvar = false) = function
     | Type.INT     -> int_candidates
@@ -189,12 +192,14 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) =
     | Type.CHAR    -> char_candidates
     | Type.STRING  -> string_candidates
     | Type.LIST _  -> list_candidates
+    | Type.BITVEC _ -> bitvec_candidates
     | Type.ARRAY _ -> array_candidates
     | Type.TVAR _ when not no_tvar
       -> raise (Internal_Exn "No candidates for TVAR")
     | Type.TVAR _ -> let (@) = Array.append
                       in int_candidates @ bool_candidates @ char_candidates
-                       @ string_candidates @ list_candidates @ array_candidates
+                         @ string_candidates @ list_candidates @ array_candidates
+                         @ bitvec_candidates
   in
 
   let seen_outputs = ref (Set.empty (module Output)) in
@@ -262,6 +267,7 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) =
             let cod = Type.(match unified_component.codomain with
                             | ARRAY _ -> ARRAY (TVAR "_" , TVAR "_")
                             | LIST _ -> LIST (TVAR "_")
+                            | BITVEC _ -> BITVEC (-1)
                             | cod -> cod)
              in if not (Type.equal cod cand_type) then
                   Log.debug (lazy ("  > The candidate type " ^ (Type.to_string cand_type) ^
@@ -311,13 +317,15 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) =
                                  ; (CHAR, char_candidates)
                                  ; (STRING, string_candidates)
                                  ; (LIST (TVAR "_"), list_candidates)
-                                 ; (ARRAY (TVAR "_", TVAR "_"), array_candidates) ]
+                                 ; (ARRAY (TVAR "_", TVAR "_"), array_candidates)
+                                 ; (BITVEC (-1), bitvec_candidates) ]
                             [ bool_components.(l)
                             ; int_components.(l)
                             ; char_components.(l)
                             ; string_components.(l)
                             ; poly_list_components.(l)
-                            ; poly_array_components.(l) ]
+                            ; poly_array_components.(l)
+                            ; bitvec_components.(l) ]
                             ~f:(fun (cand_type, cands) comps
                                 -> List.iter comps ~f:(expand_component l level cost cands cand_type))))
 
diff --git a/src/TestGen.ml b/src/TestGen.ml
index 4da3bcd..057acbf 100644
--- a/src/TestGen.ml
+++ b/src/TestGen.ml
@@ -15,5 +15,13 @@ let rec for_type (t : Type.t) : Value.t Generator.t =
   | Type.ARRAY (key,value) -> (Int.gen_incl 0 64)
                               >>= fun len -> ((tuple2 (List.gen_with_length len (tuple2 (for_type key) (for_type value))) (for_type value))
                                               >>= fun (arr, def) -> singleton (Value.Array (key, value, arr, def)))
+  | Type.BITVEC n -> let bv = Bitarray.create n in
+                     let randarray = Bitarray.fold bv ~init:((singleton bv), 0)
+                                       ~f:(fun (sbv, i) _ ->
+                                         (sbv >>= fun bitarr -> bool >>= fun b ->
+                                                                Bitarray.set bitarr i b; singleton bitarr), i+1) in
+                     (match randarray with
+                      | sbv, i -> sbv >>= fun bv -> singleton (Value.BitVec bv))
+
   | Type.LIST _ | Type.TVAR _
     -> raise (Exceptions.Internal_Exn "Generator not implemented!")
\ No newline at end of file
diff --git a/src/Type.ml b/src/Type.ml
index 766221a..2894e96 100644
--- a/src/Type.ml
+++ b/src/Type.ml
@@ -10,6 +10,7 @@ module T = struct
          | TVAR of string
          | LIST of t
          | ARRAY of (t * t)
+         | BITVEC of int
          [@@deriving compare,sexp]
 end
 
@@ -27,6 +28,8 @@ let rec of_sexp (sexp: Sexp.t) : t =
       -> LIST (of_sexp typ)
     | List [Atom "Array" ; index ; value]
       -> ARRAY ((of_sexp index) , (of_sexp value))
+    | List [Atom "_"; Atom "BitVec"; Atom n]
+      -> BITVEC (Int.of_string n)
     | s -> raise (Parse_Exn ("Could not parse type `" ^ (Sexp.to_string_hum s) ^ "`."))
 
 let rec to_string : t -> string = function
@@ -36,6 +39,7 @@ let rec to_string : t -> string = function
   | STRING      -> "String"
   | LIST t      -> "(List " ^ (to_string t) ^ ")"
   | ARRAY (k,v) -> "(Array " ^ (to_string k) ^ " " ^ (to_string v) ^ ")"
+  | BITVEC n    -> "(_ BitVec " ^ (Int.to_string n) ^ ")"
   | TVAR n      -> n
     (* TODO: We may want to detect cases when a TVAR should never occur in a type,
              and throw exceptions in those cases *)
@@ -46,41 +50,60 @@ module Unification = struct
   * TODO: The algorithm below is simple but not efficient.
   * See: https://eli.thegreenplace.net/2018/unification#efficiency
   *)
+  type id =
+    | STR of string
+    | NUM of int
 
-  let rec substitute_with_exn (env : (string * t) list) = function
+  let rec substitute_with_exn (env : (id * t) list) = function
     | TVAR name -> begin
-        match List.find ~f:(fun (id,_) -> String.equal id name) env with
+        match List.find ~f:(fun (id,_) -> match id with
+                                          | STR idstr -> String.equal idstr name
+                                          | _ -> false) env with
         | Some (_,value) -> value
         | _ -> raise (Unification_Exn ("Could not find a binding for " ^ name))
       end
     | LIST typ          -> LIST (substitute_with_exn env typ)
     | ARRAY (key,value) -> ARRAY ((substitute_with_exn env key),
                                   (substitute_with_exn env value))
+    | BITVEC len        -> (match List.find env ~f:(fun (id,_) -> (match id with
+                                                                   | NUM idnum -> Int.equal idnum len
+                                                                   | _ -> false)) with
+                            | Some (_, value) -> value
+                            | _ -> raise (Unification_Exn ("Could not find a binding for " ^ (to_string (BITVEC len)))))
     | t -> t
 
-  let substitute (env : (string * t) list) (t : t) : t option =
+  let substitute (env : (id * t) list) (t : t) : t option =
     try Some (substitute_with_exn env t) with _ -> None
 
   let rec resolve_var ?(env = []) = function
-    | lhs, TVAR rhs -> if String.equal lhs rhs
-                       then raise (Unification_Exn "Circular dependency!")
-                       else begin
-                         match List.find env ~f:(fun (e,_) -> String.equal e rhs) with
-                         | None -> (lhs, TVAR rhs)
-                         | Some (_, (TVAR x)) -> resolve_var ~env (lhs, (TVAR x))
-                         | Some (_, rhs) -> (lhs, rhs)
-                       end
+    | STR lhs, TVAR rhs -> if String.equal lhs rhs
+                           then raise (Unification_Exn "Circular dependency!")
+                           else begin
+                               match List.find env ~f:(fun (e,_) -> match e with
+                                                                    | STR idstr -> String.equal idstr rhs
+                                                                    | _ -> false) with
+                               | None -> (STR lhs, TVAR rhs)
+                               | Some (_, (TVAR x)) -> resolve_var ~env (STR lhs, (TVAR x))
+                               | Some (_, rhs) -> (STR lhs, rhs)
+                             end
     | pair -> pair
 
-  let rec of_var ?(env = []) (var : string) (rhs : t) =
-    match List.Assoc.find env ~equal:String.equal var with
+  let rec of_var ?(env = []) (var : id) (rhs : t) =
+    match List.Assoc.find env ~equal:(fun idquery idenv -> (match (idenv, idquery) with
+                                                | (STR id1), (STR id2) -> String.equal id1 id2
+                                                | (NUM id1), (NUM id2) -> Int.equal id1 id2
+                                                | _ -> false)) var with
     | None -> begin
         match rhs with
         | TVAR var_rhs -> begin
-            match List.Assoc.find env ~equal:String.equal var_rhs with
+            match List.Assoc.find env ~equal:(fun _ idvar -> match idvar with
+                                                           | STR idstr -> String.equal idstr var_rhs
+                                                           | _ -> false) (STR var_rhs) with
             | None -> List.fold ((var,rhs) :: env) ~init:[]
                                 ~f:(fun acc elem -> (resolve_var elem ~env:(((var,rhs) :: env)) :: acc))
-            | Some value -> of_type ~env (TVAR var) value
+            | Some value -> (match var with
+                            | STR varstr -> of_type ~env (TVAR varstr) value
+                            | _ -> raise (Unification_Exn ("Type variable was as integer but should be a string")))
           end
         | _ -> List.fold ((var,rhs) :: env) ~init:[]
                          ~f:(fun acc elem -> (resolve_var elem ~env:(((var,rhs)::env)) :: acc))
@@ -88,21 +111,25 @@ module Unification = struct
     | Some value -> of_type ~env value rhs
   and of_type ?(env = []) (lhs : t) (rhs : t) =
     match lhs, rhs with
-    | TVAR x , _ -> of_var ~env x rhs
-    | _ , TVAR y -> of_var ~env y lhs
+    | TVAR x , _ -> of_var ~env (STR x) rhs
+    | _ , TVAR y -> of_var ~env (STR y) lhs
     | LIST lhs_type, LIST rhs_type
       -> of_type lhs_type rhs_type ~env
     | ARRAY (lhs_key,lhs_value), ARRAY (rhs_key,rhs_value)
       -> let env = env @ (of_type ~env lhs_key rhs_key)
           in (of_type lhs_value rhs_value ~env)
+    | BITVEC llen, BITVEC rlen -> (match llen, rlen with
+                                   | _ when Int.(<) llen 0 -> of_var ~env (NUM llen) rhs
+                                   | _ when Int.(<) rlen 0 -> of_var ~env (NUM rlen) lhs
+                                   | _ -> env)
     | lhs , rhs -> if equal lhs rhs then env
                    else raise (Unification_Exn "Circular dependency!")
 
-  let rec of_types_exn ?(env = []) (lhs : t list) (rhs : t list) : (string * t) list =
+  let rec of_types_exn ?(env = []) (lhs : t list) (rhs : t list) : (id * t) list =
     match lhs , rhs with
     | (x :: tx, y :: ty) -> of_types_exn ~env:(of_type ~env x y) tx ty
     | _ -> env
 
-  let of_types ?(env = []) (t1 : t list) (t2 : t list) : (string * t) list option =
+  let of_types ?(env = []) (t1 : t list) (t2 : t list) : (id * t) list option =
       try Some (of_types_exn t1 t2) with _ -> None
 end
\ No newline at end of file
diff --git a/src/Value.ml b/src/Value.ml
index 8035d7b..ba1e937 100644
--- a/src/Value.ml
+++ b/src/Value.ml
@@ -7,6 +7,7 @@ module T = struct
          | Bool of bool
          | Char of char
          | String of string
+         | BitVec of BitarrayExt.t
          | List of Type.t * t list
          | Array of Type.t * Type.t * (t * t) list * t
            (* FIXME: Use HashTable instead of List *)
@@ -24,6 +25,7 @@ let rec typeof : t -> Type.t = function
   | List (typ, _) -> Type.LIST typ
   | Array (key_type, value_type, _, _)
     -> Type.ARRAY (key_type,value_type)
+  | BitVec bv -> Type.BITVEC bv.length
 
 let rec to_string : t -> string = function
   | Int i    -> Int.to_string i
@@ -31,6 +33,7 @@ let rec to_string : t -> string = function
   | Char c   -> "\'" ^ (Char.to_string c) ^ "\'"
   | String s -> "\"" ^ s ^ "\""
   | List _   -> raise (Internal_Exn "List type (de/)serialization not implemented!")
+  | BitVec bv -> BitarrayExt.to_string bv
   | Array (key_type, val_type, value, default_v)
     -> let default_string = "((as const (Array " ^ (Type.to_string key_type) ^ " " ^ (Type.to_string val_type) ^ ")) " ^ (to_string default_v) ^ ")"
         in List.fold_left ~init:default_string value
@@ -44,6 +47,8 @@ let of_atomic_string (s : string) : t =
   with Invalid_argument _ -> try
     Char (Char.of_string (String.(chop_suffix_exn ~suffix:"\'"
                                     (chop_prefix_exn ~prefix:"\'" s))))
+  with Invalid_argument _ -> try
+    BitVec (BitarrayExt.of_string s)
   with Invalid_argument _ -> try
     String String.(chop_suffix_exn ~suffix:"\"" (chop_prefix_exn ~prefix:"\"" s))
   with Invalid_argument _ ->
diff --git a/test/Runner.ml b/test/Runner.ml
index c5554a1..6cea918 100644
--- a/test/Runner.ml
+++ b/test/Runner.ml
@@ -3,6 +3,7 @@ let () =
     (* FIXME: Find a way to pass command-line arguments within dune's runtest alias *)
     (let zpath = if (Array.length Sys.argv) > 1 then Sys.argv.(1) else ""
       in [ "Test_ArrayComponents", Test_ArrayComponents.all
+         ; "Test_BitVecComponents", Test_BitVecComponents.all
          ; "Test_BFL", Test_BFL.all
          ; "Test_Expr", Test_Expr.all
          ; "Test_NormalForm", Test_NormalForm.all
diff --git a/test/Test_BitVecComponents.ml b/test/Test_BitVecComponents.ml
new file mode 100644
index 0000000..a0a7eca
--- /dev/null
+++ b/test/Test_BitVecComponents.ml
@@ -0,0 +1,129 @@
+open Base
+
+open LoopInvGen
+
+let bveq_eval = (List.find_exn BitVecComponents.all
+                    ~f:(fun comp -> String.equal comp.name "bv-eq")).evaluate
+let bvadd_eval = (List.find_exn BitVecComponents.all
+                    ~f:(fun comp -> String.equal comp.name "bvadd")).evaluate
+let bvnot_eval = (List.find_exn BitVecComponents.all
+                    ~f:(fun comp -> String.equal comp.name "bvnot")).evaluate
+let bvult_eval = (List.find_exn BitVecComponents.all
+                    ~f:(fun comp -> String.equal comp.name "bvult")).evaluate
+let bvuge_eval = (List.find_exn BitVecComponents.all
+                    ~f:(fun comp -> String.equal comp.name "bvuge")).evaluate
+let bvugt_eval = (List.find_exn BitVecComponents.all
+                    ~f:(fun comp -> String.equal comp.name "bvugt")).evaluate
+let bvule_eval = (List.find_exn BitVecComponents.all
+                    ~f:(fun comp -> String.equal comp.name "bvule")).evaluate
+let bvsub_eval = (List.find_exn BitVecComponents.all
+                    ~f:(fun comp -> String.equal comp.name "bvsub")).evaluate
+
+
+let equal_hex_bin () =
+  let bv1 = Value.BitVec (BitarrayExt.of_string "#x1010") in
+  let bv2 = Value.BitVec (BitarrayExt.of_string "#b0001000000010000") in
+  let eq_ret = bveq_eval [bv1; bv2] in
+  let ret = Value.equal (Value.Bool true) eq_ret in
+  Alcotest.(check bool) "identical" true ret
+
+let bvadd () =
+  let bv1 = Value.BitVec (BitarrayExt.of_string "#b10101010101010101") in
+  let bv2 = Value.BitVec (BitarrayExt.of_string "#b01010101010101010") in
+  let add_ret = bvadd_eval [bv1; bv2] in
+  let ret = Value.equal (Value.BitVec (BitarrayExt.of_string "#b11111111111111111")) add_ret in
+  Alcotest.(check bool) "identical" true ret
+
+let bvadd_ovf () =
+  let bv1 = Value.BitVec (BitarrayExt.of_string "#b10101010101010101") in
+  let bv2 = Value.BitVec (BitarrayExt.of_string "#b01010101010101011") in
+  let add_ret = bvadd_eval [bv1; bv2] in
+  let ret = Value.equal (Value.BitVec (BitarrayExt.of_string "#b00000000000000000")) add_ret in
+  Alcotest.(check bool) "identical" true ret  
+
+let bvnot () =
+  let bv = Value.BitVec (BitarrayExt.of_string "#xa482ad9301") in
+  let bvnot_ret = bvnot_eval [bv] in
+  let ret = Value.equal (Value.BitVec (BitarrayExt.of_string "#x5b7d526cfe")) bvnot_ret in
+  Alcotest.(check bool) "identical" true ret
+
+let bvult_same () =
+  let bv1 = Value.BitVec (BitarrayExt.of_string "#x00000000") in
+  let bvult_ret = bvult_eval [bv1; bv1] in
+  let ret = Value.equal (Value.Bool false) bvult_ret in
+  Alcotest.(check bool) "identical" true ret
+
+let bvult_ovf () =
+  (* bv1 is a bitvector which has a 63bit BitarrayExt *)
+  let bv1 = Value.BitVec
+              (BitarrayExt.of_string
+                 "#b111111111111111111111111111111111111111111111111111111111111111") in
+  let bvult_ret = bvult_eval [bv1; bv1] in
+  let ret = Value.equal (Value.Bool false) bvult_ret in
+  Alcotest.(check bool) "identical" true ret
+
+let bvult_onegreater () =
+  let bv1 = Value.BitVec (BitarrayExt.of_string "#x1") in
+  let bv2 = Value.BitVec (BitarrayExt.of_string "#x0") in
+  let bvult_ret = bvult_eval [bv2; bv1] in
+  let ret = Value.equal (Value.Bool true) bvult_ret in
+  Alcotest.(check bool) "identical" true ret
+
+let bvuge () =
+  let bv1 = Value.BitVec (BitarrayExt.of_string "#xff") in
+  let bv2 = Value.BitVec (BitarrayExt.of_string "#b11111111") in
+  let bvuge_ret = bvuge_eval [bv2; bv1] in
+  let ret = Value.equal (Value.Bool true) bvuge_ret in
+  Alcotest.(check bool) "identical" true ret
+  
+let bvugt () =
+  let bv1 = Value.BitVec (BitarrayExt.of_string "#xa") in
+  let bv2 = Value.BitVec (BitarrayExt.of_string "#b1000") in
+  let bvugt_ret = bvugt_eval [bv1; bv2] in
+  let ret = Value.equal (Value.Bool true) bvugt_ret in
+  Alcotest.(check bool) "identical" true ret
+
+let bvule () =
+  let bv1 = Value.BitVec (BitarrayExt.of_string "#x1") in
+  let bv2 = Value.BitVec (BitarrayExt.of_string "#xb") in
+  let bvule_ret = bvult_eval [bv1; bv2] in
+  let ret = Value.equal (Value.Bool true) bvule_ret in
+  Alcotest.(check bool) "identical" true ret
+
+let bvsub () =
+  let bv1 = Value.BitVec (BitarrayExt.of_string "#b00") in
+  let bv2 = Value.BitVec (BitarrayExt.of_string "#b01") in
+  let bvsub_ret = bvsub_eval [bv1; bv2] in
+  (* We should get the representation for -1 *)
+  let ret = Value.equal (Value.BitVec (BitarrayExt.of_string "#b11")) bvsub_ret in
+  Alcotest.(check bool) "identical" true ret
+
+
+let bv_pp f p = match p with
+  | Value.BitVec ba -> Format.fprintf f "%s\n" (BitarrayExt.to_string ba)
+  | _ -> Format.fprintf f "Error with pretty printing the BitVector\n"
+            
+let bitvec_testable = Alcotest.testable bv_pp (fun x y -> Value.equal (Value.Bool true) (bveq_eval [x; y]))
+
+let gen () =
+  let bvgen1 = TestGen.for_type (Type.BITVEC 32) in
+  let bvgen2 = TestGen.for_type (Type.BITVEC 32) in
+  Alcotest.(check (neg bitvec_testable)) "identical"
+    (Core.Quickcheck.Generator.generate bvgen1 ~size:1 ~random:(Splittable_random.State.of_int 1))
+    (Core.Quickcheck.Generator.generate bvgen2 ~size:1 ~random:(Splittable_random.State.of_int 2))
+
+
+let all = [
+    "equal hex and binary", `Quick, equal_hex_bin ;
+    "bvadd", `Quick, bvadd ;
+    "bvadd_ovf", `Quick, bvadd_ovf ;
+    "bvnot", `Quick, bvnot ;
+    "bvult_same", `Quick, bvult_same ;
+    "bvult_ovf", `Quick, bvult_ovf ;
+    "bvult_onegreater", `Quick, bvult_onegreater ;
+    "bvuge", `Quick, bvuge ;
+    "bvugt", `Quick, bvugt ;
+    "bvule", `Quick, bvule ;
+    "bvsub", `Quick, bvsub ;
+    "gen", `Quick, gen
+  ]
\ No newline at end of file
diff --git a/test/Test_Synthesizer.ml b/test/Test_Synthesizer.ml
index 43c77a4..2d19fd9 100644
--- a/test/Test_Synthesizer.ml
+++ b/test/Test_Synthesizer.ml
@@ -180,6 +180,39 @@ let all_mapR_ge_l_0 () =
     constants = []
   } in Alcotest.(check string) "identical" "(all (map-fixR-int-geq l 0))" result.string
 
+let bvadd_a_b () =
+  let result = solve ~config:{ Config.default with logic = Logic.of_string "BV" } {
+    arg_names = ["a"; "b"];
+    inputs = List.map ~f:(fun a -> Array.map ~f:(fun x -> Value.BitVec (BitarrayExt.of_string x)) a)
+    [ [| "#b00"; "#b01" ; "#b10" ; "#b11" |] ;
+      [| "#b01"; "#b10" ; "#b11" ; "#b00"|]];
+    outputs = Array.map ~f:(fun x -> Value.BitVec (BitarrayExt.of_string x))
+    [| "#b01"; "#b11"; "#b01" ; "#b11" |];
+    constants = []
+  } in Alcotest.(check string) "identical" "(bvadd a b)" result.string
+
+let bvult_a_b () =
+  let result = solve ~config:{ Config.default with logic = Logic.of_string "BV" } {
+    arg_names = ["a"; "b"];
+    inputs = List.map ~f:(fun a -> Array.map ~f:(fun x -> Value.BitVec (BitarrayExt.of_string x)) a)
+    [ [| "#b00"; "#b01" ; "#b10" ; "#b11"|] ;
+      [| "#b01"; "#b10" ; "#b11" ; "#b00"|]];
+    outputs = Array.map ~f:(fun b -> Value.Bool b)
+    [|true; true; true; false|];
+    constants = []
+  } in Alcotest.(check string) "identical" "(bvult a b)" result.string
+
+let bvnot_bvsub_a_b () =
+  let result = solve ~config:{ Config.default with logic = Logic.of_string "BV" } {
+    arg_names = ["a"; "b"];
+    inputs = List.map ~f:(fun a -> Array.map ~f:(fun x -> Value.BitVec (BitarrayExt.of_string x)) a)
+    [ [| "#b0000"; "#b0010" ; "#b1000" ; "#b1100"|] ;
+      [| "#b0100"; "#b1000" ; "#b1100" ; "#b0000"|]];
+    outputs = Array.map ~f:(fun x -> Value.BitVec (BitarrayExt.of_string x))
+    [|"#b0011"; "#b0101"; "#b0011"; "#b0011"|];
+    constants = []
+  } in Alcotest.(check string) "identical" "(bvnot (bvsub a b))" result.string
+
 let all = [
   "(+ x y)",                         `Quick, plus_x_y ;
   "(>= (+ x z) y)",                  `Quick, ge_plus_x_z_y ;
@@ -191,4 +224,7 @@ let all = [
   "(store a k v) ; with duplicates", `Quick, store_a_k_v__with_duplicates ;
   "(>= y (len x))",                  `Quick, ge_y_len_x ;
   "(all (map-fixR-int-geq l 0))",    `Quick, all_mapR_ge_l_0 ;
+  "(bvadd a b)",                     `Quick, bvadd_a_b ;
+  "(bvult a b)",                     `Quick, bvult_a_b ;
+  "(bvnot (bvsub a b))",             `Quick, bvnot_bvsub_a_b ;
 ]
\ No newline at end of file
diff --git a/test/Test_Unification.ml b/test/Test_Unification.ml
index fbad637..612bb27 100644
--- a/test/Test_Unification.ml
+++ b/test/Test_Unification.ml
@@ -6,7 +6,10 @@ open Exceptions
 open Type
 
 let are_bindings_equal =
-  List.equal (Tuple.T2.equal ~eq1:String.equal ~eq2:equal)
+  List.equal (Tuple.T2.equal ~eq1:(fun var1 var2 -> match var1, var2 with
+                                                    | Unification.STR var1str, Unification.STR var2str -> String.equal var1str var2str
+                                                    | Unification.NUM var1num, Unification.NUM var2num -> Int.equal var1num var2num
+                                                    | _ -> false) ~eq2:equal)
 
 let monomorphic () =
   let domain1 = [ INT ; STRING ] in
@@ -20,7 +23,7 @@ let without_dependencies () =
   let domain1 = [ ARRAY (TVAR "a", TVAR "b") ; INT ; STRING ] in
   let domain2 = [ ARRAY (INT,BOOL) ; INT ; STRING ] in
   let bindings = Unification.of_types_exn domain1 domain2 in
-  let bindings_correct = [("a", INT); ("b", BOOL)] in
+  let bindings_correct = [(Unification.STR "a", INT); (Unification.STR "b", BOOL)] in
   let res = are_bindings_equal bindings bindings_correct
    in Alcotest.(check bool) "identical" true res
 
@@ -28,7 +31,7 @@ let with_dependencies () =
   let domain1 = [ ARRAY (TVAR "a", TVAR "b") ; LIST(TVAR "a") ] in
   let domain2 = [ ARRAY (STRING,INT) ; LIST STRING ] in
   let bindings = Unification.of_types_exn domain1 domain2 in
-  let correct_bindings = [("a", STRING) ; ("b", INT)] in
+  let correct_bindings = [(Unification.STR "a", STRING) ; (Unification.STR "b", INT)] in
   let res = are_bindings_equal bindings correct_bindings
    in Alcotest.(check bool) "identical" true res
 
@@ -45,7 +48,7 @@ let direct_circular () =
    in Alcotest.check_raises "cannot unify" (Unification_Exn "Circular dependency!") test
 
 let substitution () =
-  let env = [("a",STRING) ; ("b",INT)] in
+  let env = [(Unification.STR "a",STRING) ; (Unification.STR "b",INT)] in
   let codomain = ARRAY(TVAR "b" , TVAR "a") in
   let resolved_codomain = ARRAY(INT,STRING) in
   let res = match Unification.substitute env codomain with
@@ -54,7 +57,7 @@ let substitution () =
    in Alcotest.(check bool) "correct application of env" true res
 
 let incomplete_substitution () =
-  let env = [("a",INT)] in
+  let env = [(Unification.STR "a",INT)] in
   let codomain = ARRAY(TVAR "a" , TVAR "b") in
   let resolved_codomain = ARRAY (INT ,INT) in
   let res = match Unification.substitute env codomain with
@@ -62,6 +65,23 @@ let incomplete_substitution () =
             | None -> false
    in Alcotest.(check bool) "incorrect application of env" false res
 
+let bitvec () =
+  let domain1 = [BITVEC (-2); BITVEC (-1) ; BITVEC (-2)] in
+  let domain2 = [BITVEC (32); BITVEC (32) ; BITVEC (32)] in
+  let bindings = Unification.of_types_exn domain1 domain2 in
+  let bindings_correct = [(Unification.NUM (-2), BITVEC (32)) ; (Unification.NUM (-1), BITVEC (32))] in
+  let res = are_bindings_equal bindings bindings_correct
+  in Alcotest.(check bool) "identical" true res
+
+let bitvec_sub () =
+  let env = [(Unification.NUM (-1), BITVEC (32))] in
+  let codomain = BITVEC (-1) in
+  let resolved_codomain =  BITVEC (32) in
+  let res = match Unification.substitute env codomain with
+    | Some res -> equal res resolved_codomain
+    | None -> false in
+  Alcotest.(check bool) "incorrect application of env" true res
+
 let all = [
   "Unif. of monomorphic types",   `Quick, monomorphic ;
   "Unif. without dependencies",   `Quick, without_dependencies ;
@@ -70,4 +90,6 @@ let all = [
   "Indirect circular dependency", `Quick, indirect_circular ;
   "Substitution",                 `Quick, substitution ;
   "Incomplete substitution",      `Quick, incomplete_substitution ;
+  "Bitvec",                       `Quick, bitvec ;
+  "Bitvec substitution",          `Quick, bitvec_sub ;
 ]
\ No newline at end of file