mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

fix #3510

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-25 01:50:30 -07:00
parent b8c25ac20b
commit 0609408fd7
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/tactic/arith/purify_arith_tactic.cpp
View file

@ -175,6 +175,7 @@ struct purify_arith_proc {
m_sin_cos.insert(to_app(theta), pair); m_sin_cos.insert(to_app(theta), pair);
m_pinned.push_back(pair.first); m_pinned.push_back(pair.first);
m_pinned.push_back(pair.second); m_pinned.push_back(pair.second);
m_pinned.push_back(theta);
// TBD for model conversion // TBD for model conversion
} }
x = pair.first; x = pair.first;