GitLab

to the counter-example model.

This line must be marked with the label "model_vc".
If VC line is postcondition, it can be marked with the label
"model_func" or "model_func:func_name". Terms corresponding to
old values of arguments will be marked with @old, term corresponding
to the function result will be marked with @result or
func_name@result if func_name was given.

Pretty printing of model element names in counter-example.
Possibility to print differently model elements corresponding to
function result, old values of function arguments and other model
elements.

displayed in any case (even if the debug flag whyml_wp is not given).

Merge branch 'counter-examples' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3 into counter-examples

Conflicts:
	src/core/model_parser.ml

new module mach.int.Refint63
new module mach.int.MinMax63
new module mach.matrix.Matrix63
mach.array.Array63: type array renamed into array63

Conflicts:
	examples/warshall_algorithm/why3session.xml
	examples/warshall_algorithm/why3shapes.gz
	modules/matrix.mlw

Matrix.get and Matrix.set are now currified
no more matrix.MatrixSyntax

maps Why3 type int to OCaml type int
this is of course unsafe, unless one has proved absence of overflows