From a5f87ba02342ae0b96fe0d8ba16f1ec78469d760 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Fri, 22 Sep 2023 16:48:37 +0200
Subject: Allow bitshifts with any pair of integer types

---
 compiler/SymbolicToPure.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 3512270a..08f67592 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1542,7 +1542,11 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
         | [ arg0; arg1 ] ->
             let int_ty0 = ty_as_integer arg0.ty in
             let int_ty1 = ty_as_integer arg1.ty in
-            assert (int_ty0 = int_ty1);
+            (match binop with
+            (* The Rust compiler accepts bitshifts for any integer type combination for ty0, ty1 *)
+            | E.Shl | E.Shr -> ()
+            | _ -> assert (int_ty0 = int_ty1)
+            );
             let effect_info =
               {
                 can_fail = ExpressionsUtils.binop_can_fail binop;
-- 
cgit v1.2.3