o changed assumes into commands
o added assert commands
o added line numbers to step proof obligations
o added command line options to the continuous program: -c makes it
continuous, -V makes it verbose, i.e. it prints the successful
verification conditions