Fix a bug in Simplifier

In a shared node, when merging contextes, CollectContext did not
update the mcontext array in the CollectContext-object, which is used for
collecting the contextes of the children of a shared node.
Made echo function publicly available in the Script interface.  Instead of adding a requested comment function to the Script interface or the LoggingScript, we decided to add the echo functionality instead.  Note that this function should not have any negative effect since it is mostly implemented as a no-op.  Only the LoggingScript actually does something more than returning the input.
Fixed endCheck notification

The notification was missing in all cases in DPLLEngine.solve.  This lead to bad performance and even worse interpolants in many cases.
Introduced proof rule distinctBoolEq.

This rule is used to transform a distinct term over Boolean terms into an
equality where one of the two terms gets negated.
Updated proof documentation.

The proof documentation was missing the rule :distinctBoolEq.  A presentation
of this rule was added.  To this point, no additional documentation is present
since the rule should be self-explanatory.
Fixed AssertionError in mixed integer logics.

LAEquality wrongly computed the type of the equality to Int even if the
value was a Real.  In this case, the variable will be wrapped by a
to_real and not be integral anymore.  However, this seems to be a good
point for optimization since equalities of the form (= i 0.5) should be
simplified to false and not be subject to the IRA-Hack.
Added Matthias' echo Simplifier commands.
Allow division by Rational.ZERO.

We erronously threw an exception instead of returning one of the special
values POSITIVE_INFINITY, NEGATIVE_INFINITY, or NAN.
Updated usage page and added version switch.

Also removed -e parameter for echo; this is not supported by some
shells and not posix conform.
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.
Merge branch master into array

Updated buildjar.xml to build delta-debugger.