Functions that are defined as @extern can use non-purescala features
within their body. Leon will reason about them according to their
specification (the unknown body becomes a hole and then a choose).

Implies(pre, f(x) = body)

becomes, with (--assumepre):

And(pre, f(x) = body)

- Detect definitions of ADTs that wil lbe problematic for solvers to
  handle. e.g. case class Ls(elems: List[Cons[T]])

- Use IncrementalBijections in native z3 solvers

- ADTManager is responsible for computing dependencies between ADTs so
  that definitions can be grouped.
- Simplify and generalize solver handling of RawArrays.
- Remove dead-code in fair-z3 to parse non-ground models.
- OptionManager was mostly useless, moved *Type to Library
- MapGet can be implemented as (Some-value (Select m k)),
  as the solver will treat Some-value as uninterpreted if Select yields
  a None

 * Fixed typo and wording in references
 * Streamlined intro opening

Multiple-file benchmarks are getting common nowadays, so we report the
files corresponding to the error to help debugging. File should be
relative to the CWD, when possible, absolute otherwise.

Refactor all existing Modulo into Remainder, as it is
the correct term in Scala for the operation %.

BigInt now supports `mod` operator, which gets represented
as Modulo in Leon.

This is necessary because what was there was invalid:
sorts<->types are not a bijection, since several Leon types compile to
the same sort (BV32) <-> (CharType, Int32Type).

By providing the expected type, we can reconstruct the correct model.
If the model uses expressions, we can no longer make sure we get the
right thing, and will guess using sorts.