Clean up CC-Lemmmas, especially ArrayLemmas

Lots of duplicated code removed.  WeakSubPaths are SubPaths.
The subpaths are now explicitly collected in an array of all paths.
The subpaths are ordered correctly.
The subpath annotation no longer remembers the literals (they are in
the clause anyway).
Cache produced smt terms.

This is necessary for proof production.
FIXME: I would rather like to have this in an extra hash table that is
given as parameter to toSMTTerm.  This way we would save a pointer for each
CCAppTerm.
Added ProofChecker and option proof-check-mode.
Bug fix for CC annotation patch

Let it compile with Java-1.5 again.
Checkstyle issues
Exponential grow in scope lists.

This improves run-time from quadratic to linear on average.
We grow by a factor of 2 and shrink by a factor of 2.
Shrinking is only done if the table is filled for less than
a quarter.
Checking for free variables faster.

Added a specialised procedure that checks for free variables, instead
of computing getFreeVars() for every sub term.
Fixed removal of unused fresh symbols.

The removal code did not correctly complement the set of used definitions
leading to left-over definition of fresh function symbols created as pre-
commands for some term commands.  Now, these declarations should be correctly
removed.
Merge branch 'master' into after-smtcomp
added test file for most aux axioms.

I did not manage to trigger
 * AUX_TRUE_NOT_FALSE
 * AUX_OR_POS
Improved .gitignore.
Added test for or-pos aux axiom.

Note that the proof is not correct for the last case.  The
tautology clause is not flat but used directly with @clause.
Added test for AUX_TRUE_NOT_FALSE
Make array-store/diff a tautology, not a lemma.

There is no reason why the div aux axioms are tautologies, while
the array aux axioms are lemmas.  They are both generated from a
single input clause and easy to interpolate.
Make eq a lemma instead of a tautology

A lemma is something that needs to be interpolated, a tautology is
created from a single source assertion.
Normalize lira smtaffineterm to int if possible.

Renamed toReal in typecast, since it is also used for integer cast.
Convert real SMTAffineTerm to int in createEqualityProxy, if all coefficients
are of type int.
Support interpolation of non-arrays in array logic

Only return unsupported if the proof of unsatisfiability contains
an array axiom.
Merge branch 'master' into after-smtcomp
Bugfix: clausifier setup in copy-constructor

Put the code to setup the clausifier and engine that is shared
between the copy-constructor and setLogic into a new method
setupClausifier
Bugfix: Unsoundness in QF_UFLIRA

Create equalities between int an real always in the linear arithmetic
solver, so that it can check for integrality.

Added a test case that shows a bug in the Cut-generator.  We currently
diverge on this benchmark.