diff --git a/CHANGES.md b/CHANGES.md
index eaa355eef5..8ff9fe7cf5 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,8 +1,10 @@
 ## unreleased
 
+ - Support the `int.pow2` function, which takes an integer `n` and computes
+   `ae.pow_int 2 n` (#1365)
  - Support parsing of SMT-LIB FPA Theory literals and add the theory `smt.float`
-   that enables thte support for the SMT-LIB FPA, and that can be used with the
-   cmdline option `--enable-theory smt.float` (#1358)
+   that enables the support for the SMT-LIB FPA Theory, and that can be used
+   with the cmdline option `--enable-theory smt.float` (#1358)
  - Bump minimal cmdliner version to 2.0 (#1340)
 
 ## v2.6.2
diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml
index 20c1b3f73d..b9a064e8e9 100644
--- a/src/lib/frontend/translate.ml
+++ b/src/lib/frontend/translate.ml
@@ -149,6 +149,7 @@ type _ DStd.Builtin.t +=
       Not_theory_constant
   | Is_theory_constant
   | Linear_dependency
+  | Int_pow2
 
 let builtin_term t = Dl.Typer.T.builtin_term t
 
@@ -268,7 +269,7 @@ let ae_fpa_builtins =
     let a = Var.mk "alpha" in
     op ~tyvars:[a] "is_theory_constant" Is_theory_constant ([of_var a] ->. prop)
   in
-  let fpa_builtins =
+  let additional_builtins =
     let open DT in
     DStd.Id.Map.empty |> add_rounding_modes
     (* the first argument is mantissas' size (including the implicit bit), the
@@ -316,13 +317,15 @@ let ae_fpa_builtins =
     |> op "integer_log2" Integer_log2 ([real] ->. int)
     (* only used for arithmetic. It should not be used for x in float(x) to
        enable computations modulo equality *)
+    |> op "int.pow2" Int_pow2 ([int] ->. int)
+    (* computes 2 to the power of a given integer. *)
     |> op "not_theory_constant" Not_theory_constant ([real] ->. prop)
     |> is_theory_constant
     |> op "linear_dependency" Linear_dependency ([real; real] ->. prop)
   in
   fun env s ->
     let search_id id =
-      try DStd.Id.Map.find_exn id fpa_builtins env s
+      try DStd.Id.Map.find_exn id additional_builtins env s
       with Not_found -> `Not_found
     in
     match s with
@@ -336,6 +339,10 @@ let smt_fpa_builtins =
     Dl.Typer.T.builtin_term
     @@ Dolmen_type.Base.term_app2 (module Dl.Typer.T) env s f
   in
+  let int_pow2_cst =
+    let ty = DT.arrow [DT.int] DT.int in
+    DE.Id.mk ~name:"int.pow2" ~builtin:Int_pow2 (DStd.Path.global "int.pow2") ty
+  in
   let other_builtins = DStd.Id.Map.empty |> add_rounding_modes in
   fun env s ->
     match s with
@@ -359,6 +366,9 @@ let smt_fpa_builtins =
       term_app env s DE.Term.Int.pow
     | Id { ns = Term; name = Simple "ae.pow_real" } ->
       term_app env s DE.Term.Real.pow
+    | Id { ns = Term; name = Simple "int.pow2" } ->
+      Dl.Typer.T.builtin_term
+      @@ Dolmen_type.Base.term_app_cst (module Dl.Typer.T) env int_pow2_cst
     | Dl.Typer.T.Id id -> begin
       match DStd.Id.Map.find_exn id other_builtins env s with
       | e -> e
@@ -1211,6 +1221,10 @@ let rec mk_expr ?(loc = Loc.dummy) ?(name_base = "") ?(toplevel = false)
         | Max_int, _ -> op Max_int
         | Min_int, _ -> op Min_int
         | Integer_log2, _ -> op Integer_log2
+        | Int_pow2, [n] ->
+          E.mk_term (Sy.Op Sy.Pow)
+            [E.Ints.of_int 2; aux_mk_expr n]
+            (dty_to_ty term_ty)
         | Not_theory_constant, _ -> op Not_theory_constant
         | Is_theory_constant, _ -> op Is_theory_constant
         | Linear_dependency, _ -> op Linear_dependency
diff --git a/tests/arith/int_pow2_sym.expected b/tests/arith/int_pow2_sym.expected
new file mode 100644
index 0000000000..6f99ff0f44
--- /dev/null
+++ b/tests/arith/int_pow2_sym.expected
@@ -0,0 +1,2 @@
+
+unsat
diff --git a/tests/arith/int_pow2_sym.smt2 b/tests/arith/int_pow2_sym.smt2
new file mode 100644
index 0000000000..41fa81b365
--- /dev/null
+++ b/tests/arith/int_pow2_sym.smt2
@@ -0,0 +1,4 @@
+(set-logic ALL)
+(declare-const n Int)
+(assert (not (= (int.pow2 n) (ae.pow_int 2 n))))
+(check-sat)