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.