Removed PDF file, time stamped documents.

The date is now hard-coded in the TeX file.
Removed the PDF file.
Ignore TeX files.
Cleaned up documentation.

Removed outdated files.
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.
clean up annotations.

Remove getSExpr() from IAnnotation.
Simplify RuleKind enum.
Fix solver setup for logic QF_AX.
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.
Merge branch 'after-smtcomp' into prooftracker