Suggestions for further improvements of PA engine

[blishko]

Things that should be tried:

• Experiment with different exploration strategies. Currently, the CHC system is explored in BFS-like manner. Maybe DFS or more complex strategy work work better.
• Try to avoid so many SMT calls when checking satisfaction of predicates. Maybe multiple predicates could be checked together, similar to how we check lemmas to be pushed to the next frame in SpacerContext::tryPushComponents? Another option is to simplify the query up front as much as possible, for example by constant propagation on state variables.
• Run more preprocessing passes to simplify the system as much as possible before passing it to the actual backend algorithm.