diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 399aa76f2..d229865ad 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -273,6 +273,17 @@ public:
     bool is_rem0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_REM0); }
     bool is_mod0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_MOD0); }
     bool is_power0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_POWER0); }
+    bool is_power(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_POWER); }
+    bool is_add(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_ADD); }
+    bool is_mul(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_MUL); }
+    bool is_sub(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_SUB); }
+    bool is_uminus(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_UMINUS); }
+    bool is_div(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_DIV); }
+    bool is_rem(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_REM); }
+    bool is_mod(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_MOD); }
+    bool is_to_real(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_TO_REAL); }
+    bool is_to_int(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_TO_INT); }
+    bool is_is_int(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_IS_INT); }
 
     bool is_add(expr const * n) const { return is_app_of(n, arith_family_id, OP_ADD); }
     bool is_sub(expr const * n) const { return is_app_of(n, arith_family_id, OP_SUB); }
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 19be6d9d5..1fa0606c2 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -1447,21 +1447,19 @@ namespace arith {
             TRACE("arith", tout << "canceled\n";);
             return l_undef;
         }
-        if (!m_nla) {
-            TRACE("arith", tout << "no nla\n";);
+        CTRACE("arith", !m_nla, tout << "no nla\n";);
+        if (!m_nla) 
             return l_true;
-        }
         if (!m_nla->need_check())
             return l_true;
 
         m_a1 = nullptr; m_a2 = nullptr;
         lbool r = m_nla->check(m_nla_lemma_vector);
         switch (r) {
-        case l_false: {
+        case l_false: 
             for (const nla::lemma& l : m_nla_lemma_vector)
                 false_case_of_check_nla(l);
             break;
-        }
         case l_true:
             if (assume_eqs())
                 return l_false;
@@ -1478,11 +1476,26 @@ namespace arith {
     }
 
     bool solver::include_func_interp(func_decl* f) const {
-        return 
-            a.is_div0(f) ||
-            a.is_idiv0(f) ||
-            a.is_power0(f) ||
-            a.is_rem0(f) ||
-            a.is_mod0(f);        
+        SASSERT(f->get_family_id() == get_id());
+        switch (f->get_decl_kind()) {
+        case OP_ADD:
+        case OP_SUB:
+        case OP_UMINUS:
+        case OP_MUL:
+        case OP_LE:
+        case OP_LT:
+        case OP_GE:
+        case OP_GT:
+        case OP_MOD:
+        case OP_REM:
+        case OP_DIV:
+        case OP_POWER:
+        case OP_IS_INT:
+        case OP_TO_INT:
+        case OP_TO_REAL:
+            return false;
+        default:
+            return true;            
+        }
     }
 }