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

Vegard Nossum vegard.nossum at gmail.com
Mer 19 Jan 22:42:54 CET 2011


On 19 January 2011 21:24, Martin Maurer <meinemailingliste at online.de> wrote:
> Hi all,
>
> just some comments, don't know if relevant:
>
>>  Lit(int var, bool sign):
>>  x(var + var + (int) sign)
>>  {
>>  }
>
> I think bool must not be 0 and 1, but 0 and not zero (every value beside 0).
> So could it be that sign has values outside 0 and 1 ?
>
>>  int var() const
>>  {
>>  return x & 1;
>>  }
>
>>  bool sign() const
>>  {
>>  return x >> 1;
>>  }
>
> In sign() i get a warning (/W3) with MSVC telling cast is needed from x to
> bool. Perhaps add one ?
> Perhaps change to real if statement and return to true and false.
>
> Are these both function also like this in reality ? sign is shifted right by
> 1, so a lot of bits used just for sign.
> And return value of var() can only be 0 and 1. But perhaps it was written
> down only to get it compiling, no real implementation... ?

Heh, you're right, I actually swapped the implementations of var() and
sign(). But no matter, it apparently didn't make a difference for the
example.

Meanwhile, I asked the gcc guys on IRC -- they were able to produce an
even further simplification of the code:

struct Lit
{
  int x;
};

struct Clause
{
  Lit data[2];
};

Clause c = { 0, 3 };
Lit p = { 1 };

void
prop ()
{
  if (c.data[0].x == p.x ^ 1)
    {
      Lit t = c.data[0];
      c.data[0] = c.data[1];
      c.data[1] = t;
    }

  if (c.data[1].x != p.x ^ 1)
    __builtin_abort ();
  if (c.data[0].x == 0)
    __builtin_abort ();
}

int
main ()
{
  prop ();
  return 0;
}

...and they seem to think it's a bug as well. This test-case
apparently fails for 4.5 but works in 4.4 and trunk. Which means it
may be fixed in the latest version (not released), but they would like
to file it as a bug anyway (somebody's on it).

Compiler bugs are nasty!


Vegard



More information about the Cryptominisat-devel mailing list