GitLab

              when one of the field is empty.

              (Thx Jean-Christophe)

Bugfix in the transformation prepare_for_counterexamp - the transformation introduce_premises must be run before the transformation intro_projections_counterexmp

It finished for why3prove but not finishedfor why3ide yet.

Add int.NumOf realization.

Signed-off-by: Claude Marche <Claude.Marche@inria.fr>

Move of the transformations introduce_premises and intro_projections_counterexmp to the end of the driver.
Note that this requires putting meta "inline : no" for every projection function to the source file.
Otherwise, declarations projection functions are removed and the transformation intro_projections_counterexmp fails.

Conflicts:
	examples/hackers-delight/why3session.xml
	examples/hackers-delight/why3shapes.gz
	theories/bv.why

- generation in the makefile
- proofs done
Remove complex axioms from Pow2int in bv.why.
Add guards in rotates axioms in bv.why.