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.
Some more comments in cut creator
Merge branch 'after-smtcomp'
Newline after log message.

When the formatting version of the log method was used, no new line was
introduced and the writer was not flushed.  This update fixes this problem.
Merge branch 'master' into logger

Conflicts:
	SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/smtlib2/SMTInterpol.java