* time limit set to 1 sec. Quicker, and results are the same !

* use Stdlib whenever possible

* FIXME: the use of StringMap.bindings should not be useful, and wastes time and memory

otherwise, superfluous diff may show up

Formerly we only parsed elements of float values as decimals when they can
be hexadecimal.

* src/driver/parse_smtv2_model_lexer.mll
(float_num): Now takes hexadecimal number instead of decimal numbers.

Change-Id: Ie3c4e3452c7cb68af8767d2859bfbb4bb90e607e

This commit adds parsing for boolean expression and floating point value
which are returned by z3 on the last version. This adds floating point
values in the collected data and JSON printed data. This does not add
boolean expressions because it does not add information.
Also added transformation eliminate epsilon in driver for Z3 ce.

* drivers/z3_gnatprove_ce.drv
(eliminate_epsilon): Added transformation eliminate epsilon in driver for
counterex for z3.

* src/core/model_parser.ml
(float_type): Added a float_type and functions to send it as JSON data.

* src/driver/collect_data_model.ml
(convert_array_value): Explicit matching for error handling when adding
constructs.
(convert_float): Dummy conversion of float_type to avoid circular
dependency.

* src/driver/parse_smtv2_model_lexer.mll
(token): Adding z3 specific boolean expressions. Also adding a way to
parse all floating point value including those we don't want to print
because we need to parse them even if we don't want to print them.

* src/driver/parse_smtv2_model_parser.mly
(smt_term): Adding floating point value case which is handled in the lexer.
Added boolean_expression case.

* src/driver/smt2_model_defs.ml
(float_type): Adding a duplicated float_type for dependencies reasons.
(print_float): Debugging print of float_type.
(): Adding cases for float in remaining functions.

Change-Id: I5baee2880a9843f0fec61b1bf3edb2a2f3e54bd1

This commits allows printing of arrays which have indices typed as
bitvectors.

* src/driver/collect_data_model.ml
(convert_to_indice): Add bitvector case.

Change-Id: Iafe10e5e6cd1aab0a3e023aeb69df03fde8880e8

from a commit by Florian Schanda in 2013 (Spark repo 9b954f4).

On N127-001, an optimisation of the fast WP was introduced, based on
marking states that contain variables that need to be refreshed when
merging them. However, this "marked" status was incorrectly reset to
false when merging states, even though some of those "unfresh" variables
could survive the merge. The consequence was that the WP was reusing
variables too aggressively, which would result in incorrect VCs.

We now compute the marked status of a merged state from the states to be
merged: if one of them is marked, the merged state is marked too.

mlw_wp.ml:
(merge): synthetize marked status from input states

Change-Id: Ifb02c54fca58137c31762469e48b59e7c907b995

- most important improvement : the explanation, used as first part
  of the shape was computed twice ! (at least)
- several improvements in the implementation, avoid using Format
  in particular (done also in checksum computations)
- possible further improvements:
    do not compute shapes if checksums are OK
       (they must be the same as in previous session)
    do not compute goal checksums if theory checksum is OK
       (they must be the same as in previous session)

If drivers in why3.conf are simple names like "alt_ergo", then the driver file
is search as <datadir>/drivers/alt_ergo.drv

This behavior is now the same as when a driver is given with option -D on the
command line for why3prove, why3replay or why3extract

Reminder: the datadir is either given as
1) the environment variable WHY3DATA
2) the field "datadir" of the [main] section of the
   why3 config file if exists
3) or by default the compile-time datadir

The underlying Monoid does not need to be commutative,
and is indeed not in example fibonacci.mlw