mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

add comment regarding usage model for flush_objects() to relate with pr #6992

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-11-15 11:54:59 -08:00
parent 3baaba5edd
commit f1a39b8884
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/api/api_context.cpp
View file

@ -78,6 +78,11 @@ namespace api {
m().dec_ref(a); 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() { void context::flush_objects() {
#ifndef SINGLE_THREAD #ifndef SINGLE_THREAD
if (!m_concurrent_dec_ref) if (!m_concurrent_dec_ref)