More efficient mutate code.

The old approach was quadratic in number of shared variables.  This version
should only be linear, but still also linear in number of columns and
linear in number of mutations.
Bug fix: new mutator
Improved version handling; clean-up.

Removed old smtlib2/smtlib Main files, which are superseeded by
smtinterpol/Main.  Removed old version handling (Version.java).
The version is now read from a property file.  This property file
is created by the ant build script.  If the property file is not
present (e.g. in a local git checkout) unknown-version is given
as version string.  The version string now also contains the
information whether it is the competition version.
Updated distribution target for new version code.
Bug Fix: Mixed LA interpolation.

We added the epsilon with the wrong sign to produce s3 < 0.
This caused an assertion error (but toLeq0() did actually produce
s3 < 0 correctly).
Fixed Expensive Assert logic.

The assert was only executed if EXPENSIVE_ASSERT is false.
Fixed Bug in DeltaDebugger for TermListCmds.

The delta debbugger ran into an endless loop if a term list consisted of only
one term.  Now, such term lists are not simplified anymore.
Bug Fix: computing eps honors shared disequalities

Previously, we did not care about shared disequalities when
computing epsilon.  Previously, in a situations where the solver
has the pre-model a != b, a = 1+eps, b=2, it could choose eps=1
which lead to assertion errors and wrong models afterwards.
Check for TerminationRequest in Clausifier
Fix warnings.
Fixed some PMD warnings.
Fixed a crash in the delta debugger.

The delta debugger made a wrong assumption while removing neutral elements.
This lead to a crash when for example an "and" could not be replaced by "true",
but had to remain.  Now, I try to replace it by a binary "and" with parameters
"true" and "true".
Fixed bug in DeltaDebugger.

removeNeutrals was broken in the delta debugger for numeric terms as well.  Now
we replace an empty sum by the sum of two zeros.
Bug Fix: Fix computation of mCount
Smaller LA clauses.

We now check on a set literal if its negation was already propagated
and in that case just return a conflict clause using getUnitClause.
Also when generating a clause, we use the annotation, which already
removes literals that go in positively and negatively with the same
amount.
Build deltadebugger (patch from array branch)
Merged Deltadebugger from array branch
Ensure monotonicity of termination requests.

Once termination is requested, SMTInterpol will keep this state until the next
pop command which will restore the previous state.
Fixed some PMD warnings and infos.

Some variables are made final others are not declared before an exit point of
the function that does not depend upon them.
Fixed a bug in the proof production.

We now normalize every SMTAffineTerm as soon as possible (when creating them).
This fixes a bug in the proof where normalization was not tracked but actually
changed the resulting term.