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

Martin Maurer meinemailingliste at online.de
Mer 19 Jan 19:55:51 CET 2011

Hello Vergard,

great work !

Do you already have "inline" eliminated ?
Can you create list files again for a working and non-working version ?

I just opened your attached main.cpp, std::swap is not more inside, or have 
i overseen it ?

Best regards,


----- Original Message ----- 
From: "Vegard Nossum" <vegard.nossum at gmail.com>
To: "Mate Soos" <soos.mate at gmail.com>
Cc: "Oliver Kullmann" <O.Kullmann at swansea.ac.uk>; 
<cryptominisat-devel at lists.gforge.inria.fr>
Sent: Wednesday, January 19, 2011 7:50 PM
Subject: Re: [Cryptominisat-devel] I need a bit of help 

> On 19 January 2011 18:29, Mate Soos <soos.mate at gmail.com> wrote:
>> 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


Cryptominisat-devel mailing list
Cryptominisat-devel at lists.gforge.inria.fr

More information about the Cryptominisat-devel mailing list