[Cryptominisat-devel] I need a bit of help debugging CryptoMiniSat

Vegard Nossum vegard.nossum at gmail.com
Mer 19 Jan 19:50:41 CET 2011


On 19 January 2011 18:29, Mate Soos <soos.mate at gmail.com> wrote:
> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>
> Dear Vergard,
>
> On 01/19/2011 06:14 PM, Vegard Nossum wrote:
>> I created a new Main.cpp which defines a new class Solver2, which is
>> MUCH smaller than the regular Solver. It uses Var, Lit, vec, and
>> ClauseAllocator from the other files, so the next step is to eliminate
>> those as well. So you see this new file also demonstrates the same
>> problem, but with a much simpler program now. This is the output:
>>
>> $ for o in 0 3; do echo -n "-O$o: "; g++ -Wall -O$o -ISolver -Imtl
>> -IMTRand -o test Main.cpp Solver/ClauseAllocator.cpp && ./test; done
>> -O0: success
>> -O3: error
>
> All I can say is: WOW :) I've spent a whole day to isolate the problem
> from 13'000 LOC to a couple of lines in a function and all its
> dependencies, and you have managed to isolate it down to maybe only
> 1-200 LOC in just a couple of hours! The way this goes, the bug will be
> squashed today :) I am so looking forward to CryptoMS 2.9.0, finally
> without bugs ;)
>
> I will work on this right now,

It's not that amazing, because you already told us where the bug was
in the first e-mail:

>    if (c[0] == ~p) {
>        std::swap(c[0], c[1]);
>    }

See next one (attached), it's completely independent of any other
files and still exhibit the same behaviour:

$ for o in 0 3; do echo -n "-O$o: "; g++ -Wall -O$o -o test$o Main.cpp
&& ./test$o; done
-O0: success
-O3: error

I can't really see what makes the difference and I tried to isolate it
even further in various ways (but then only getting "success" from
both programs).

Maybe I'll start trying out different gcc flags now, to see what makes
a difference.


Vegard
-------------- section suivante --------------
Une pièce jointe autre que texte a été nettoyée...
Nom: Main.cpp
Type: text/x-c++src
Taille: 1512 octets
Desc: non disponible
URL: <http://lists.gforge.inria.fr/pipermail/cryptominisat-devel/attachments/20110119/ed7969af/attachment-0001.cpp>


More information about the Cryptominisat-devel mailing list