Comment section of dimacs format

[rumia masburah]

Hi ,

Consider the following C file

int main()

{

int a=1,b=4,c;

c= a + b;

assert(c>10);

}

We generate the dimacs format (following --dimacs option) (attached)

Can any one explain the comment section of the file or share any resource regarding the same?

[Martin Nyx Brain]

I'm not sure we have anything written down as it's not really an
intentional feature (although a lot of people have asked about it, so
we probably should write something).

The comments are a map from the SSA names (the same ones from --show-
vcc) to the SAT variables that represent each bit. IIRC they are LSB
first. This is a dump of the map that is used to construct the
counter-example trace (--trace) from a satisfiable example.

HTH

Cheers,
- Martin