From 3210dce63c83d3f5da092151363839a081df2725 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 18 Feb 2020 12:38:10 -0800
Subject: [PATCH] fix #3038
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/expr2polynomial.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/ast/expr2polynomial.cpp b/src/ast/expr2polynomial.cpp
index 4669f39d4..ea37730cf 100644
--- a/src/ast/expr2polynomial.cpp
+++ b/src/ast/expr2polynomial.cpp
@@ -181,7 +181,7 @@ 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_unsigned()) {
+ if (!m_autil.is_numeral(t->get_arg(1), k) || !k.is_unsigned() || k.is_zero()) {
if (m_use_var_idxs)
throw_not_polynomial();
else