mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

fix #5235

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-01 10:53:39 -07:00
parent 77dea18f54
commit aa3975ed87
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/cmd_context/cmd_context.cpp
View file

@ -877,10 +877,11 @@ void cmd_context::insert(symbol const & s, func_decl * f) {
}
void cmd_context::insert(symbol const & s, psort_decl * p) {
pm().inc_ref(p);
if (m_psort_decls.contains(s)) {
pm().dec_ref(p);
throw cmd_exception("sort already defined ", s);
}
pm().inc_ref(p);
m_psort_decls.insert(s, p);
if (!m_global_decls) {
m_psort_decls_stack.push_back(s);