Preliminary Array-Propagation engine

Suggestions need clean-up (they are effectively disabled now)
CClosure changes need review.
There is still code duplication in WeakCongruence versus Cursor.collect.
Note also that they need to create the same index disequalities, otherwise
propagation is unsound.
Bug Fix: do not simplify disequalities.

The code in ArrayTheory assumes, that the weak congruence will
simply use the index disequalities as is.  Otherwise the unit clauses
will not be unit clauses.  TODO: still have to check that the
propagated equality agrees between array theory and weak congruence
path.

Also the generated lemma was buggy, if the shared term disequality
simplified to false:  The equalities that lead to the shared terms
were missing.
Clean up suggestion code.

The suggestions were not used at all.  Using suggestions seems to make
the solver slower, as it contradicts the default DPLL heuristics.
Merge branch 'array' into arrayprop
Reverted the patch that I'm unsure of.

On backtracking it may be necessary to propagate congruences again.
This happens if a appterm was created on a non-empty decide stack.
Although this is not possible at the moment, we want to keep it
running in case we want to add triggers later.

Ugly: checked is always true in buildCongruence.  I don't think it
is necessary when it is called from checkpoint, but I play safe for
now.
Merge branch 'arrayprop' into array

Weak-over-eq lemmas are computed in checkpoint and if all but
one disequality in the conflict is set, the last is propagated as
an equality.  Also compute unit-clauses and conflict-clauses only
when needed.