ASSERTION VIOLATION when an external function and the GC run concurrently

[gyggg]

I encountered a possible bug in the GC when called concurrently with an external function of the SMT solver Z3 (version 4.8.11).

Here is a simple program that reproduces the error: https://github.com/gyggg/Multicore_OCaml_Test/tree/for_latest_multicore
There, the master branch is for OCaml 4.12.0+domains and the for_latest_multicore branch is for

> ocamlrun -version
> The OCaml runtime, version 4.14.0+domains+dev0
> Built with git hash '379f052ef' on branch '5.00' with tag '<tag unavailable>'

Description

In the program (main.ml), an external function get_unsat_core of Z3 is called repeatedly (line 21) in a subdomain and GC.major is called repeatedly in the main domain (line 25).

An assertion in Z3 is violated probabilistically when GC.major and get_unsat_core are called simultaneously, showing the following error message:

ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 432
UNEXPECTED CODE WAS REACHED.
Z3 4.8.11.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new

By inspecting the code around the line, I found that the assertion is violated when Z3 tries to free some objects in the function get_unsat_core that have already been freed (by the GC).
In fact, if we modify the program to call GC.full_major just before the call to get_unsat_core to avoid such a conflict, we no longer get the error.

[gyggg]

I tried to install the latest version of multicore-ocaml, i.e. 23a04fb98. But the problem still exists. If there is any workaround for this problem, I would be grateful if you could let me know!