* all the provers with the same prover_id are threated as one prover,
* the first description of a prover in the file pdd.conf which have an
  executable with a good version is used,
* the order used to test the executable (exec) inside a prover description
  is not specified,
* a version_bad allows to forbid a version.
* a version_ok matches no warning is printed
* a version_old matches a warning is printed
* if no version matches a warning is printed

z3_smtv2* .drv : factorized

	 of a file into a driver

include "toto.drv.import"

Clarify documentation.

Perform intros before abstraction, since abstraction would otherwise erase the goal due to the presence of quantifiers.
The bug was introduced in 589890aa.

In the Gappa printer, perform a pseudo-congruence on the goal and move the introduce_premises transformation after abstraction.

Goal
  h (f x) = 1 /\ f x = g y -> h (g y) = 1
is now transformed by fmla_cond_subst into
  h (g y) = 1 /\ f x = g y -> h (g y) = 1
which can now be abstracted to
  abstr = 1 /\ abstr1 = abstr2 -> abstr = 1.

Add function fmla_cond_subst that converts equalities/disequalities into a substitution and returns an equivalent formula.

Avoid lazy variables in the Gappa printer, as it might happen that two tasks do not share the same environment.
See http://lists.gforge.inria.fr/pipermail/why3-commits/2011-April/000053.html for details.
There are still global references to unary minus symbols, but they are now refreshed each time.

As a side effect, it brings support for integer division with Gappa for free.

First step in removing hardcoded symbols from Gappa printer: work on identifiers instead of symbols.

This makes bench/valid/intreal.why pass with Gappa.

This fixes the following assertion failure:
anomaly: File "src/printer/gappa.ml", line 182, characters 19-25: Assertion failed

Before:
File "b/../b.why", line 7, characters 36-37This term has type int but is expected to have type real

After:
File "b/../b.why", line 7, characters 36-37:
This term has type int but is expected to have type real