Mate Soos

Hi, Can you please run: ``` ldd cryptominisat5 ``` and paste the output here? Also, please do what's above again, but this time, run with: ``` cd .. rm -rf...

Ah, now I see! Thanks @capiman for helping out! Sorry, I had the `NOMPI` flag only in my development version. I now backported it to the `master` branch. This is...

Hey, Thanks for the issue and thanks for the compliment :) This is a very interesting topic and I would stronlgy recommend you to check out this paper, I think...

Hi, Potentially, there is a bug in CryptoMiniSat, or there is a bug in the way you are using it. You'll need to use `gdb` and try to get to...

Sorry, I'll pick this up in the coming days, this is 100÷ an issue. I'll get back to you on Saturday, hopefully with a fix :) Mate On Wed, Oct...

Wow, this is a weird instance :) Can you please do me a favour and check if setting `-intree 0 --sls 0` helps? I am running [massif](https://www.valgrind.org/docs/manual/ms-manual.html) right now, but...

Hi! So `valgrind` crashed on me overnight and decided not to dump the data while crashing :D My understanding is that it's the `--sls 0` that will fix things. Can...

Ah nice! so `--intree 0 and --sls 0` is not eating memory and effectively is fixing the problem. That's great feedback! I'll try to check what that could mean. In...

Nice! So what is probably happening is that in-tree probing (i.e. `intree`) is generating a ton of binary clauses in your case and they are slowing things down. I wonder...

All right, I see, let's do that. Note that MiniSat and CryptoMiniSat are about 45'000 lines of code from each other, so "the same" may a bit of a stretch...