From 04a19cd1d8d964f4c7e88732be4844f84af0c11b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 10 Mar 2020 16:21:01 -0700
Subject: [PATCH] fix #3219

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/arith_rewriter.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 08ad077df..da71891a4 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -1161,6 +1161,10 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
     if (!is_num_x && !is_irrat_x)
         return BR_FAILED;
 
+    if (y.is_zero()) {
+        return BR_FAILED;
+    }
+
     rational num_y = numerator(y);
     rational den_y = denominator(y);
     bool is_neg_y  = false;