[Cryptominisat-devel] I need a bit of help debuggingCryptoMiniSat

Vegard Nossum vegard.nossum at gmail.com
Jeu 20 Jan 00:25:44 CET 2011

On 19 January 2011 23:31, Mate Soos <soos.mate at gmail.com> wrote:
> Actually, I have posted this to gcc-help just half an hour ago, and the
> impression was also that this is a bug. Apparently, pre-4.6.0 compiles
> my version of the code[1] fine, but that's no guarantee by all means
> that the bug in gcc is fixed (as mentioned by Vegard). I am, by the way,
> very happy that we have managed to nail down a possible gcc bug, it was
> great working with all of you!

For tracking:


> Now that we know we are not responsible, a workaround needs to be
> thought up, as most people will not compile a new gcc for CryptoMS :). I
> think a version of the assert() I have mentioned will work fine, but I
> need to use release_assert() so that the assert stays in case NDEBUG is
> defined (i.e. for "Release" version of compilation). What do you think?

Here are some suggestions, some of them might require a bit of work, though:

1. Test for the gcc version in the configure script. Give a warning
and/or compile with lower -O level.
2. Test for the bug (using the test-case) in the configure script. If
it triggers, give a warning and/or compile with lower -O level.
3. Test for the gcc version using preprocessor magic and use #error to
abort compilation or print a warning at run-time.

In any case, it might be an idea to include the gcc version that was
used to compile CryptoMiniSat somewhere in the solver output? There is
a very simple way to do this -- the __VERSION__ macro is a string with
the gcc version.


PS: I wonder if this is the same bug that hit me initially with
--nthreads, because that too triggered using the -ftree-pre flag
(which is enabled in -O3) and it was also gcc 4.5.1...

More information about the Cryptominisat-devel mailing list