From dd07d21f6c311da2e7657ed52403407766854ab4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Dec 2019 12:16:28 -0800 Subject: [PATCH] fix #2821 Signed-off-by: Nikolaj Bjorner --- src/ast/expr2polynomial.cpp | 5 ++++- src/tactic/arith/probe_arith.cpp | 4 +++- 2 files changed, 7 insertions(+), 2 deletions(-) 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)