diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 71e54c0a3..9ccf02d0d 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -290,6 +290,8 @@ 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_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); }
 
     MATCH_UNARY(is_uminus);
     MATCH_UNARY(is_to_real);
@@ -307,8 +309,13 @@ public:
     MATCH_BINARY(is_idiv);
     MATCH_BINARY(is_power);
 
-    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); }
+    MATCH_UNARY(is_sin);
+    MATCH_UNARY(is_asin);
+    MATCH_UNARY(is_cos);
+    MATCH_UNARY(is_acos);
+    MATCH_UNARY(is_tan);
+    MATCH_UNARY(is_atan);
+
 };
 
 class arith_util : public arith_recognizers {
@@ -355,6 +362,9 @@ public:
     app * mk_int(int i) {
         return mk_numeral(rational(i), true);
     }
+    app * mk_real(int i) {
+        return mk_numeral(rational(i), false);
+    }
     app * mk_le(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LE, arg1, arg2); }
     app * mk_ge(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_GE, arg1, arg2); }
     app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LT, arg1, arg2); }
diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index c9a2d2379..8f8c9a2bc 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -1196,11 +1196,17 @@ expr * arith_rewriter::mk_sin_value(rational const & k) {
 }
 
 br_status arith_rewriter::mk_sin_core(expr * arg, expr_ref & result) {
-    if (is_app_of(arg, get_fid(), OP_ASIN)) {
+    expr * m, *x;
+    if (m_util.is_asin(arg, x)) {
         // sin(asin(x)) == x
-        result = to_app(arg)->get_arg(0);
+        result = x;
         return BR_DONE;
     }
+    if (m_util.is_acos(arg, x)) {
+        // sin(acos(x)) == sqrt(1 - x^2)
+        result = m_util.mk_power(m_util.mk_sub(m_util.mk_real(1), m_util.mk_mul(x,x)), m_util.mk_numeral(rational(1,2), false));
+        return BR_REWRITE_FULL;
+    }
     rational k;
     if (is_numeral(arg, k) && k.is_zero()) {
         // sin(0) == 0
@@ -1214,7 +1220,6 @@ br_status arith_rewriter::mk_sin_core(expr * arg, expr_ref & result) {
             return BR_REWRITE_FULL;
     }
 
-    expr * m;
     if (is_pi_offset(arg, k, m)) {
         rational k_prime = mod(floor(k), rational(2)) + k - floor(k);
         SASSERT(k_prime >= rational(0) && k_prime < rational(2));
@@ -1250,11 +1255,15 @@ br_status arith_rewriter::mk_sin_core(expr * arg, expr_ref & result) {
 }
 
 br_status arith_rewriter::mk_cos_core(expr * arg, expr_ref & result) {
-    if (is_app_of(arg, get_fid(), OP_ACOS)) {
+    expr* x;
+    if (m_util.is_acos(arg, x)) {
         // cos(acos(x)) == x
-        result = to_app(arg)->get_arg(0);
+        result = x;
         return BR_DONE;
     }
+    if (m_util.is_asin(arg, x)) {
+        // cos(asin(x)) == ...
+    }
 
     rational k;
     if (is_numeral(arg, k) && k.is_zero()) {
diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp
index 346153adb..d0891b28b 100644
--- a/src/tactic/arith/purify_arith_tactic.cpp
+++ b/src/tactic/arith/purify_arith_tactic.cpp
@@ -782,8 +782,8 @@ struct purify_arith_proc {
             obj_map<app, std::pair<expr*,expr*> >::iterator it = m_sin_cos.begin(), end = m_sin_cos.end();
             for (; it != end; ++it) {
                 emc->insert(it->m_key->get_decl(), 
-                            u().mk_add(u().mk_acos(it->m_value.second), 
-                                       m().mk_ite(u().mk_ge(it->m_value.first, mk_real_zero()), mk_real_zero(), u().mk_pi())));
+                            m().mk_ite(u().mk_ge(it->m_value.first, mk_real_zero()), u().mk_acos(it->m_value.second), 
+                                       u().mk_add(u().mk_acos(u().mk_uminus(it->m_value.second)), u().mk_pi())));
             }
 
         }