diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 9ccf02d0d..4f0379674 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -290,6 +290,9 @@ public:
     bool is_asin(expr const* n) const { return is_app_of(n, m_afid, OP_ASIN); }
     bool is_acos(expr const* n) const { return is_app_of(n, m_afid, OP_ACOS); }
     bool is_atan(expr const* n) const { return is_app_of(n, m_afid, OP_ATAN); }
+    bool is_asinh(expr const* n) const { return is_app_of(n, m_afid, OP_ASINH); }
+    bool is_acosh(expr const* n) const { return is_app_of(n, m_afid, OP_ACOSH); }
+    bool is_atanh(expr const* n) const { return is_app_of(n, m_afid, OP_ATANH); }
     bool is_pi(expr * arg) { return is_app_of(arg, m_afid, OP_PI); }
     bool is_e(expr * arg) { return is_app_of(arg, m_afid, OP_E); }
 
@@ -311,10 +314,13 @@ public:
 
     MATCH_UNARY(is_sin);
     MATCH_UNARY(is_asin);
+    MATCH_UNARY(is_asinh);
     MATCH_UNARY(is_cos);
     MATCH_UNARY(is_acos);
+    MATCH_UNARY(is_acosh);
     MATCH_UNARY(is_tan);
     MATCH_UNARY(is_atan);
+    MATCH_UNARY(is_atanh);
 
 };
 
diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 8f8c9a2bc..368476b8e 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -946,12 +946,13 @@ 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;
     if (m_util.is_numeral(arg, a)) {
         result = m_util.mk_numeral(floor(a), true);
         return BR_DONE;
     }
-    else if (m_util.is_to_real(arg)) {
-        result = to_app(arg)->get_arg(0);
+    else if (m_util.is_to_real(arg, x)) {
+        result = x;
         return BR_DONE;
     }
     else {
@@ -982,8 +983,8 @@ br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
                         new_args.push_back(m_util.mk_numeral(a, true));
                     }
                     else {
-                        SASSERT(m_util.is_to_real(c));
-                        new_args.push_back(to_app(c)->get_arg(0));
+                        VERIFY (m_util.is_to_real(c, x));
+                        new_args.push_back(x);
                     }
                 }
                 SASSERT(num_args == new_args.size());
@@ -1315,9 +1316,10 @@ br_status arith_rewriter::mk_cos_core(expr * arg, expr_ref & result) {
 }
 
 br_status arith_rewriter::mk_tan_core(expr * arg, expr_ref & result) {
-    if (is_app_of(arg, get_fid(), OP_ATAN)) {
+    expr* x;
+    if (m_util.is_atan(arg, x)) {
         // tan(atan(x)) == x
-        result = to_app(arg)->get_arg(0);
+        result = x;
         return BR_DONE;
     }
 
@@ -1497,9 +1499,10 @@ br_status arith_rewriter::mk_atan_core(expr * arg, expr_ref & result) {
 }
 
 br_status arith_rewriter::mk_sinh_core(expr * arg, expr_ref & result) {
-    if (is_app_of(arg, get_fid(), OP_ASINH)) {
+    expr* x;
+    if (m_util.is_asinh(arg, x)) {
         // sinh(asinh(x)) == x
-        result = to_app(arg)->get_arg(0);
+        result = x;
         return BR_DONE;
     }
     expr * t;
@@ -1512,12 +1515,12 @@ br_status arith_rewriter::mk_sinh_core(expr * arg, expr_ref & result) {
 }
 
 br_status arith_rewriter::mk_cosh_core(expr * arg, expr_ref & result) {
-    if (is_app_of(arg, get_fid(), OP_ACOSH)) {
-        // cosh(acosh(x)) == x
-        result = to_app(arg)->get_arg(0);
+    expr* t;
+    if (m_util.is_acosh(arg, t)) {
+        // cosh(acosh(t)) == t
+        result = t;
         return BR_DONE;
     }
-    expr * t;
     if (m_util.is_times_minus_one(arg, t)) {
         // cosh(-t) == cosh
         result = m_util.mk_cosh(t);
@@ -1527,12 +1530,12 @@ br_status arith_rewriter::mk_cosh_core(expr * arg, expr_ref & result) {
 }
 
 br_status arith_rewriter::mk_tanh_core(expr * arg, expr_ref & result) {
-    if (is_app_of(arg, get_fid(), OP_ATANH)) {
-        // tanh(atanh(x)) == x
-        result = to_app(arg)->get_arg(0);
+    expr * t;
+    if (m_util.is_atanh(arg, t)) {
+        // tanh(atanh(t)) == t
+        result = t;
         return BR_DONE;
     }
-    expr * t;
     if (m_util.is_times_minus_one(arg, t)) {
         // tanh(-t) == -tanh(t)
         result = m_util.mk_uminus(m_util.mk_tanh(t));
diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index 083fd6e0c..109eb0deb 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -125,7 +125,6 @@ namespace smt {
         unsigned num_units = assigned_literals().size();
         app_ref eq(m_manager);
         TRACE("context", 
-              tout << "pop:  " << num_levels << "\n";
               tout << "vars: " << vars.size() << "\n";
               tout << "lits: " << num_units << "\n";);
         m_case_split_queue->init_search_eh();