diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 4778caf89..a1d067a32 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -370,7 +370,7 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) { if (is_real) { return m_manager->mk_func_decl(symbol("^0"), m_real_decl, m_real_decl, m_real_decl, func_decl_info(m_family_id, OP_POWER0)); } - return m_manager->mk_func_decl(symbol("^0"), m_int_decl, m_int_decl, m_int_decl, func_decl_info(m_family_id, OP_POWER0)); + return m_manager->mk_func_decl(symbol("^0"), m_int_decl, m_int_decl, m_real_decl, func_decl_info(m_family_id, OP_POWER0)); case OP_TO_REAL: return m_to_real_decl; case OP_TO_INT: return m_to_int_decl; case OP_IS_INT: return m_is_int_decl; @@ -834,7 +834,7 @@ bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, expr* con func_decl* arith_util::mk_ipower0() { sort* s = mk_int(); sort* rs[2] = { s, s }; - return m_manager.mk_func_decl(arith_family_id, OP_POWER0, 0, nullptr, 2, rs, s); + return m_manager.mk_func_decl(arith_family_id, OP_POWER0, 0, nullptr, 2, rs, mk_real()); } func_decl* arith_util::mk_rpower0() {