From 1619311ff7ae7213ec0389b1ad94b60a58b38d15 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 27 Nov 2020 10:42:02 -0800
Subject: [PATCH] fix #4826

---
 src/ast/rewriter/arith_rewriter.cpp  | 16 +++++++++++++---
 src/ast/rewriter/arith_rewriter.h    |  3 ++-
 src/ast/rewriter/bv_rewriter.h       |  3 ++-
 src/ast/rewriter/poly_rewriter_def.h |  5 +++--
 4 files changed, 20 insertions(+), 7 deletions(-)

diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 0cb2a8e19..eb55c8877 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -480,10 +480,12 @@ expr * arith_rewriter::reduce_power(expr * arg, bool is_eq) {
         if (m_util.is_power(arg, arg0, arg1) && m_util.is_numeral(arg1, k) && k.is_int() &&
             ((is_eq && k > rational(1)) || (!is_eq && k > rational(2)))) {
             if (is_eq || !k.is_even()) {
+                if (m_util.is_int(arg0))
+                    arg0 = m_util.mk_to_real(arg0);
                 new_args.push_back(arg0);
             }
             else {
-                new_args.push_back(mk_power(arg0, rational(2)));
+                new_args.push_back(m_util.mk_power(arg0, m_util.mk_real(2)));
             }
         }
         else {
@@ -1245,11 +1247,19 @@ br_status arith_rewriter::mk_rem_core(expr * arg1, expr * arg2, expr_ref & resul
     return BR_FAILED;
 }
 
-app* arith_rewriter_core::mk_power(expr* x, rational const& r) { 
+expr* arith_rewriter_core::coerce(expr* x, sort* s) {
+    if (m_util.is_int(x) && m_util.is_real(s))
+        return m_util.mk_to_real(x);
+    if (m_util.is_real(x) && m_util.is_int(s))
+        return m_util.mk_to_int(x);
+    return x;
+}
+
+app* arith_rewriter_core::mk_power(expr* x, rational const& r, sort* s) { 
     SASSERT(r.is_unsigned() && r.is_pos());
     bool is_int = m_util.is_int(x);
     app* y = m_util.mk_power(x, m_util.mk_numeral(r, is_int));
-    if (is_int) 
+    if (m_util.is_int(s))
         y = m_util.mk_to_int(y);
     return y;
 }
diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h
index 38be5486f..d64896d3d 100644
--- a/src/ast/rewriter/arith_rewriter.h
+++ b/src/ast/rewriter/arith_rewriter.h
@@ -44,7 +44,8 @@ protected:
     decl_kind mul_decl_kind() const { return OP_MUL; }
     bool use_power() const { return m_mul2power && !m_expand_power; }
     decl_kind power_decl_kind() const { return OP_POWER; }
-    app* mk_power(expr* x, rational const& r);
+    app* mk_power(expr* x, rational const& r, sort* s);
+    expr* coerce(expr* x, sort* s);
 public:
     arith_rewriter_core(ast_manager & m):m_util(m) {}
     bool is_zero(expr * n) const { return m_util.is_zero(n); }
diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
index 6a2b3aefa..e9596256f 100644
--- a/src/ast/rewriter/bv_rewriter.h
+++ b/src/ast/rewriter/bv_rewriter.h
@@ -39,7 +39,8 @@ protected:
     decl_kind add_decl_kind() const { return OP_BADD; }
     decl_kind mul_decl_kind() const { return OP_BMUL; }
     bool use_power() const { return false; }
-    app* mk_power(expr* x, rational const& r) { UNREACHABLE(); return nullptr; }
+    app* mk_power(expr* x, rational const& r, sort* s) { UNREACHABLE(); return nullptr; }
+    expr* coerce(expr* x, sort* s) { UNREACHABLE(); return nullptr; }
     decl_kind power_decl_kind() const { UNREACHABLE(); return static_cast<decl_kind>(UINT_MAX); }
 
 public:
diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h
index 4a236283b..fd95bb85a 100644
--- a/src/ast/rewriter/poly_rewriter_def.h
+++ b/src/ast/rewriter/poly_rewriter_def.h
@@ -85,15 +85,16 @@ expr * poly_rewriter<Config>::mk_mul_app(unsigned num_args, expr * const * args)
         return args[0];
     default: 
         if (use_power()) {
+            sort* s = m().get_sort(args[0]);
             rational k_prev;
             expr * prev = get_power_body(args[0], k_prev);
             rational k;
             ptr_buffer<expr> new_args;
             auto push_power = [&]() { 
                 if (k_prev.is_one())                                                           
-                    new_args.push_back(prev);                                                   
+                    new_args.push_back(this->coerce(prev, s));
                 else  
-                    new_args.push_back(this->mk_power(prev, k_prev));                                                                                            
+                    new_args.push_back(this->mk_power(prev, k_prev, s));
             };
  
             for (unsigned i = 1; i < num_args; i++) {