Observations:
- AssertOnly takes just about 1/2 of Assert time -- examine 'pending' (not true in general?)
- DPLL/AddClause takes 13% of time and is much slower than the C++ version (not true anymore?)
- in Q-DPLL assert(big monome) is called twice (though in the state where it is already asserted)


Dynamic strategy switching:
  - trigger selection
  - expensive theory reasoning
  - different instantiation strategy (bounded arithmetic)
Faster variable selection:
  - rebuild the heap when there is too much waste in it
  - some wise watching scheme for not-needed literals
Better stop condition needed for strategy switching.