Sriram Sankaranarayanan wrote:

The new tarball is attached. I could have generated a patch, but this is easier

Just to make sure.. Here are the versions of things I am using

srirams@Dali:~% g++ --version

g++ (GCC) 3.2.2 20030222 (Red Hat Linux 3.2.2-5) Copyright (C) 2002 Free Software Foundation, Inc.

srirams@Dali:~% flex --version flex version 2.5.4

srirams@Dali:~% ~/bin/bison --version bison (GNU Bison) 1.875c Written by Robert Corbett and Richard Stallman.

I am using GCC 3.4.2, Bison 1.875d, and Flex 2.5.4. There is only one problem in the sources you sent:

MatrixStore.cc:14: error: array bound forbidden after parenthesized type-id MatrixStore.cc:14: note: try removing the parentheses around the type-id

This can be easily fixed by changing the guilty line to

mat= new Rational*[n]; // the last column is the $b$ augment

I tried it with your latest ppl bug fix, it works. Thanks for fixing that.

Thanks to you for your report!

I have packaged the examples in with the src under lsting-src/Examples

If you run

lsting invcheck < inputfile

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? :-)

I hope this works without further troubles.

It seems it does. We will use your program regularly for regression testing. Thanks! All the best,

Roberto