C extraction cosmetics

See merge request why3/why3!32

Naming proposition for expl of transformations with arguments #191

See merge request why3/why3!28

the beginner transformation `split_vc` is now using `introduce_premises`
followed by `subst_all`, instead of `simplify_trivial_quantification`
followed by `introduce_premises`.

following Andrei's suggestion, instead of `subst_all` we instead substitute
only the symbols that (1) were introduced earlier and (2) do not have
any attributes `[@model...]` so as to keep symbols present in the initial
code.

Fix issue #190

Closes #190

See merge request why3/why3!27

This puts explanations on goals generated by some transformations with
arguments. Ideally, no goals should be without explanations.

Exceptions from transformations are of two kinds:
- fatal exception which are then raised into a popup in the ide
- normal exception which appears in the message view

This updates values of already failing counterexamples which were changed
by the fix for z3/encoding_twin in 4b79dcf1.

also, the callback for transformation `remove` is not called when transformation fails,
preventing the display of numerous error messages in the IDE

Not done for low-level TypeMismatch exception in Ity.
However, this should not be an issue, since the majority
of type errors happen in Dexpr and will be reported with
qualified names.

ce-bench now fails when there is a diff

See merge request why3/why3!25

This decreases the memory consumption by 10% on multiprecision/add.mlw.

Sept merge new ide

Closes #161 and #160

See merge request why3/why3!24

This intends to add improvements that were done in new_ide but not merged
in master yet.
In particular, this merges
- the commit for interruption of provers in why3server.
- several counterexamples improvements:
  * choice of pretty printing for float counterexamples
  * countereamples parsing of lowercase "lambda"
- itp_server/controller_itp improvements:
  * error handling in itp_server (any_from_node_ID is now option)
  * reformating of controller_itp queues as record instead of tuples
  * choice to always give a new goal with the automatic function that gets
next goal

Conflicts:
	bench/ce/algebraic_type_CVC4,1.5.oracle
	bench/ce/algebraic_type_Z3,4.6.0.oracle
	bench/ce/array_records_CVC4,1.5.oracle
	bench/ce/array_records_Z3,4.6.0.oracle
	bench/ce/arrays_CVC4,1.5.oracle
	bench/ce/arrays_Z3,4.6.0.oracle
	bench/ce/floats_CVC4,1.5.oracle
	bench/ce/floats_Z3,4.6.0.oracle
	bench/ce/if_decision_branch.mlw
	bench/ce/if_decision_branch_CVC4,1.5.oracle
	bench/ce/if_decision_branch_Z3,4.6.0.oracle
	bench/ce/int.mlw
	bench/ce/int32_CVC4,1.5.oracle
	bench/ce/int32_Z3,4.6.0.oracle
	bench/ce/int_CVC4,1.5.oracle
	bench/ce/int_Z3,4.6.0.oracle
	bench/ce/int_overflow_CVC4,1.5.oracle
	bench/ce/int_overflow_Z3,4.6.0.oracle
	bench/ce/jlamp0_CVC4,1.5.oracle
	bench/ce/jlamp0_Z3,4.6.0.oracle
	bench/ce/jlamp_array_CVC4,1.5.oracle
	bench/ce/jlamp_array_Z3,4.6.0.oracle
	bench/ce/jlamp_projections_CVC4,1.5.oracle
	bench/ce/jlamp_projections_Z3,4.6.0.oracle
	bench/ce/map_CVC4,1.5.oracle
	bench/ce/map_Z3,4.6.0.oracle
	bench/ce/real_CVC4,1.5.oracle
	bench/ce/real_Z3,4.6.0.oracle
	bench/ce/record_map_CVC4,1.5.oracle
	bench/ce/record_map_Z3,4.6.0.oracle
	bench/ce/records_CVC4,1.5.oracle
	bench/ce/records_Z3,4.6.0.oracle
	bench/ce/ref_CVC4,1.5.oracle
	bench/ce/ref_Z3,4.6.0.oracle
	bench/ce/simple_array_CVC4,1.5.oracle
	bench/ce/simple_array_Z3,4.6.0.oracle
	src/core/ident.ml
	src/core/ident.mli
	src/parser/parser.mly
	src/printer/alt_ergo.ml
	src/printer/smtv2.ml
	src/session/itp_server.ml
	src/transform/eval_match.ml
	src/transform/intro_projections_counterexmp.ml
	src/transform/intro_vc_vars_counterexmp.ml
	src/whyml/mlw_wp.ml
	tests/demo-itp.mlw

not updated:
- stdlib/array - the proof is broken
- ring_decision/ - not replayed, proof broken
- in_progress/, util/, prover/bench/ - not replayed

[transform apply] let is now a premise for applied condition of apply

See merge request why3/why3!23

For framac

See merge request why3/why3!21