[PPL-devel] Bug in PPL?

[Roberto Bagnara]

Dear Roberto,

If you run lsting invcheck < berkeley.in, you will notice that the 
output of CH79 fails to be inductive.  The bug only happens when you compile
the code with the boring diagnostic messages turned off.

I also noticed that adding the line

 ConSys cs = my_poly.constraints();

just before I widen my_poly (InvariantMap.cc Line 94) corrects this problem.
I am still clueless  about this. It is not like I use "cs" for anything else.
It is just a dummy call.

Does it have to do with the fact that the widening may not work properly
if the constraint representation is stale or missing, or something?

I noticed this "fix" because I turned the printing diagnostics on, and
the bug disappeared. The only extra thing I do when I print is to ask
for the constraints and pretty print them.

As usual, I could be missing something obvious :-) , or it could be 
a bug. If you could point me out
to the right direction, I am very grateful. In the meantime, 
the release I sent you has the same bug which is absent in the older version.
So please ignore the code. I will send you a new version when I fix this bug.

Thanks,
Sriram