-------- Original Message -------- Subject: Re: Source Code Date: Wed, 15 Sep 2004 10:01:23 -0700 From: Sriram Sankaranarayanan srirams@CS.Stanford.EDU To: Roberto Bagnara bagnara@cs.unipr.it

Dear Roberto,

Thanks for the fix! I fixed the problem in my version and it compiles fine. I am assuming you have already removed the offending brackets in yours.

...

it will print a message prefixed by the word ERROR on the stderr stream if something breaks (i.e, the computed invariant fails the inductive check.. which is finally all we care about :-)

Hey, but you proved it correct, didn't you? :-)

Yes.. but to quote Don Knuth, "Beware of bugs in the above code; I have only proved it correct, not tried it."

Sriram