Prevent data race

[jamesjer]

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 executing parallel_tactic::report_sat. One thread holds m_mutex and is incrementing the reference count of an AST. The other thread does not hold m_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 hold m_mutex so that the reference count manipulations are properly synchronized. With this change, the segfault is no longer reproducible.

[NikolajBjorner]

Thanks a lot for pro-actively checking this out. The bug should have been filed against z3.
I need to look closer into this: the fix is at best a patch and doesn't seem to address the root cause. At first look it seems the parallel solver uses a main solver state that runs in parallel with other solvers. Other solvers copy into that main state under a lock, but the main solver performs other operations that are not protected.
This is a first look and typically such hypotheses are wrong, so I need to check this.

[NikolajBjorner]

I pushed a fix: the root cause was along the lines I outlined above.
It was abusing shared state that was used by a designated thread. The shared state should have been treated symmetrically and under serialization.

[jamesjer]

Thank you for the quick fix, Nikolaj. Much appreciated.