Release-built hoice sometimes crashes while learning on macOS Monterey

[hopv]

Release-built hoice sometimes crashes while learning on macOS Monterey

[AdrienChampion]

Now you really shouldn't say that, I'm going to pretend I did not see anything otherwise it will take centuries 🐱

[AdrienChampion]

Wow. Thank you for this detailed issue!

This looks like a bug far underneath hoice itself. I'll try my best to find time to investigate, feel free to ping me if I don't get back to you "soon".

[AdrienChampion]

The last frame of the stack trace is hoice::data::Data::destroy, which does nothing but extract statistics for profiling. So it's pretty weird, but the good news is that I don't think it will take a long time to identify whether the problem is in hoice itself or in something below (a Rust library hoice uses, Rust's stdlib itself, rustc or macos).

[AdrienChampion]

@khei4 I could not reproduce the bug 😢

I pushed a new version of hoice though, totally unrelated to this issue. I tested your clauses with it running z3 4.8.17 and nothing went wrong on Monterey 12.3.1.

Let me know if updating hoice + z3 fixes the problem, just in case. In the mean time I'm going to close this issue as I cannot reproduce it. Do feel free to re-open it if new clues come up.

[khei4]

@AdrienChampion Thank you! I can reproduce this error with HoIce(commit hash: 90d348933) for the same input on my MacBookPro (2018 model with Intel Core i5) with the same version z3 as you write. I guess this bug is related to the concurrency and happens non deterministically(sometimes nothing happens on this). Could you reproduce this by executing repeatedly? If nothing happens, maybe some of my dependencies are the cause of this...

[AdrienChampion]

I did a while true running hoice on your clauses on each iteration for a while and failed to crash it. I ran on M1 though, not on Intel. I do have a macbook pro running Monterey on Intel, though I believe it's an i7.

Hmm, I wrote hoice quite a while ago and I thought I did not use unsafe, but I just took a look and I actually do use unsafe to implement Send and Sync (concurrency-related traits) on some types. The fact that I have to do this means Rust cannot show automatically that these types are thread-safe, so maybe there's a problem there.
Outside of a bug in the compiler/LLVM/your machine, it's relatively safe (!) to assume the problem comes from an unsafe block somewhere.

I still find it weird that I cannot reproduce this behavior.

I will investigate further but I need some time, probably a few days. Please ping me in this thread if this issue is time-sensitive for you 🐱
In the mean time, thank you again for opening the issue and keeping in touch to help solve it!

(Re-opening the issue.)

[khei4]

@AdrienChampion Thank you! I'm not in haste. So you don't need to be careful about the time 😃