Speedup ideas:

- implement separate Array theory
- implement separate Subtyping theory
- check why 3-level sat solver doesn't work
- do some wise case-split accounting (we have all the info)
- bump literal activity based on usefullness
- organize some kind of priority queue for ``bad'' instances
- instance clustering by shared, new literals
- in 2-level sat -- examine if we changed the main patch and if yes -- try the useful axioms first
- kill ExpandITE (preprocessing?)
- resimplify -- keep new literals and assert clauses when they become true/false (likely to cut only theory costs)


- re-minimize the small sat conflict clause