diff --git a/src/ast/expr2polynomial.cpp b/src/ast/expr2polynomial.cpp
index 4831d435b..541f8a770 100644
--- a/src/ast/expr2polynomial.cpp
+++ b/src/ast/expr2polynomial.cpp
@@ -181,13 +181,16 @@ struct expr2polynomial::imp {
         case OP_POWER: {
             rational k;
             SASSERT(t->get_num_args() == 2);
-            if (!m_autil.is_numeral(t->get_arg(1), k) || !k.is_int() || !k.is_unsigned()) {
+            if (!m_autil.is_numeral(t->get_arg(1), k) || !k.is_unsigned()) {
                 if (m_use_var_idxs)
                     throw_not_polynomial();
                 else
                     store_var_poly(t);
                 return true;
             }
+            if (k.is_zero()) {
+                throw_not_polynomial();
+            }
             push_frame(t);
             return false;
         }
diff --git a/src/tactic/arith/probe_arith.cpp b/src/tactic/arith/probe_arith.cpp
index 4f307c9f8..14affd518 100644
--- a/src/tactic/arith/probe_arith.cpp
+++ b/src/tactic/arith/probe_arith.cpp
@@ -153,7 +153,7 @@ struct has_nlmul {
             case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD:
                 if (!a.is_numeral(n->get_arg(1)))
                     throw_found(n);
-				break;
+                break;
             case OP_POWER:
                 throw_found(n);
             default:
@@ -500,6 +500,8 @@ struct is_non_nira_functor {
             case OP_POWER:
                 if (m_linear)
                     throw_found(n);
+                if (!u.is_numeral(n->get_arg(0), r) || !r.is_unsigned() || r.is_zero())
+                    throw_found(n);
                 return;
             case OP_IRRATIONAL_ALGEBRAIC_NUM:
                 if (m_linear || !m_real)