diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 9e06a42d1..346153adb 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 >::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_asin(it->m_value.first), - m().mk_ite(u().mk_ge(it->m_value.second, mk_real_zero()), mk_real_zero(), u().mk_pi()))); + 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()))); } }