From aa3975ed870b855a48e5a5e7b1688abfe6957ae4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 1 May 2021 10:53:39 -0700
Subject: [PATCH] fix #5235
---
src/cmd_context/cmd_context.cpp | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index ac0287312..b5c99f5ce 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -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);