From 247e94a7c04dc651c4cba5d8a0b214f37435492b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Jul 2016 10:34:12 -0700 Subject: [PATCH] fix model generation for cos/sin transformation. Issue #680 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/purify_arith_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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()))); } }