Fix unsoundness in incremental ALIA

[blishko]

Incremental solving including arrays and arithmetic contained a bug that could cause the solver to respond sat when the formula is actually unsat. The theory combination relies on creating interface lemmas in order for the individual solvers to agree if a pair of interface variables have the same value or not. Such interface lemmas are created on demand, lazily. However, the array solver may create new equalities (and introduce new variables to the SAT solver) when it formulates its new lemmas. In case of incremental solving, these outlive their frame in assertion stack after pop. They are still present in the core. If, afterwards, we assert the corresponding disequality (which gets split into inequalities), we miss the introduction of the interface lemmas, because the variables of the equality are not considered interface variables (they appear only in UF part of the formula in first frame, and, after pop, they appear only in the arithmetic part of the formula).

The proposed fix is to introduce interface lemmas in the case of equalities introduced by the array solver more eagerly. This, however, comes with a performance cost because we eagerly add (possibly unnecessary) interface lemmas.

[Tomaqa]

It seems to fix all remaining SMT-LIB benchmarks with arrays (QF_A*) under the timeout of 20 minutes. I also have noticed no significant performance drop.

[Tomaqa]

Resolves #710. I have discovered no new bugs even with 1h timeout.