diff --git a/src/math/lp/nla_powers.cpp b/src/math/lp/nla_powers.cpp
index 847ef7a84..4054dd7c1 100644
--- a/src/math/lp/nla_powers.cpp
+++ b/src/math/lp/nla_powers.cpp
@@ -17,7 +17,7 @@ Description:
 
 Special cases:
 
-1. Exponentiation. x is fixed numeral.
+1. Exponentiation. x is fixed numeral a.
 
 TOCL18 axioms:
    a^y > 0                     (if a > 0)
@@ -29,13 +29,13 @@ TOCL18 axioms:
 
 Other special case:
 
-   y = 1 <= a^y = a
+   y = 1 <=> a^y = a
 
 TOCL18 approach: Polynomial abstractions
 
 Taylor: a^y = sum_i ln(a)*y^i/i!
 
-Truncation: P(n, a) = sum_{i=0}^n ln(a)*y^i/i!
+Truncation: P(n, a) = sum_{i=0}^n ln(a)*y^i/i! = 1 + ln(a)*y + ln(a)^2*y^2/2 + 
 
 y = 0: handled by axiom a^y = 1
 y < 0: P(2n-1, y) <= a^y <= P(2n, y), n > 0 because Taylor contribution is negative at odd powers.
@@ -131,9 +131,9 @@ namespace nla {
             return l_false;
         }
 
-        if (xval >= 2 && yval != 0 & rval <= yval + 1) {
-            new_lemma lemma(c, "x >= 2, y != 0 => x^y > y + 1");
-            lemma |= ineq(x, llc::LT, rational(2));
+        if (xval >= 3 && yval != 0 & rval <= yval + 1) {
+            new_lemma lemma(c, "x >= 3, y != 0 => x^y > ln(x)y + 1");
+            lemma |= ineq(x, llc::LT, rational(3));
             lemma |= ineq(y, llc::EQ, rational::zero());
             lemma |= ineq(lp::lar_term(r, rational::minus_one(), y), llc::GT, rational::one());
             return l_false;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index c5b897d78..29f34655a 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1115,7 +1115,8 @@ public:
 
     void mk_power_axiom(expr* p, expr* x, expr* y) {
         rational r;
-        if (a.is_extended_numeral(x, r) && r.is_unsigned() && r.is_pos()) {
+        // r > 0 => r^y > 0
+        if (a.is_extended_numeral(x, r) && r > 0) {
             expr_ref zero(a.mk_real(0), m);
             mk_axiom(~mk_literal(a.mk_le(p, zero)));
         }