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