fix #8024

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/arith_decl_plugin.cpp

@@ -188,8 +188,12 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
 
     m_to_real_decl = m->mk_func_decl(symbol("to_real"), i, r, func_decl_info(id, OP_TO_REAL));
     m->inc_ref(m_to_real_decl);
+    m_r_to_real_decl = m->mk_func_decl(symbol("to_real"), r, r, func_decl_info(id, OP_TO_REAL));
+    m->inc_ref(m_r_to_real_decl);
     m_to_int_decl = m->mk_func_decl(symbol("to_int"), r, i, func_decl_info(id, OP_TO_INT));
     m->inc_ref(m_to_int_decl);
+    m_i_to_int_decl = m->mk_func_decl(symbol("to_int"), i, i, func_decl_info(id, OP_TO_INT));
+    m->inc_ref(m_i_to_int_decl);
     m_is_int_decl = m->mk_func_decl(symbol("is_int"), r, m->mk_bool_sort(), func_decl_info(id, OP_IS_INT));
     m->inc_ref(m_is_int_decl);
 
@@ -311,6 +315,8 @@ void arith_decl_plugin::finalize() {
     DEC_REF(m_i_rem_decl);
     DEC_REF(m_to_real_decl);
     DEC_REF(m_to_int_decl);
+    DEC_REF(m_r_to_real_decl);
+    DEC_REF(m_i_to_int_decl);
     DEC_REF(m_is_int_decl);
     DEC_REF(m_i_power_decl);
     DEC_REF(m_r_power_decl);
@@ -368,8 +374,8 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool 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_real_decl, func_decl_info(m_family_id, OP_POWER0));
-    case OP_TO_REAL: return m_to_real_decl;
+    case OP_TO_REAL: return is_real ? m_r_to_real_decl : m_to_real_decl;
-    case OP_TO_INT:  return m_to_int_decl;
+    case OP_TO_INT:  return is_real ? m_to_int_decl : m_i_to_int_decl;
     case OP_IS_INT:  return m_is_int_decl;
     case OP_POWER:   return is_real ? m_r_power_decl : m_i_power_decl;
     case OP_ABS:     return is_real ? m_r_abs_decl : m_i_abs_decl;

src/ast/arith_decl_plugin.h

@@ -120,11 +120,13 @@ protected:
     func_decl * m_i_mod_decl;
     func_decl * m_i_rem_decl;
 
-    func_decl * m_to_real_decl;
+    func_decl * m_to_real_decl = nullptr;
-    func_decl * m_to_int_decl;
+    func_decl * m_to_int_decl = nullptr;
-    func_decl * m_is_int_decl;
+    func_decl * m_r_to_real_decl = nullptr;
-    func_decl * m_r_power_decl;
+    func_decl * m_i_to_int_decl = nullptr;
-    func_decl * m_i_power_decl;
+    func_decl * m_is_int_decl = nullptr;
+    func_decl * m_r_power_decl = nullptr;
+    func_decl * m_i_power_decl = nullptr;
 
     func_decl * m_r_abs_decl;
     func_decl * m_i_abs_decl;

src/ast/rewriter/arith_rewriter.cpp

@@ -1829,6 +1829,10 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
 br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
     numeral a;
     expr* x = nullptr;
+    if (m_util.is_int(arg)) {
+        result = arg;
+        return BR_DONE;
+    }
     if (m_util.convert_int_numerals_to_real())
         return BR_FAILED;
 
@@ -1837,7 +1841,7 @@ br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
         return BR_DONE;
     }
 
-    if (m_util.is_to_real(arg, x)) {
+    if (m_util.is_to_real(arg, x) && m_util.is_int(x)) {
         result = x;
         return BR_DONE;
     }
@@ -1885,6 +1889,10 @@ br_status arith_rewriter::mk_to_real_core(expr * arg, expr_ref & result) {
         result = m_util.mk_numeral(a, false);
         return BR_DONE;
     }
+    if (m_util.is_real(arg)) {
+        result = arg;
+        return BR_DONE;
+    }
     // push to_real over OP_ADD, OP_MUL
     if (m_push_to_real) {
         if (m_util.is_add(arg) || m_util.is_mul(arg)) {
@@ -1909,7 +1917,7 @@ br_status arith_rewriter::mk_is_int(expr * arg, expr_ref & result) {
         return BR_DONE;
     }
     
-    if (m_util.is_to_real(arg)) {
+    if (m_util.is_to_real(arg) && m_util.is_int(to_app(arg)->get_arg(0))) {
         result = m.mk_true();
         return BR_DONE;
     }