Use Z.(~$1 lsl n) rather than Z.(pow ~$2 n)

src/lib/reasoners/arith.ml

@@ -393,7 +393,7 @@ module Shostak
       begin match P.to_list p with
         | [], c ->
           let c = Q.to_z c in
-          let c = ZA.(erem c @@ pow ~$2 n) in
+          let c = ZA.(erem c @@ ~$1 lsl n) in
           let biv =
             String.init n (fun i ->
                 let i = n - i - 1 in

src/lib/reasoners/bitv.ml

@@ -1150,17 +1150,17 @@ module Shostak(X : ALIEN) = struct
      expression. *)
   let simple_term_to_nat acc st =
     match st.bv with
-    | Cte false -> E.Ints.(acc * ~$Z.(pow ~$2 st.sz))
-    | Cte true -> E.Ints.((acc + ~$$1) * ~$Z.(pow ~$2 st.sz) - ~$$1)
+    | Cte false -> E.Ints.(acc * ~$Z.(~$1 lsl st.sz))
+    | Cte true -> E.Ints.((acc + ~$$1) * ~$Z.(~$1 lsl st.sz) - ~$$1)
     | Other r ->
       let t = term_extract r in
-      E.Ints.(acc * ~$Z.(pow ~$2 st.sz) + E.BV.bv2nat t)
+      E.Ints.(acc * ~$Z.(~$1 lsl st.sz) + E.BV.bv2nat t)
     | Ext (o, _, i, j) ->
       assert (st.sz = j - i + 1);
       let t = term_extract o in
       E.Ints.(
-        acc * ~$Z.(pow ~$2 st.sz) +
-        (E.BV.bv2nat t / ~$Z.(pow ~$2 i)) mod ~$Z.(pow ~$2 st.sz))
+        acc * ~$Z.(~$1 lsl st.sz) +
+        (E.BV.bv2nat t / ~$Z.(~$1 lsl i)) mod ~$Z.(~$1 lsl st.sz))
 
   let abstract_to_nat r =
     List.fold_left simple_term_to_nat (E.Ints.of_int 0) r
@@ -1181,7 +1181,7 @@ module Shostak(X : ALIEN) = struct
           (* bv2nat will *not* simplify: become uninterpreted with interval
              information *)
           let t = E.BV.bv2nat t in
-          X.term_embed t, [ E.Ints.(~$$0 <= t) ; E.Ints.(t < ~$Z.(pow ~$2 n)) ]
+          X.term_embed t, [ E.Ints.(~$$0 <= t) ; E.Ints.(t < ~$Z.(~$1 lsl n)) ]
         | { ty; _ } ->
           Util.internal_error "expected bitv, got %a" Ty.print ty
       end

src/lib/structures/expr.ml

@@ -2970,7 +2970,7 @@ module BV = struct
        are added here, bitv.ml must be updated as well. *)
     match term_view t with
     | { f = Op Int2BV n; xs = [ t ]; _ } ->
-      Ints.(t mod ~$Z.(pow ~$2 n))
+      Ints.(t mod ~$Z.(~$1 lsl n))
     | _ -> mk_term (Op BV2Nat) [t] Tint
 
   (* Bit-wise operations *)
@@ -2996,7 +2996,7 @@ module BV = struct
   (* Arithmetic operations *)
   let bvneg s =
     let m = size s in
-    int2bv m Ints.(~$Z.(pow ~$2 m) - bv2nat s)
+    int2bv m Ints.(~$Z.(~$1 lsl m) - bv2nat s)
   let bvadd s t = int2bv (size s) Ints.(bv2nat s + bv2nat t)
   let bvsub s t = bvadd s (bvneg t)
   let bvmul s t = int2bv (size s) Ints.(bv2nat s * bv2nat t)