From 0609408fd7dda5df3ad18dd6ab02de355b2580fe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Mar 2020 01:50:30 -0700 Subject: [PATCH] fix #3510 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/purify_arith_tactic.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 88c530857..783202566 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -175,6 +175,7 @@ struct purify_arith_proc { m_sin_cos.insert(to_app(theta), pair); m_pinned.push_back(pair.first); m_pinned.push_back(pair.second); + m_pinned.push_back(theta); // TBD for model conversion } x = pair.first;