diff --git a/libASL/rASL_check.ml b/libASL/rASL_check.ml
index dd3d7b63..f5315713 100644
--- a/libASL/rASL_check.ml
+++ b/libASL/rASL_check.ml
@@ -114,6 +114,7 @@ module AllowedIntrinsics = struct
       FIdent("slt_bits",0);
       FIdent("sle_bits",0);
       FIdent("sdiv_bits",0);
+      FIdent("udiv_bits",0);
       FIdent("ite",0);
       FIdent("eq_bool",0);
       FIdent("ne_bool",0);
@@ -143,6 +144,7 @@ module AllowedIntrinsics = struct
       FIdent("sub_vec",0);
       FIdent("mul_vec",0);
       FIdent("sdiv_vec",0);
+      FIdent("udiv_vec",0);
       FIdent("lsr_vec",0);
       FIdent("asr_vec",0);
       FIdent("lsl_vec",0);
diff --git a/libASL/scala_backend.ml b/libASL/scala_backend.ml
index e089bfe7..261d7355 100644
--- a/libASL/scala_backend.ml
+++ b/libASL/scala_backend.ml
@@ -59,7 +59,7 @@ module StringSet = Set.Make(String)
         "f_gen_load"; "f_gen_SignExtend"; "f_gen_ZeroExtend"; "f_gen_add_bits";
         "f_gen_and_bits"; "f_gen_and_bool"; "f_gen_asr_bits"; "f_gen_lsl_bits";
         "f_gen_lsr_bits"; "f_gen_mul_bits"; "f_gen_ne_bits"; "f_gen_not_bits";
-        "f_gen_not_bool"; "f_gen_or_bits"; "f_gen_or_bool"; "f_gen_sdiv_bits";
+        "f_gen_not_bool"; "f_gen_or_bits"; "f_gen_or_bool"; "f_gen_sdiv_bits"; "f_gen_udiv_bits";
         "f_gen_sle_bits"; "f_gen_slt_bits"; "f_gen_sub_bits";
         "f_gen_AArch64_MemTag_read"; "f_gen_AArch64_MemTag_set"; "f_gen_Mem_read"; "f_gen_slice";
         "f_gen_replicate_bits"; "f_gen_append_bits"; "f_gen_array_load";
diff --git a/libASL/symbolic.ml b/libASL/symbolic.ml
index eb7fd3df..e5d8a99c 100644
--- a/libASL/symbolic.ml
+++ b/libASL/symbolic.ml
@@ -942,6 +942,7 @@ let prims_pure () =
     FIdent("slt_bits",0);
     FIdent("sle_bits",0);
     FIdent("sdiv_bits",0);
+    FIdent("udiv_bits",0);
     FIdent("ite",0);
   ] @ (if !use_vectoriser then [
     FIdent("Elem.set",0);
@@ -950,6 +951,7 @@ let prims_pure () =
     FIdent("sub_vec",0);
     FIdent("mul_vec",0);
     FIdent("sdiv_vec",0);
+    FIdent("udiv_vec",0);
     FIdent("lsr_vec",0);
     FIdent("asr_vec",0);
     FIdent("lsl_vec",0);
diff --git a/libASL/transforms.ml b/libASL/transforms.ml
index fceeaa49..b50a8765 100644
--- a/libASL/transforms.ml
+++ b/libASL/transforms.ml
@@ -73,6 +73,7 @@ let infer_type (e: expr): ty option =
     | "sub_bits"           -> Some(Type_Bits(num))
     | "mul_bits"           -> Some(Type_Bits(num))
     | "sdiv_bits"          -> Some(Type_Bits(num))
+    | "udiv_bits"          -> Some(Type_Bits(num))
     | "and_bits"           -> Some(Type_Bits(num))
     | "or_bits"            -> Some(Type_Bits(num))
     | "eor_bits"           -> Some(Type_Bits(num))
@@ -356,10 +357,16 @@ module StatefulIntToBits = struct
   let wrapper_ident = FIdent ("StatefulIntToBit_wrapper", 0)
 
   let build_div x y =
-    let w = abs_of_div (snd x) (snd y) in
-    let ex = extend w in
-    let f = sym_prim (FIdent ("sdiv_bits", 0)) [sym_of_abs w] [ex x; ex y] in
-    (f,w)
+    if signed (snd x) || signed (snd y) then
+      let w = abs_of_div (snd x) (snd y) in
+      let ex = extend w in
+      let f = sym_prim (FIdent ("sdiv_bits", 0)) [sym_of_abs w] [ex x; ex y] in
+      (f,w)
+    else
+      let w = merge_abs (snd x) (snd y) in
+      let ex = extend w in
+      let f = sym_prim (FIdent ("udiv_bits", 0)) [sym_of_abs w] [ex x; ex y] in
+      (f,w)
 
   (** Covert an integer expression tree into a bitvector equivalent *)
   let rec bv_of_int_expr (st: state) (e: expr): (sym * abs) =
@@ -417,8 +424,8 @@ module StatefulIntToBits = struct
 
     (* Interface only supports zero rounding division at present, force fdiv result to be positive *)
     | Expr_TApply (FIdent ("fdiv_int", 0), [], [x; y]) ->
-        let x = force_signed (bv_of_int_expr st x) in
-        let y = force_signed (bv_of_int_expr st y) in
+        let x = bv_of_int_expr st x in
+        let y = bv_of_int_expr st y in
         assert (is_pos x = is_pos y);
         build_div x y
 
@@ -478,8 +485,8 @@ module StatefulIntToBits = struct
         bv_of_int_expr st (Expr_LitInt n)
 
     | Expr_TApply (FIdent ("divide_real",0), [], [x; y]) ->
-        let x = force_signed (bv_of_real_expr st x) in
-        let y = force_signed (bv_of_real_expr st y) in
+        let x = bv_of_real_expr st x in
+        let y = bv_of_real_expr st y in
         build_div x y
 
     | Expr_TApply (FIdent ("cvt_int_real", 0), [], [x]) ->
@@ -865,6 +872,7 @@ module IntToBits = struct
       | FIdent ("sub_bits", 0), [Expr_LitInt n], _
       | FIdent ("mul_bits", 0), [Expr_LitInt n], _
       | FIdent ("sdiv_bits", 0), [Expr_LitInt n], _
+      | FIdent ("udiv_bits", 0), [Expr_LitInt n], _
       | FIdent ("and_bits", 0), [Expr_LitInt n], _
       | FIdent ("or_bits", 0), [Expr_LitInt n], _
       | FIdent ("eor_bits", 0), [Expr_LitInt n], _
@@ -1830,7 +1838,7 @@ module type ScopedBindings = sig
     val add_bind : 'elt t  -> ident -> 'elt -> unit
     val find_binding : 'elt t -> ident -> 'elt option
     val current_scope_bindings : 'elt t -> 'elt Bindings.t
-    val init: unit -> 'elt t  
+    val init: unit -> 'elt t
 end
 
 module ScopedBindings : ScopedBindings = struct
@@ -2182,7 +2190,7 @@ end
 module BDDSimp = struct
   let log = false
 
-  type abs = 
+  type abs =
     Top |
     Val of MLBDD.t list |
     Bot
@@ -2196,9 +2204,9 @@ module BDDSimp = struct
 
   module type Lattice = RTAnalysisLattice with type olt = state
 
-  module NopAnalysis = struct  
+  module NopAnalysis = struct
     type rt = unit
-    type olt = state 
+    type olt = state
     let xfer_stmt o r s = r,[s]
     let join o c j r ro = ()
     let init _ = ()
@@ -2209,7 +2217,7 @@ module BDDSimp = struct
     man = MLBDD.manager ctx;
     vars = Bindings.empty ;
     ctx ;
-    stmts = [] 
+    stmts = []
   }
 
 
@@ -2262,7 +2270,7 @@ module BDDSimp = struct
 
   let to_bool abs st =
     match abs with
-    | Top 
+    | Top
     | Bot -> MLBDD.dtrue st.man
     | Val [v] -> v
     | _ -> failwith "unexpected to_bool"
@@ -2297,7 +2305,7 @@ module BDDSimp = struct
 
   let wrap_bop f a b =
     match a, b with
-    | Bot, _ 
+    | Bot, _
     | _, Bot -> Bot
     | Top, _
     | _, Top -> Top
@@ -2379,72 +2387,72 @@ module BDDSimp = struct
     match e with
     | Top -> Top
     | Bot -> Bot
-    | Val v -> 
+    | Val v ->
         let start = List.length v - lo - wd in
         Val (sublist v start wd)
 
 
-  let half_add_bit l r = MLBDD.dand l r, MLBDD.xor l r  (* carry, sum *) 
-  let full_add_bit l r carry = 
+  let half_add_bit l r = MLBDD.dand l r, MLBDD.xor l r  (* carry, sum *)
+  let full_add_bit l r carry =
     let c1,s1 = half_add_bit l r in
     let c2,o = half_add_bit s1 carry in
     let ocarry = MLBDD.dor c1 c2 in
     ocarry,o
 
-  let twos_comp_add (xs : MLBDD.t list) (ys: MLBDD.t list) : MLBDD.t * (MLBDD.t list)= 
+  let twos_comp_add (xs : MLBDD.t list) (ys: MLBDD.t list) : MLBDD.t * (MLBDD.t list)=
       let xs = List.rev xs in let ys = List.rev ys in
-      match xs,ys with 
-        | hx::tlx,hy::tly ->  
+      match xs,ys with
+        | hx::tlx,hy::tly ->
           let lscarry,lsb = half_add_bit hx hy in
           let bits,carry = List.fold_left2
-          (fun (acc,carry) (l:MLBDD.t) (r:MLBDD.t)  -> let carry,o = (full_add_bit l r carry) in o::acc , carry) 
+          (fun (acc,carry) (l:MLBDD.t) (r:MLBDD.t)  -> let carry,o = (full_add_bit l r carry) in o::acc , carry)
             ([lsb], lscarry) tlx tly
           in carry,bits
         | _,_ -> failwith "invalid bit strings"
 
   let signed_add_wrap x y = let _,bits = twos_comp_add x y in bits
 
-  
+
   let addone m xs  = let one = MLBDD.dtrue m in
       let xs = List.rev xs  in
-      let c,rs = match xs with 
-        | hx::tlx ->  
+      let c,rs = match xs with
+        | hx::tlx ->
           let lscarry,lsb = half_add_bit hx one in
           let bits,carry = List.fold_left
-            (fun (acc,carry) (l:MLBDD.t) -> let carry,o = (half_add_bit l carry) in o::acc, carry) 
+            (fun (acc,carry) (l:MLBDD.t) -> let carry,o = (half_add_bit l carry) in o::acc, carry)
             ([lsb], lscarry) tlx
           in carry,bits
         | _ -> failwith "no"
       in rs
-    
+
 
   let signed_negation m (x:MLBDD.t list) =  addone m (List.map MLBDD.dnot x)
 
   let signed_sub_wrap m x y = let _,bits = twos_comp_add x (signed_negation m y) in bits
 
 (*
-  let signed_lt m x y =  
+  let signed_lt m x y =
 
   let signed_gt m x y = List.map MLBDD.dnot (signed_lt m x y)
   *)
 
 
 
-  let eq_bvs a b = 
+  let eq_bvs a b =
     let bits = List.map2 MLBDD.eq a b in
     match bits with
       | x::xs -> List.fold_right MLBDD.dand xs x
       | _ -> failwith "bad bits width"
 
-    let sle_bits m x y = 
-      MLBDD.dor 
+    let sle_bits m x y =
+      MLBDD.dor
         (MLBDD.dand (List.hd x) (MLBDD.dnot (List.hd y)))
         (MLBDD.dnot (MLBDD.xor (List.hd x) (List.hd y)) )
 
   (* https://cs.nyu.edu/pipermail/smt-lib/2007/000182.html *)
 
   let unknown_prims = ref Bindings.empty
-  let print_unknown_prims (c:unit) = if log then (Bindings.to_seq !unknown_prims |> List.of_seq |> List.sort (fun a b -> compare (snd a) (snd b)) 
+  let print_unknown_prims (c:unit) = if log then (Bindings.to_seq !unknown_prims |> List.of_seq |> List.sort (fun a b -> compare (snd a) (snd b))
     |> List.iter (fun (id,c) -> Printf.printf "%d \t : %s\n" c (pprint_ident id)))
 
   let eq_bit a b = MLBDD.dnot (MLBDD.xor a b)
@@ -2456,23 +2464,23 @@ module BDDSimp = struct
       (MLBDD.dfalse m, MLBDD.dtrue m) (s) (t))
   in (MLBDD.dand a b)
 
-  let bvult m x y : MLBDD.t = bvugt m y x 
+  let bvult m x y : MLBDD.t = bvugt m y x
   let bvule m x y = MLBDD.dor (bvult m x y) (eq_bvs x y)
   let bvuge m x y = MLBDD.dor (bvugt m x y) (eq_bvs x y)
 
-  let bvslt m x y = MLBDD.dor 
+  let bvslt m x y = MLBDD.dor
     (MLBDD.dand (List.hd x) (MLBDD.dnot (List.hd y)))
     (MLBDD.dand (eq_bit (List.hd x) (List.hd y)) (bvult m x y))
 
   let bvsgt m x y = bvslt m y x
 
-  let bvsle m x y = MLBDD.dor 
+  let bvsle m x y = MLBDD.dor
     (MLBDD.dand (List.hd x) (MLBDD.dnot (List.hd y)))
     (MLBDD.dand (eq_bit (List.hd x) (List.hd y)) (bvule m x y))
 
-  let bvsge m x y = bvsle m y x 
+  let bvsge m x y = bvsle m y x
 
-  let wrap_bv_bool f m x y  =  match x , y with 
+  let wrap_bv_bool f m x y  =  match x , y with
       | Val x, Val y -> Val [(f m x y)]
       | _,_ -> Top
 
@@ -2483,7 +2491,7 @@ module BDDSimp = struct
 
   let twos_comp_sub man (xs : MLBDD.t list) (ys: MLBDD.t list) = ()
 
-  let replicate_bits newlen bits = match bits with 
+  let replicate_bits newlen bits = match bits with
     | Val bits -> if Int.rem newlen (List.length bits) <> 0 then failwith "indivisible rep length"  ;
       let repeats = newlen / (List.length bits) in Val (List.concat (List.init repeats (fun i -> bits)))
     | _ -> Top
@@ -2493,7 +2501,7 @@ module BDDSimp = struct
   (****************************************************************)
 
 
-  let eval_prim f tes es st = 
+  let eval_prim f tes es st =
     match f, tes, es with
     | "and_bool", [], [x; y] -> and_bool x y
     | "or_bool",  [], [x; y] -> or_bool x y
@@ -2515,20 +2523,20 @@ module BDDSimp = struct
         zero_extend_bits x (int_of_string nw) st
     | "SignExtend", [w;Expr_LitInt nw], [x; y] ->
         sign_extend_bits x (int_of_string nw) st
-      
-    | "add_bits", [Expr_LitInt w], [x; y] -> (match x,y with 
+
+    | "add_bits", [Expr_LitInt w], [x; y] -> (match x,y with
       | Val x, Val y -> let r = (signed_add_wrap x y) in assert (List.length r == (int_of_string w)); Val r
         | _,_ -> Top)
-    | "sub_bits", [w], [x; y] -> (match x,y with 
+    | "sub_bits", [w], [x; y] -> (match x,y with
         | Val x, Val y -> Val (signed_add_wrap x (signed_negation st.man y))
-        | _,_ -> Top) 
-        
-    | "ule_bits", [w], [x; y] -> wrap_bv_bool bvule st.man x y  
-    | "uge_bits", [w], [x; y] -> wrap_bv_bool bvuge st.man x y  
-    | "sle_bits", [w], [x; y] -> wrap_bv_bool bvsle st.man x y  
-    | "sge_bits", [w], [x; y] -> wrap_bv_bool bvsge st.man x y  
-    | "slt_bits", [w], [x; y] -> wrap_bv_bool bvslt st.man x y  
-    | "sgt_bits", [w], [x; y] -> wrap_bv_bool bvsgt st.man x y  
+        | _,_ -> Top)
+
+    | "ule_bits", [w], [x; y] -> wrap_bv_bool bvule st.man x y
+    | "uge_bits", [w], [x; y] -> wrap_bv_bool bvuge st.man x y
+    | "sle_bits", [w], [x; y] -> wrap_bv_bool bvsle st.man x y
+    | "sge_bits", [w], [x; y] -> wrap_bv_bool bvsge st.man x y
+    | "slt_bits", [w], [x; y] -> wrap_bv_bool bvslt st.man x y
+    | "sgt_bits", [w], [x; y] -> wrap_bv_bool bvsgt st.man x y
 
     (*
 
@@ -2538,8 +2546,8 @@ module BDDSimp = struct
     | "mul_bits", _, [x; y] -> Top
       *)
 
-    | _, _, _ -> 
-        unknown_prims  :=  (Bindings.find_opt (Ident f) !unknown_prims) |> (function Some x -> x + 1 | None -> 0) 
+    | _, _, _ ->
+        unknown_prims  :=  (Bindings.find_opt (Ident f) !unknown_prims) |> (function Some x -> x + 1 | None -> 0)
             |> (fun x -> Bindings.add (Ident f) x !unknown_prims) ;
         Top
 
@@ -2547,7 +2555,7 @@ module BDDSimp = struct
     match e with
     | Expr_Var (Ident "TRUE") -> Val ([ MLBDD.dtrue st.man ])
     | Expr_Var (Ident "FALSE") -> Val ([ MLBDD.dfalse st.man ])
-    | Expr_LitBits b -> 
+    | Expr_LitBits b ->
         Val (String.fold_right (fun c acc ->
           match c with
           | '1' -> (MLBDD.dtrue st.man)::acc
@@ -2580,7 +2588,7 @@ module BDDSimp = struct
     | Expr_LitString _ -> if log then Printf.printf "unexpected Expr_LitString %s" (pp_expr e); Top
     | Expr_If _ -> if log then Printf.printf "unexpected Expr_If %s" (pp_expr e); Top
 
-    | _ -> failwith @@ Printf.sprintf "BDDSimp eval_expr: unexpected expr: %s\n"  (pp_expr e)  
+    | _ -> failwith @@ Printf.sprintf "BDDSimp eval_expr: unexpected expr: %s\n"  (pp_expr e)
 
   (****************************************************************)
   (** Stmt Walk                                                   *)
@@ -2591,7 +2599,7 @@ module BDDSimp = struct
 
   let ctx_to_mask c =
     let imps = MLBDD.allprime c in
-    match imps with 
+    match imps with
     | x::xs -> List.fold_right join_imps xs x
     | _ -> invalid_arg "ctx_to_mask"
 
@@ -2603,7 +2611,7 @@ module BDDSimp = struct
 
 
   let bdd_to_expr cond st =
-    let bd_to_test b = 
+    let bd_to_test b =
         let bv = Value.to_mask Unknown (Value.from_maskLit b) in
         sym_expr @@ sym_inmask Unknown (Exp (Expr_Var (Ident "enc"))) bv
       in
@@ -2632,18 +2640,18 @@ module BDDSimp = struct
           )
     | _ -> None
 
-  let rebuild_expr e cond st = match bdd_to_expr cond st with 
+  let rebuild_expr e cond st = match bdd_to_expr cond st with
       | Some x -> x
       | None -> if log then Printf.printf "Unable to simplify expr" ; e
 
 
-  class nopvis = object(self) 
+  class nopvis = object(self)
     method xf_stmt (x:stmt) (st:state) : stmt list = [x]
   end
 
   let nop_transform = new nopvis
 
-  module EvalWithXfer (Xf: Lattice) = struct 
+  module EvalWithXfer (Xf: Lattice) = struct
 
   let rec eval_stmt (xs:Xf.rt) (s:stmt) (st:state) =
       (* (transfer : xs, s, st ->  xs', s' ; eval : st -> s -> st' ; write s' : s' , st' -> st'' ) -> xs' s' st''  *)
@@ -2675,7 +2683,7 @@ module BDDSimp = struct
           restrict_ctx abs st, xs
 
     (* State becomes bot - unreachable *)
-    | Stmt_Throw _ -> 
+    | Stmt_Throw _ ->
         if log then Printf.printf "%s : %s\n" (pp_stmt s) (pp_state st);
         let st = writeall ns st in
         halt st,xs
@@ -2684,7 +2692,7 @@ module BDDSimp = struct
     | Stmt_If(c, tstmts, [], fstmts, loc) ->
         let cond = eval_expr c st in
 
-        if is_true cond st then  
+        if is_true cond st then
           eval_stmts xs tstmts st
         else if is_false cond st then
           eval_stmts xs fstmts st
@@ -2703,7 +2711,7 @@ module BDDSimp = struct
 
     (* Can't do anything here *)
     | Stmt_Assign _
-    | Stmt_TCall _ -> 
+    | Stmt_TCall _ ->
         writeall ns st,xs
 
     | _ -> failwith "unknown stmt"
@@ -2717,7 +2725,7 @@ module BDDSimp = struct
     let enc = Val (List.rev (List.init 32 (MLBDD.ithvar st.man))) in
     {st with vars = Bindings.add (Ident "enc") enc st.vars}
 
-  module Eval = EvalWithXfer(NopAnalysis) 
+  module Eval = EvalWithXfer(NopAnalysis)
 
   let just_eval a b c = fst (Eval.eval_stmts (NopAnalysis.init ()) a b)
 
@@ -2777,7 +2785,7 @@ module BDDSimp = struct
     Bindings.mapi (fun nm fnsig ->
       let i = match nm with FIdent(s,_) -> Ident s | s -> s in
       match Bindings.find_opt i st.instrs with
-      | Some reach -> fnsig_upd_body (fun b -> 
+      | Some reach -> fnsig_upd_body (fun b ->
         if log then Printf.printf "transforming %s\n" (pprint_ident nm);
         do_transform nm b reach) fnsig
       | None -> fnsig) instrs
@@ -3152,6 +3160,7 @@ module LoopClassify = struct
     "sub_bits";
     "mul_bits";
     "sdiv_bits";
+    "udiv_bits";
     "sle_bits";
     "slt_bits";
     "eq_bits";
@@ -3470,6 +3479,8 @@ module LoopClassify = struct
         Expr_TApply(FIdent("mul_vec", 0),  [iters; w], vec_args [x; y])
     | "sdiv_bits", 0, [w], [x;y] ->
         Expr_TApply(FIdent("sdiv_vec", 0), [iters; w], vec_args [x; y])
+    | "udiv_bits", 0, [w], [x;y] ->
+        Expr_TApply(FIdent("udiv_vec", 0), [iters; w], vec_args [x; y])
     | "sle_bits", 0, [w], [x;y] ->
         Expr_TApply(FIdent("sle_vec", 0),  [iters; w], vec_args [x; y])
     | "slt_bits", 0, [w], [x;y] ->
diff --git a/offlineASL-cpp/subprojects/aslp-lifter-llvm/include/aslp/llvm_interface.hpp b/offlineASL-cpp/subprojects/aslp-lifter-llvm/include/aslp/llvm_interface.hpp
index 03358cb7..34d38f39 100644
--- a/offlineASL-cpp/subprojects/aslp-lifter-llvm/include/aslp/llvm_interface.hpp
+++ b/offlineASL-cpp/subprojects/aslp-lifter-llvm/include/aslp/llvm_interface.hpp
@@ -394,6 +394,9 @@ class llvm_run_time_interface : virtual public lifter_interface<llvm_lifter_trai
   rt_expr f_gen_sdiv_bits(rt_expr x, rt_expr y) override {
     return builder->CreateSDiv(x, y);
   }
+  rt_expr f_gen_udiv_bits(rt_expr x, rt_expr y) override {
+    return builder->CreateUDiv(x, y);
+  }
   rt_expr f_gen_sle_bits(rt_expr x, rt_expr y) override {
     return builder->CreateICmpSLE(x, y);
   }
diff --git a/offlineASL-cpp/subprojects/aslp-lifter/include/aslp/interface.hpp b/offlineASL-cpp/subprojects/aslp-lifter/include/aslp/interface.hpp
index 54cc5405..07316eb1 100644
--- a/offlineASL-cpp/subprojects/aslp-lifter/include/aslp/interface.hpp
+++ b/offlineASL-cpp/subprojects/aslp-lifter/include/aslp/interface.hpp
@@ -134,6 +134,7 @@ template <typename Traits> class lifter_interface : public Traits {
   virtual rt_expr f_gen_add_bits(rt_expr x, rt_expr y) = 0;
   virtual rt_expr f_gen_sub_bits(rt_expr x, rt_expr y) = 0;
   virtual rt_expr f_gen_sdiv_bits(rt_expr x, rt_expr y) = 0;
+  virtual rt_expr f_gen_udiv_bits(rt_expr x, rt_expr y) = 0;
   virtual rt_expr f_gen_sle_bits(rt_expr x, rt_expr y) = 0;
   virtual rt_expr f_gen_slt_bits(rt_expr x, rt_expr y) = 0;
   virtual rt_expr f_gen_mul_bits(rt_expr x, rt_expr y) = 0;
diff --git a/offlineASL-scala/lifter/src/interface.scala b/offlineASL-scala/lifter/src/interface.scala
index 077a36f6..1e571312 100644
--- a/offlineASL-scala/lifter/src/interface.scala
+++ b/offlineASL-scala/lifter/src/interface.scala
@@ -93,6 +93,7 @@ trait LiftState[RTSym, RTLabel, BV <: RTSym] {
   def f_gen_or_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym
   def f_gen_or_bool(arg0: RTSym, arg1: RTSym): RTSym
   def f_gen_sdiv_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym
+  def f_gen_udiv_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym
   def f_gen_sle_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym
   def f_gen_slt_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym
   def f_gen_sub_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym
diff --git a/offlineASL-scala/main/src/NoneLifter.scala b/offlineASL-scala/main/src/NoneLifter.scala
index e82d471d..2bc63c4e 100644
--- a/offlineASL-scala/main/src/NoneLifter.scala
+++ b/offlineASL-scala/main/src/NoneLifter.scala
@@ -104,6 +104,7 @@ class NotImplementedLifter extends LiftState[RExpr, String, BitVec] {
   def f_gen_or_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError()
   def f_gen_or_bool(arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError()
   def f_gen_sdiv_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError()
+  def f_gen_udiv_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError()
   def f_gen_sle_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError()
   def f_gen_slt_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError()
   def f_gen_sub_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError()
diff --git a/offlineASL/template_offline_utils.ml b/offlineASL/template_offline_utils.ml
index 2fcda9db..874dcd84 100644
--- a/offlineASL/template_offline_utils.ml
+++ b/offlineASL/template_offline_utils.ml
@@ -227,6 +227,8 @@ let f_gen_sub_bits w e1 e2 =
   Expr_TApply (FIdent ("sub_bits", 0), [expr_of_z w], [e1;e2])
 let f_gen_sdiv_bits w e1 e2 =
   Expr_TApply (FIdent ("sdiv_bits", 0), [expr_of_z w], [e1;e2])
+let f_gen_udiv_bits w e1 e2 =
+  Expr_TApply (FIdent ("udiv_bits", 0), [expr_of_z w], [e1;e2])
 let f_gen_sle_bits w e1 e2 =
   Expr_TApply (FIdent ("sle_bits", 0), [expr_of_z w], [e1;e2])
 let f_gen_slt_bits w e1 e2 =
diff --git a/tests/aslt/test_cntlm.t b/tests/aslt/test_cntlm.t
index dc75f7b7..794991b6 100644
--- a/tests/aslt/test_cntlm.t
+++ b/tests/aslt/test_cntlm.t
@@ -17373,7 +17373,7 @@ strip opcode information before passing to antlr.
   Stmt_If(Expr_TApply("eq_bits.0",[32],[Expr_Slices(Expr_Array(Expr_Var("_R"),3),[Slice_LoWd(0,32)]);'00000000000000000000000000000000']),[
   Stmt_Assign(LExpr_Array(LExpr_Var("_R"),1),'0000000000000000000000000000000000000000000000000000000000000000')
   ],[],[
-  Stmt_Assign(LExpr_Array(LExpr_Var("_R"),1),Expr_TApply("ZeroExtend.0",[32;64],[Expr_Slices(Expr_TApply("sdiv_bits.0",[64],[Expr_TApply("ZeroExtend.0",[32;64],[Expr_Slices(Expr_Array(Expr_Var("_R"),1),[Slice_LoWd(0,32)]);64]);Expr_TApply("ZeroExtend.0",[32;64],[Expr_Slices(Expr_Array(Expr_Var("_R"),3),[Slice_LoWd(0,32)]);64])]),[Slice_LoWd(0,32)]);64]))
+  Stmt_Assign(LExpr_Array(LExpr_Var("_R"),1),Expr_TApply("ZeroExtend.0",[32;64],[Expr_TApply("udiv_bits.0",[32],[Expr_Slices(Expr_Array(Expr_Var("_R"),1),[Slice_LoWd(0,32)]);Expr_Slices(Expr_Array(Expr_Var("_R"),3),[Slice_LoWd(0,32)])]);64]))
   ])
   "0x1ac322e3"
   Stmt_Assign(LExpr_Array(LExpr_Var("_R"),3),Expr_TApply("ZeroExtend.0",[32;64],[Expr_TApply("lsl_bits.0",[32;10],[Expr_Slices(Expr_Array(Expr_Var("_R"),23),[Slice_LoWd(0,32)]);Expr_TApply("ZeroExtend.0",[5;10],[Expr_Slices(Expr_Array(Expr_Var("_R"),3),[Slice_LoWd(0,5)]);10])]);64]))
@@ -17439,7 +17439,7 @@ strip opcode information before passing to antlr.
   Stmt_If(Expr_TApply("eq_bits.0",[32],[Expr_Slices(Expr_Array(Expr_Var("_R"),8),[Slice_LoWd(0,32)]);'00000000000000000000000000000000']),[
   Stmt_Assign(LExpr_Array(LExpr_Var("_R"),1),'0000000000000000000000000000000000000000000000000000000000000000')
   ],[],[
-  Stmt_Assign(LExpr_Array(LExpr_Var("_R"),1),Expr_TApply("ZeroExtend.0",[32;64],[Expr_Slices(Expr_TApply("sdiv_bits.0",[64],[Expr_TApply("ZeroExtend.0",[32;64],[Expr_Slices(Expr_Array(Expr_Var("_R"),15),[Slice_LoWd(0,32)]);64]);Expr_TApply("ZeroExtend.0",[32;64],[Expr_Slices(Expr_Array(Expr_Var("_R"),8),[Slice_LoWd(0,32)]);64])]),[Slice_LoWd(0,32)]);64]))
+  Stmt_Assign(LExpr_Array(LExpr_Var("_R"),1),Expr_TApply("ZeroExtend.0",[32;64],[Expr_TApply("udiv_bits.0",[32],[Expr_Slices(Expr_Array(Expr_Var("_R"),15),[Slice_LoWd(0,32)]);Expr_Slices(Expr_Array(Expr_Var("_R"),8),[Slice_LoWd(0,32)])]);64]))
   ])
   "0x1ac82401"
   Stmt_Assign(LExpr_Array(LExpr_Var("_R"),1),Expr_TApply("ZeroExtend.0",[32;64],[Expr_TApply("lsr_bits.0",[32;10],[Expr_Slices(Expr_Array(Expr_Var("_R"),0),[Slice_LoWd(0,32)]);Expr_TApply("ZeroExtend.0",[5;10],[Expr_Slices(Expr_Array(Expr_Var("_R"),8),[Slice_LoWd(0,5)]);10])]);64]))
@@ -17453,13 +17453,13 @@ strip opcode information before passing to antlr.
   Stmt_If(Expr_TApply("eq_bits.0",[32],[Expr_Slices(Expr_Array(Expr_Var("_R"),19),[Slice_LoWd(0,32)]);'00000000000000000000000000000000']),[
   Stmt_Assign(LExpr_Array(LExpr_Var("_R"),2),'0000000000000000000000000000000000000000000000000000000000000000')
   ],[],[
-  Stmt_Assign(LExpr_Array(LExpr_Var("_R"),2),Expr_TApply("ZeroExtend.0",[32;64],[Expr_Slices(Expr_TApply("sdiv_bits.0",[64],[Expr_TApply("ZeroExtend.0",[32;64],[Expr_Slices(Expr_Array(Expr_Var("_R"),2),[Slice_LoWd(0,32)]);64]);Expr_TApply("ZeroExtend.0",[32;64],[Expr_Slices(Expr_Array(Expr_Var("_R"),19),[Slice_LoWd(0,32)]);64])]),[Slice_LoWd(0,32)]);64]))
+  Stmt_Assign(LExpr_Array(LExpr_Var("_R"),2),Expr_TApply("ZeroExtend.0",[32;64],[Expr_TApply("udiv_bits.0",[32],[Expr_Slices(Expr_Array(Expr_Var("_R"),2),[Slice_LoWd(0,32)]);Expr_Slices(Expr_Array(Expr_Var("_R"),19),[Slice_LoWd(0,32)])]);64]))
   ])
   "0x1ad30884"
   Stmt_If(Expr_TApply("eq_bits.0",[32],[Expr_Slices(Expr_Array(Expr_Var("_R"),19),[Slice_LoWd(0,32)]);'00000000000000000000000000000000']),[
   Stmt_Assign(LExpr_Array(LExpr_Var("_R"),4),'0000000000000000000000000000000000000000000000000000000000000000')
   ],[],[
-  Stmt_Assign(LExpr_Array(LExpr_Var("_R"),4),Expr_TApply("ZeroExtend.0",[32;64],[Expr_Slices(Expr_TApply("sdiv_bits.0",[64],[Expr_TApply("ZeroExtend.0",[32;64],[Expr_Slices(Expr_Array(Expr_Var("_R"),4),[Slice_LoWd(0,32)]);64]);Expr_TApply("ZeroExtend.0",[32;64],[Expr_Slices(Expr_Array(Expr_Var("_R"),19),[Slice_LoWd(0,32)]);64])]),[Slice_LoWd(0,32)]);64]))
+  Stmt_Assign(LExpr_Array(LExpr_Var("_R"),4),Expr_TApply("ZeroExtend.0",[32;64],[Expr_TApply("udiv_bits.0",[32],[Expr_Slices(Expr_Array(Expr_Var("_R"),4),[Slice_LoWd(0,32)]);Expr_Slices(Expr_Array(Expr_Var("_R"),19),[Slice_LoWd(0,32)])]);64]))
   ])
   "0x1ad32000"
   Stmt_Assign(LExpr_Array(LExpr_Var("_R"),0),Expr_TApply("ZeroExtend.0",[32;64],[Expr_TApply("lsl_bits.0",[32;10],[Expr_Slices(Expr_Array(Expr_Var("_R"),0),[Slice_LoWd(0,32)]);Expr_TApply("ZeroExtend.0",[5;10],[Expr_Slices(Expr_Array(Expr_Var("_R"),19),[Slice_LoWd(0,5)]);10])]);64]))
@@ -127469,7 +127469,7 @@ strip opcode information before passing to antlr.
   Stmt_If(Expr_TApply("eq_bits.0",[64],[Expr_Array(Expr_Var("_R"),3);'0000000000000000000000000000000000000000000000000000000000000000']),[
   Stmt_Assign(LExpr_Array(LExpr_Var("_R"),2),'0000000000000000000000000000000000000000000000000000000000000000')
   ],[],[
-  Stmt_Assign(LExpr_Array(LExpr_Var("_R"),2),Expr_Slices(Expr_TApply("sdiv_bits.0",[128],[Expr_TApply("ZeroExtend.0",[64;128],[Expr_Array(Expr_Var("_R"),2);128]);Expr_TApply("ZeroExtend.0",[64;128],[Expr_Array(Expr_Var("_R"),3);128])]),[Slice_LoWd(0,64)]))
+  Stmt_Assign(LExpr_Array(LExpr_Var("_R"),2),Expr_TApply("udiv_bits.0",[64],[Expr_Array(Expr_Var("_R"),2);Expr_Array(Expr_Var("_R"),3)]))
   ])
   "0x9ac62042"
   Stmt_Assign(LExpr_Array(LExpr_Var("_R"),2),Expr_TApply("lsl_bits.0",[64;12],[Expr_Array(Expr_Var("_R"),2);Expr_TApply("ZeroExtend.0",[6;12],[Expr_Slices(Expr_Array(Expr_Var("_R"),6),[Slice_LoWd(0,6)]);12])]))
diff --git a/tests/override.asl b/tests/override.asl
index 21205aad..c71b4b15 100644
--- a/tests/override.asl
+++ b/tests/override.asl
@@ -37,6 +37,11 @@ bits(N) sdiv_bits(bits(N) x, bits(N) y)
     integer yn = SInt(y);
     return RoundTowardsZero(Real(xn) / Real (yn))[N-1:0];
 
+bits(N) udiv_bits(bits(N) x, bits(N) y)
+    integer xn = UInt(x);
+    integer yn = UInt(y);
+    return RoundTowardsZero(Real(xn) / Real (yn))[N-1:0];
+
 bits(N1) lsl_bits(bits(N1) x, bits(N2) y)
     integer yn = SInt(y);
     // LSL will assert if yn is negative, but we assume this
@@ -356,6 +361,12 @@ bits(W * N) sdiv_vec(bits(W * N) x, bits(W * N) y, integer N)
     Elem[result, i, W] = sdiv_bits(Elem[x, i, W], Elem[y, i, W]);
   return result;
 
+bits(W * N) udiv_vec(bits(W * N) x, bits(W * N) y, integer N)
+  bits(W * N) result;
+  for i = 0 to (N - 1)
+    Elem[result, i, W] = udiv_bits(Elem[x, i, W], Elem[y, i, W]);
+  return result;
+
 bits(W * N) lsr_vec(bits(W * N) x, bits(W * N) y, integer N)
   bits(W * N) result;
   for i = 0 to (N - 1)