Add BV interpretation

dolmen @ 365eeab8

-Subproject commit 7cd59bbeaa536056d19facdbdc724b104e891732
+Subproject commit 365eeab891d19457e8cc8cc103ce21d3e50b33dc

src_colibri2/stdlib/std.ml

@@ -110,6 +110,9 @@ module Q = struct
 
   let is_integer q = Z.equal Z.one q.Q.den
 
+  let is_unsigned_integer size q =
+    is_integer q && Int.(Z.sign q.Q.num >= 0) && Int.(Z.numbits q.Q.num <= size)
+
   let floor x = Q.of_bigint (Z.fdiv x.Q.num x.Q.den)
 
   let ceil x = Q.of_bigint (Z.cdiv x.Q.num x.Q.den)

src_colibri2/stdlib/std.mli

@@ -68,6 +68,10 @@ module Q : sig
 
   val is_integer : t -> bool
 
+  val is_unsigned_integer : int -> t -> bool
+  (** [is_unsigned_integer size q] checks that [q] is an integer that fits in
+   [size] bits *)
+
   val none_zero : t -> t option
   (** return None if the input is zero otherwise Some of the value *)
 

src_colibri2/tests/solve/smt_bv/sat/bigHex.smt2

+(set-info :smt-lib-version 2.6)
+(set-logic QF_BV)
+(set-info :source |
+	Constructed by Trevor Hansen to test that #x and #b literals are working. Allocation of big constants.
+        With explicit explicit constant added.
+|)
+(set-info :category "check")
+(set-info :status sat)
+(assert (= #b1111 #xf))
+(assert (= (_ bv114813069527425452423283320117768198402231770208869520047764273682576626139237031385665948631650626991844596463898746277344711896086305533142593135616665318539129989145312280000688779148240044871428926990063486244781615463646388363947317026040466353970904996558162398808944629605623311649536164221970332681344168908984458505602379484807914058900934776500429002716706625830522008132236281291761267883317206598995396418127021779858404042159853183251540889433902091920554957783589672039160081957216630582755380425583726015528348786419432054508915275783882625175435528800822842770817965453762184851149029375 2000) (bvnot (_ bv0 2000))))
+(check-sat)
+(exit)

src_colibri2/tests/solve/smt_bv/sat/dune

+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps
+  (glob_files *.cnf)
+  (glob_files *.smt2))
+ (action
+  (with-stdout-to
+   dune.inc
+   (run %{exe:../../../generate_tests/generate_dune_tests.exe} . sat)))
+ (mode promote))

src_colibri2/tests/solve/smt_bv/sat/dune.inc

+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=30s --max-steps 3500 --check-status sat 
+--dont-print-result %{dep:bigHex.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:bigHex.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=30s --max-steps 3500 --check-status sat 
+--dont-print-result %{dep:unit_test.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:unit_test.smt2})))

src_colibri2/tests/solve/smt_bv/sat/unit_test.smt2

+(set-logic QF_BV)
+
+(assert (= (bvnot #b1010) #b0101))
+(assert (= (bvand #b1010 #b0001) #b0000))
+(assert (= (bvor  #b1010 #b0001) #b1011))
+(assert (= (bvnand #b1010 #b0001) #b1111))
+(assert (= (bvnor  #b1010 #b0001) #b0100))
+(assert (= (bvxor  #b1010 #b1001) #b0011))
+(assert (= (bvxnor  #b1010 #b1001) #b1100))
+
+(assert (= (bvneg  (_ bv4 3)) (_ bv4 3)))
+(assert (= (bvneg  (_ bv3 3)) (_ bv5 3)))
+
+(assert (= (bvcomp  (_ bv3 3) (_ bv5 3)) #b0))
+(assert (= (bvcomp  (_ bv4 3) (_ bv4 3)) #b1))
+
+(assert (= (bvadd  (_ bv3 2) (_ bv2 2)) (_ bv1 2)))
+(assert (= (bvmul  (_ bv3 2) (_ bv2 2)) (_ bv2 2)))
+
+
+(assert (= (bvudiv  (_ bv3 2) (_ bv2 2)) (_ bv1 2)))
+(assert (= (bvsdiv  (_ bv3 2) (_ bv2 2)) (_ bv0 2)))
+
+(assert (= (bvudiv  (_ bv7 3) (_ bv0 3)) (_ bv7 3)))
+(assert (= (bvudiv  (_ bv7 3) (_ bv1 3)) (_ bv7 3)))
+(assert (= (bvudiv  (_ bv7 3) (_ bv2 3)) (_ bv3 3)))
+(assert (= (bvudiv  (_ bv7 3) (_ bv3 3)) (_ bv2 3)))
+(assert (= (bvudiv  (_ bv7 3) (_ bv4 3)) (_ bv1 3)))
+(assert (= (bvudiv  (_ bv7 3) (_ bv5 3)) (_ bv1 3)))
+(assert (= (bvudiv  (_ bv7 3) (_ bv6 3)) (_ bv1 3)))
+(assert (= (bvudiv  (_ bv7 3) (_ bv7 3)) (_ bv1 3)))
+
+(assert (= (bvurem  (_ bv7 3) (_ bv0 3)) (_ bv7 3)))
+(assert (= (bvurem  (_ bv7 3) (_ bv1 3)) (_ bv0 3)))
+(assert (= (bvurem  (_ bv7 3) (_ bv2 3)) (_ bv1 3)))
+(assert (= (bvurem  (_ bv7 3) (_ bv3 3)) (_ bv1 3)))
+(assert (= (bvurem  (_ bv7 3) (_ bv4 3)) (_ bv3 3)))
+(assert (= (bvurem  (_ bv7 3) (_ bv5 3)) (_ bv2 3)))
+(assert (= (bvurem  (_ bv7 3) (_ bv6 3)) (_ bv1 3)))
+(assert (= (bvurem  (_ bv7 3) (_ bv7 3)) (_ bv0 3)))
+
+(assert (= (bvsdiv  (_ bv7 3) (_ bv0 3)) (_ bv1 3)))
+(assert (= (bvsdiv  (_ bv7 3) (_ bv1 3)) (_ bv7 3)))
+(assert (= (bvsdiv  (_ bv7 3) (_ bv2 3)) (_ bv0 3)))
+(assert (= (bvsdiv  (_ bv7 3) (_ bv3 3)) (_ bv0 3)))
+(assert (= (bvsdiv  (_ bv7 3) (_ bv4 3)) (_ bv0 3)))
+(assert (= (bvsdiv  (_ bv7 3) (_ bv5 3)) (_ bv0 3)))
+(assert (= (bvsdiv  (_ bv7 3) (_ bv6 3)) (_ bv0 3)))
+(assert (= (bvsdiv  (_ bv7 3) (_ bv7 3)) (_ bv1 3)))
+
+(assert (= (bvsdiv  (_ bv4 3) (_ bv0 3)) (_ bv1 3)))
+(assert (= (bvsdiv  (_ bv4 3) (_ bv1 3)) (_ bv4 3)))
+(assert (= (bvsdiv  (_ bv4 3) (_ bv2 3)) (_ bv6 3)))
+(assert (= (bvsdiv  (_ bv4 3) (_ bv3 3)) (_ bv7 3)))
+(assert (= (bvsdiv  (_ bv4 3) (_ bv4 3)) (_ bv1 3)))
+(assert (= (bvsdiv  (_ bv4 3) (_ bv5 3)) (_ bv1 3)))
+(assert (= (bvsdiv  (_ bv4 3) (_ bv6 3)) (_ bv2 3)))
+(assert (= (bvsdiv  (_ bv4 3) (_ bv7 3)) (_ bv4 3)))
+
+(assert (= (bvsrem  (_ bv4 3) (_ bv0 3)) (_ bv4 3)))
+(assert (= (bvsrem  (_ bv4 3) (_ bv1 3)) (_ bv0 3)))
+(assert (= (bvsrem  (_ bv4 3) (_ bv2 3)) (_ bv0 3)))
+(assert (= (bvsrem  (_ bv4 3) (_ bv3 3)) (_ bv7 3)))
+(assert (= (bvsrem  (_ bv4 3) (_ bv4 3)) (_ bv0 3)))
+(assert (= (bvsrem  (_ bv4 3) (_ bv5 3)) (_ bv7 3)))
+(assert (= (bvsrem  (_ bv4 3) (_ bv6 3)) (_ bv0 3)))
+(assert (= (bvsrem  (_ bv4 3) (_ bv7 3)) (_ bv0 3)))
+
+(assert (= (bvsmod  (_ bv4 3) (_ bv0 3)) (_ bv4 3)))
+(assert (= (bvsmod  (_ bv4 3) (_ bv1 3)) (_ bv0 3)))
+(assert (= (bvsmod  (_ bv4 3) (_ bv2 3)) (_ bv0 3)))
+(assert (= (bvsmod  (_ bv4 3) (_ bv3 3)) (_ bv2 3)))
+(assert (= (bvsmod  (_ bv4 3) (_ bv4 3)) (_ bv0 3)))
+(assert (= (bvsmod  (_ bv4 3) (_ bv5 3)) (_ bv7 3)))
+(assert (= (bvsmod  (_ bv4 3) (_ bv6 3)) (_ bv0 3)))
+(assert (= (bvsmod  (_ bv4 3) (_ bv7 3)) (_ bv0 3)))
+
+(assert (= (bvshl #b100 #b001) #b000))
+(assert (= (bvlshr #b100 #b001) #b010))
+(assert (= (bvashr #b000 #b001) #b000))
+(assert (= (bvashr #b010 #b001) #b001))
+(assert (= (bvashr #b100 #b001) #b110))
+(assert (= (bvashr #b110 #b001) #b111))
+
+(assert (= ((_ sign_extend 1) #b1000) #b11000))
+(assert (= ((_ sign_extend 1) #b0100) #b00100))
+(assert (= ((_ zero_extend 1) #b1000) #b01000))
+(assert (= ((_ zero_extend 1) #b0100) #b00100))
+
+(assert (= ((_ repeat 1) #b1011) #b1011))
+(assert (= ((_ repeat 2) #b1011) #b10111011))
+
+(assert (= ((_ extract 3 2) #b1011) #b10))
+(assert (= ((_ extract 3 1) #b1011) #b101))
+
+(assert (= ((_ rotate_left 2)  #b1011) #b1110))
+(assert (= ((_ rotate_right 2) #b1011) #b1110))
+(assert (= ((_ rotate_left 1)  #b1011) #b0111))
+(assert (= ((_ rotate_right 1) #b1011) #b1101))
+
+(check-sat)
+(exit)

src_colibri2/tests/solve/smt_bv/unsat/dune

+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps
+  (glob_files *.cnf)
+  (glob_files *.smt2))
+ (action
+  (with-stdout-to
+   dune.inc
+   (run %{exe:../../../generate_tests/generate_dune_tests.exe} . unsat)))
+ (mode promote))

src_colibri2/theories/LRA/realValue.ml

@@ -100,18 +100,46 @@ let init_ty d =
                 else Yield (nodevalue (cst' v), Q.S.add v s))
           in
           Some seq
+      | { app = { builtin = Expr.Bitv n; _ }; _ } ->
+          let open Base.Sequence.Generator in
+          let rec loop i =
+            if Z.numbits i <= n then
+              yield (nodevalue (cst' (Q.of_bigint i))) >>= fun () ->
+              loop (Z.succ i)
+            else return ()
+          in
+          let seq = Interp.SeqLim.of_seq d (run (loop Z.zero)) in
+          Some seq
       | _ -> None)
 
 module Check = struct
   let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
 
+  exception Wrong_arg
+
   let compute_ground d t =
     let ( !> ) t = RealValue.value (RealValue.coerce_nodevalue (interp d t)) in
+    let bitv n t =
+      let t = !>t in
+      if not (Q.is_unsigned_integer n t) then raise Wrong_arg;
+      t.Q.num
+    in
+    let signed_bitv n t = Z.signed_extract (bitv n t) 0 n in
     let ( !< ) v = `Some (RealValue.nodevalue (RealValue.index v)) in
     let ( !<< ) b =
       let r = if b then Boolean.values_true else Boolean.values_false in
       `Some r
     in
+    let extract n t = !<(Q.of_bigint (Z.extract t 0 n)) in
+    let from_bitv n t =
+      let t' = Q.of_bigint t in
+      if not (Q.is_unsigned_integer n t') then
+        Fmt.epr "@[[BV] %s(%a) is not of size %i@]@."
+          (Z.format (Fmt.str "%%0+#%ib" n) t)
+          Z.pp_print t n;
+      assert (Q.is_unsigned_integer n t');
+      !<t'
+    in
     match Ground.sem t with
     | {
      app = { builtin = Expr.Coercion };
@@ -171,27 +199,182 @@ module Check = struct
       ->
         let a = IArray.extract1_exn args in
         !<(Q.abs !>a)
+    | { app = { builtin = Expr.Bitvec s }; tyargs = []; args; ty = _ } ->
+        assert (IArray.is_empty args);
+        from_bitv (String.length s) (Z.of_string_base 2 s)
+    | { app = { builtin = Expr.Bitv_concat (n, m) }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        from_bitv (n + m) (Z.logor (Z.shift_left (bitv n a) m) (bitv m b))
+    | { app = { builtin = Expr.Bitv_extract (n, i, j) }; tyargs = []; args; _ }
+      ->
+        let a = IArray.extract1_exn args in
+        from_bitv (i - j + 1) (Z.extract (bitv n a) j (i - j + 1))
+    | { app = { builtin = Expr.Bitv_repeat (n, k) }; tyargs = []; args; _ } ->
+        let a = IArray.extract1_exn args in
+        let rec loop n k acc z =
+          if k = 0 then acc
+          else
+            let acc = Z.logor (Z.shift_left acc n) z in
+            loop n (k - 1) acc z
+        in
+        let a = bitv n a in
+        from_bitv (n * k) (loop n k Z.zero a)
+    | { app = { builtin = Expr.Bitv_zero_extend (n, k) }; tyargs = []; args; _ }
+      ->
+        let a = IArray.extract1_exn args in
+        from_bitv (n + k) (bitv n a)
+    | { app = { builtin = Expr.Bitv_sign_extend (n, k) }; tyargs = []; args; _ }
+      ->
+        let a = IArray.extract1_exn args in
+        let a = bitv n a in
+        if Z.testbit a (n - 1) then
+          extract (n + k) (Z.logor (Z.shift_left Z.minus_one n) a)
+        else from_bitv (n + k) a
+    | { app = { builtin = Expr.Bitv_rotate_left (n, k) }; tyargs = []; args; _ }
+      ->
+        let a = IArray.extract1_exn args in
+        let a = bitv n a in
+        let k = k mod n in
+        extract n (Z.logor (Z.shift_left a k) (Z.extract a (n - k) k))
+    | {
+     app = { builtin = Expr.Bitv_rotate_right (n, k) };
+     tyargs = [];
+     args;
+     _;
+    } ->
+        let a = IArray.extract1_exn args in
+        let a = bitv n a in
+        let k = k mod n in
+        extract n (Z.logor (Z.shift_left a (n - k)) (Z.shift_right a k))
+    | { app = { builtin = Expr.Bitv_not n }; tyargs = []; args; _ } ->
+        let a = IArray.extract1_exn args in
+        extract n (Z.lognot (bitv n a))
+    | { app = { builtin = Expr.Bitv_and n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        from_bitv n (Z.logand (bitv n a) (bitv n b))
+    | { app = { builtin = Expr.Bitv_or n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        from_bitv n (Z.logor (bitv n a) (bitv n b))
+    | { app = { builtin = Expr.Bitv_nand n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        extract n (Z.lognot (Z.logand (bitv n a) (bitv n b)))
+    | { app = { builtin = Expr.Bitv_nor n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        extract n (Z.lognot (Z.logor (bitv n a) (bitv n b)))
+    | { app = { builtin = Expr.Bitv_xor n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        extract n (Z.logxor (bitv n a) (bitv n b))
+    | { app = { builtin = Expr.Bitv_xnor n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        extract n (Z.logxor (bitv n a) (Z.lognot (bitv n b)))
+    | { app = { builtin = Expr.Bitv_comp n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        if Z.equal (bitv n a) (bitv n b) then extract 1 Z.minus_one
+        else from_bitv 1 Z.zero
+    | { app = { builtin = Expr.Bitv_neg n }; tyargs = []; args; _ } ->
+        let a = IArray.extract1_exn args in
+        from_bitv n (Z.sub (Z.shift_left Z.one n) (bitv n a))
+    | { app = { builtin = Expr.Bitv_add n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        extract n (Z.add (bitv n a) (bitv n b))
+    | { app = { builtin = Expr.Bitv_mul n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        extract n (Z.mul (bitv n a) (bitv n b))
+    | { app = { builtin = Expr.Bitv_udiv n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        let b = bitv n b in
+        if Z.equal b Z.zero then extract n Z.minus_one
+        else extract n (Z.div (bitv n a) b)
+    | { app = { builtin = Expr.Bitv_urem n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        let b = bitv n b in
+        if Z.equal b Z.zero then from_bitv n (bitv n a)
+        else extract n (Z.rem (bitv n a) b)
+    | { app = { builtin = Expr.Bitv_sdiv n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        let b = signed_bitv n b in
+        if Z.equal b Z.zero then extract n Z.one
+        else extract n (Z.div (signed_bitv n a) b)
+    | { app = { builtin = Expr.Bitv_srem n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        let b = signed_bitv n b in
+        if Z.equal b Z.zero then from_bitv n (bitv n a)
+        else extract n (Z.rem (signed_bitv n a) b)
+    | { app = { builtin = Expr.Bitv_smod n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        let b = signed_bitv n b in
+        let a = signed_bitv n a in
+        if Z.equal b Z.zero then `Uninterp
+        else extract n (Z.sub a (Z.mul (Z.fdiv a b) b))
+    | { app = { builtin = Expr.Bitv_shl n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        let b = bitv n b in
+        if Z.leq (Z.of_int n) b then from_bitv n Z.zero
+        else extract n (Z.shift_left (bitv n a) (Z.to_int b))
+    | { app = { builtin = Expr.Bitv_lshr n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        let b = bitv n b in
+        if Z.leq (Z.of_int n) b then from_bitv n Z.zero
+        else extract n (Z.shift_right (bitv n a) (Z.to_int b))
+    | { app = { builtin = Expr.Bitv_ashr n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        let b = bitv n b in
+        let b = if Z.leq (Z.of_int n) b then n else Z.to_int b in
+        extract n (Z.shift_right (signed_bitv n a) b)
+    | { app = { builtin = Expr.Bitv_ult n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        !<<(Z.lt (bitv n a) (bitv n b))
+    | { app = { builtin = Expr.Bitv_ule n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        !<<(Z.leq (bitv n a) (bitv n b))
+    | { app = { builtin = Expr.Bitv_ugt n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        !<<(Z.gt (bitv n a) (bitv n b))
+    | { app = { builtin = Expr.Bitv_uge n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        !<<(Z.geq (bitv n a) (bitv n b))
+    | { app = { builtin = Expr.Bitv_slt n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        !<<(Z.lt (signed_bitv n a) (signed_bitv n b))
+    | { app = { builtin = Expr.Bitv_sle n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        !<<(Z.leq (signed_bitv n a) (signed_bitv n b))
+    | { app = { builtin = Expr.Bitv_sgt n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        !<<(Z.gt (signed_bitv n a) (signed_bitv n b))
+    | { app = { builtin = Expr.Bitv_sge n }; tyargs = []; args; _ } ->
+        let a, b = IArray.extract2_exn args in
+        !<<(Z.geq (signed_bitv n a) (signed_bitv n b))
     | _ -> `None
 
   let init d =
     Interp.Register.check d (fun d t ->
-        if
-          Ground.Ty.equal Ground.Ty.int (Ground.sem t).ty
-          && Base.Option.for_all
-               ~f:(fun q -> not (Q.is_integer (RealValue.value q)))
-               (RealValue.of_nodevalue (interp d (Ground.node t)))
-        then Wrong
-        else
-          let check r = Value.equal r (interp d (Ground.node t)) in
-          match compute_ground d t with
-          | `None -> NA
-          | `Some v -> Interp.check_of_bool (check v)
-          | `Uninterp ->
-              Interp.check_of_bool
-                (Colibri2_theories_quantifiers.Uninterp.On_uninterpreted_domain
-                 .check d t));
+        match
+          ( (Ground.sem t).ty.app,
+            RealValue.of_nodevalue (interp d (Ground.node t)) )
+        with
+        | { builtin = Expr.Int; _ }, None -> Wrong
+        | { builtin = Expr.Int; _ }, Some v
+          when not (Q.is_integer (RealValue.value v)) ->
+            Wrong
+        | { builtin = Expr.Bitv _; _ }, None -> Wrong
+        | { builtin = Expr.Bitv n; _ }, Some v
+          when not (Q.is_unsigned_integer n (RealValue.value v)) ->
+            Wrong
+        | _ -> (
+            let check r = Value.equal r (interp d (Ground.node t)) in
+            match compute_ground d t with
+            | exception Wrong_arg -> Wrong
+            | `None -> NA
+            | `Some v -> Interp.check_of_bool (check v)
+            | `Uninterp ->
+                Interp.check_of_bool
+                  (Colibri2_theories_quantifiers.Uninterp
+                   .On_uninterpreted_domain
+                   .check d t)));
     Interp.Register.compute d (fun d t ->
         match compute_ground d t with
+        | exception Wrong_arg -> raise Impossible
         | `None -> NA
         | `Some v -> Value v
         | `Uninterp ->
@@ -201,6 +384,7 @@ module Check = struct
   let attach d g =
     let f d g =
       match compute_ground d g with
+      | exception Wrong_arg -> Egraph.contradiction d
       | `None -> raise Impossible
       | `Some v -> Egraph.set_value d (Ground.node g) v
       | `Uninterp ->
@@ -353,6 +537,175 @@ let converter d (f : Ground.t) =
       let a = IArray.extract1_exn args in
       reg a;
       Check.attach d f
+  | { app = { builtin = Expr.Bitvec s }; tyargs = []; args; ty = _ } ->
+      assert (IArray.is_empty args);
+      merge (cst (Q.of_bigint (Z.of_string_base 2 s)))
+  | { app = { builtin = Expr.Bitv_concat (_n, _m) }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_extract (_n, _i, _j) }; tyargs = []; args; _ }
+    ->
+      let a = IArray.extract1_exn args in
+      reg a;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_repeat (_n, _k) }; tyargs = []; args; _ } ->
+      let a = IArray.extract1_exn args in
+      reg a;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_zero_extend (_n, _k) }; tyargs = []; args; _ }
+    ->
+      let a = IArray.extract1_exn args in
+      reg a;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_sign_extend (_n, _k) }; tyargs = []; args; _ }
+    ->
+      let a = IArray.extract1_exn args in
+      reg a;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_rotate_left (_n, _k) }; tyargs = []; args; _ }
+    ->
+      let a = IArray.extract1_exn args in
+      reg a;
+      Check.attach d f
+  | {
+   app = { builtin = Expr.Bitv_rotate_right (_n, _k) };
+   tyargs = [];
+   args;
+   _;
+  } ->
+      let a = IArray.extract1_exn args in
+      reg a;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_not _n }; tyargs = []; args; _ } ->
+      let a = IArray.extract1_exn args in
+      reg a;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_and _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_or _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_nand _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_nor _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_xnor _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_comp _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_neg _n }; tyargs = []; args; _ } ->
+      let a = IArray.extract1_exn args in
+      reg a;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_add _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_mul _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_udiv _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_urem _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_sdiv _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_srem _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_smod _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_shl _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_lshr _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_ashr _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_ult _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_ule _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_ugt _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_uge _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_slt _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_sle _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_sgt _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
+  | { app = { builtin = Expr.Bitv_sge _n }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f
   | _ -> ()
 
 let init env =