From f1a39b888471ec6282717f26b17497b075ed068b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Nov 2023 11:54:59 -0800 Subject: [PATCH] add comment regarding usage model for flush_objects() to relate with pr #6992 Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 53f53347e..66cd715c9 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -78,6 +78,11 @@ namespace api { m().dec_ref(a); } + // flush_objects can only be called in the main thread. + // This ensures that the calls to m().dec_ref() and dealloc(o) + // only happens in the main thread. + // Calls to dec_ref are allowed in other threads when m_concurrent_dec_ref is + // set to true. void context::flush_objects() { #ifndef SINGLE_THREAD if (!m_concurrent_dec_ref)