4 files changed, 5 insertions, 8 deletions
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index c8cee6ab..e54a2d7a 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -1153,8 +1153,6 @@ let rec sgen_cval = function
 and sgen_call op cvals =
   let open Printf in
   match op, cvals with
-  | Bit_to_bool, [v] ->
-     sprintf "((bool) %s)" (sgen_cval v)
   | Bnot, [v] -> "!(" ^ sgen_cval v ^ ")"
   | List_hd, [v] ->
      sprintf "(%s).hd" ("*" ^ sgen_cval v)
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 051f5c19..52e0865a 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -362,8 +362,11 @@ let rec compile_aval l ctx = function
        | V_lit (VL_bit Sail2_values.B1, _) ->
           [icopy l (CL_id (gs, ctyp)) (V_call (Bvor, [V_id (gs, ctyp); V_lit (mask i, ctyp)]))]
        | _ ->
-          (* FIXME: Make this work in C *)
-          setup @ [iif (V_call (Bit_to_bool, [cval])) [icopy l (CL_id (gs, ctyp)) (V_call (Bvor, [V_id (gs, ctyp); V_lit (mask i, ctyp)]))] [] CT_unit] @ cleanup
+          setup
+          @ [iextern (CL_id (gs, ctyp))
+                     (mk_id "update_fbits", [])
+                     [V_id (gs, ctyp); V_lit (VL_int (Big_int.of_int i), CT_fint 64); cval]]
+          @ cleanup
      in
      [idecl ctyp gs;
       icopy l (CL_id (gs, ctyp)) (V_lit (VL_bits (Util.list_init 64 (fun _ -> Sail2_values.B0), direction), ctyp))]
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 725d2a89..8a700dbd 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -346,8 +346,6 @@ let rec smt_cval ctx cval =
         Fn ("not", [Fn ("=", [smt_cval ctx cval1; smt_cval ctx cval2])])
      | V_call (Bvor, [cval1; cval2]) ->
         Fn ("bvor", [smt_cval ctx cval1; smt_cval ctx cval2])
-     | V_call (Bit_to_bool, [cval]) ->
-        Fn ("=", [smt_cval ctx cval; Bitvec_lit [Sail2_values.B1]])
      | V_call (Eq, [cval1; cval2]) ->
         Fn ("=", [smt_cval ctx cval1; smt_cval ctx cval2])
      | V_call (Bnot, [cval]) ->
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index d24e6b8a..0b551416 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -275,7 +275,6 @@ let string_of_op = function
   | Bor -> "@or"
   | List_hd -> "@hd"
   | List_tl -> "@tl"
-  | Bit_to_bool -> "@bit_to_bool"
   | Eq -> "@eq"
   | Neq -> "@neq"
   | Bvnot -> "@bvnot"
@@ -831,7 +830,6 @@ let label str =
 
 let rec infer_call op vs =
   match op, vs with
-  | Bit_to_bool, _ -> CT_bool
   | Bnot, _ -> CT_bool
   | Band, _ -> CT_bool
   | Bor, _ -> CT_bool