Treat integer casts in a general manner

1 files changed, 6 insertions, 0 deletions

diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 3ac68365..42479a6e 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -1177,6 +1177,12 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression)
             in
             (ctx, Unop (Neg int_ty), effect_info, args, None)
         | _ -> raise (Failure "Unreachable"))
+    | S.Unop (E.Cast (src_ty, tgt_ty)) ->
+        (* Note that cast can fail *)
+        let effect_info =
+          { can_fail = true; input_state = false; output_state = false }
+        in
+        (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, None)
     | S.Binop binop -> (
         match args with
         | [ arg0; arg1 ] ->