Assertion '__builtin_expect(__n < this->size(), true)' failed

[jwaldmann]

Hi. I have this (unsat by construction) CNF (408 vars 2176 clauses) where cryptominisat5 dumps core with message

/usr/include/c++/10/bits/stl_vector.h:1045: std::vector<_Tp, _Alloc>::reference std::vector<_Tp, _Alloc>::operator[](std::vector<_Tp, _Alloc>::size_type) [with _Tp = int; _Alloc = std::allocator<int>; std::vector<_Tp, _Alloc>::reference = int&; std::vector<_Tp, _Alloc>::size_type = long unsigned int]: Assertion '__builtin_expect(__n < this->size(), true)' failed.
Aborted (core dumped)

This happens for cryptominisat5 (5.8.0) as packaged with Fedora GNU/Linux (33) on x86_64 , and also when I compile master from this repo.

I added input and log to https://github.com/jwaldmann/cryptominisat/tree/master/tests/cnf-files (crash.*)

[msoos]

Hi!

First of all, thanks so much for your work! You are 100% right, and it's a real bug, still in the newest system! Wow. So just for background, it seems that Fedora enforces -D_GLIBCXX_ASSERTIONS which turns on assertions in some C++11 constructs. And it caught a bug that not even clang Address Sanitizer could catch!

Amazing stuff. I will also alert the authors of CCANR where the bug resides. Thanks again for this, great catch! It should now be fixed. Please take master and check :) Thanks again,

Mate

[capiman]

Is it correct that the fix checks if index is not too high and if it is too high just does nothing?
Are you sure, that this fixes the real bug behind (why the index is too high) which as consequence triggers the assert?
Looking over the fix just got me thinking. I could be completely wrong. I don't know the code at all.

[msoos]

Yeah, you are right, I am not 100% sure, but it seems fine. I have written a mail to the author of CCAnr, Shaowei Cai, so he can confirm :) Let's hope I was right -- otherwise, I'm quite hopeful I'll be told what the correct fix should be :)

Good point, but I have my fingers crossed and I have a plan for verification! Cheers,

Mate

[capiman]

Ok, thanks for your quick answer and clarification.

[jwaldmann]

This error is still present with crytominisat5 that comes with (brand new) Fedora-37. I guess that's because they still package version 5.8.0 (https://src.fedoraproject.org/rpms/cryptominisat/blob/rawhide/f/cryptominisat.spec)

[msoos]

OK, so this is just an old release that has this bug. Please use a static binary that is available on the top right, under "Releases", here: https://github.com/msoos/cryptominisat/releases

Thanks! Cheers,

Mate

[jwaldmann]

Yes, sure. I can build from source just fine. It's more of a bug in Fedora (them not using your current code). Perhaps some-one around here knows how to ping their maintainer.