Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
I maintain the z3 package for the Fedora Linux distribution. Recently a user reported a segfault. A build with
-fsanitize=thread
revealed a data race. Two threads are executingparallel_tactic::report_sat
. One thread holdsm_mutex
and is incrementing the reference count of an AST. The other thread does not holdm_mutex
and is decrementing the reference count of the same AST. In some cases, this leads to a segfault down the road when a bad array access is attempted. See the linked bug report for details. This commit forces the thread that decrements the reference count to holdm_mutex
so that the reference count manipulations are properly synchronized. With this change, the segfault is no longer reproducible.