Multi-thread trigger assertion

[Flash-LHR]

The operation succeeds when using the default number of threads, but the assertion fails after setting the number of threads. OS： 5.17.0-kali3-amd64 CPU：Intel(R) Core(TM) i5-8300H CPU @ 2.30GHz

r05.cnf.txt

[msoos]

Hi,

Thanks! Is this related to this? https://github.com/meelgroup/bosphorus/issues In other words, does that PR fix this bug or it causes this bug? I understand that this needs fixing, but want to understand first how to reproduce.

Cheers,

Mate

[Flash-LHR]

This issue has nothing to do with pr.

Pr only sets the number of threads of cryptominisat5. Before pr, the number of threads of cryptominisat5 is always 1 regardless of whether the user specifies the thread parameter. In fact, I did not attempt to fix the above assertion failure.

I have uploaded the file r05.cnf for reproducing.

[msoos]

Hi,

Sorry for the late response. It was indeed a bug! I fixed it in CryptoMiniSat, here: https://github.com/msoos/cryptominisat/commit/9b4ee6f14849f7ea2b9efe2f33b698a3ba203947

If you recompile both CMS and Bosphorus (maybe no need to recompile Bosphorus, depending on your setup), it should now work! I have tested it :)

I would like to thank you for both the perfectly reproducible problem description and your patience. Sorry, lately I've been very busy so I couldn't get to this as soon as I hoped. Nevertheless, about 1 week to fix is probably not too bad. Thanks again for the bug report, it really helped,

Mate

[Flash-LHR]

Thank you very much, it helps me a lot.

Besides, I have made a pr to set threadNum for cryptominisat in bosphorus, maybe you can consider that.

[msoos]

Ah, good point, thanks for the reminder! I merged the PR as well, and cleaned up the code a bit along the way.