diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
index d9bb3aa90..11b03bd21 100644
--- a/src/sat/smt/arith_axioms.cpp
+++ b/src/sat/smt/arith_axioms.cpp
@@ -65,6 +65,31 @@ namespace arith {
         add_clause(eq, eq_internalize(t, a.mk_numeral(rational(1), a.is_int(t))));
     }
 
+    // t = n^p
+    void solver::mk_power_axiom(expr* p, expr* x, expr* y) {
+        if (a.is_zero(y)) {
+            mk_power0_axioms(to_app(p), to_app(x));
+            return;
+        }
+        rational r;
+        // r > 0 => r^y > 0
+        if (a.is_extended_numeral(x, r) && r > 0) {
+            expr_ref zero(a.mk_real(0), m);
+            add_clause(~mk_literal(a.mk_le(p, zero)));
+        }
+        if (a.is_extended_numeral(y, r) && r > 0) {
+            // r is m/n then x >= 0 => x^m = p^n
+            if (denominator(r) > 1) {
+                expr_ref x_ge_0(a.mk_ge(x, a.mk_real(0)), m);
+                expr_ref x(m);
+                if (numerator(r) > 1)
+                    x = a.mk_power(x, a.mk_real(numerator(r)));
+                expr_ref x_eq_pn(a.mk_eq(x, a.mk_power(p, a.mk_real(denominator(r)))), m);
+                add_clause(~mk_literal(x_ge_0), mk_literal(x_eq_pn));
+            }
+        }
+    }
+
     // is_int(x) <=> to_real(to_int(x)) = x
     void solver::mk_is_int_axiom(expr* n) {
         expr* x = nullptr;
diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp
index 9c4e5c9be..5527b9871 100644
--- a/src/sat/smt/arith_internalize.cpp
+++ b/src/sat/smt/arith_internalize.cpp
@@ -262,6 +262,12 @@ namespace arith {
                     st.to_ensure_var().push_back(n1);
                     st.to_ensure_var().push_back(n2);
                 }
+                else if (a.is_power(n, n1, n2)) {
+                    found_unsupported(n);
+                    mk_power_axiom(n, n1, n2);
+                    st.to_ensure_var().push_back(n1);
+                    st.to_ensure_var().push_back(n2);
+                }
                 else if (a.is_band(n) || a.is_shl(n) || a.is_ashr(n) || a.is_lshr(n)) {
                     m_bv_terms.push_back(to_app(n));
                     ctx.push(push_back_vector(m_bv_terms));
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index 3c4a58890..c11967869 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -312,6 +312,7 @@ namespace arith {
         void mk_is_int_axiom(expr* n);
         void mk_idiv_mod_axioms(expr* p, expr* q);
         void mk_rem_axiom(expr* dividend, expr* divisor);
+        void mk_power_axiom(expr* t, expr* n, expr* p);
         void mk_bound_axioms(api_bound& b);
         void mk_bound_axiom(api_bound& b1, api_bound& b2);
         void mk_power0_axioms(app* t, app* n);