Add performance tests for larger interactions

[kfriedberger]

We should test the performance of basic operations like:

• push, pop, addConstraint
• creating large amounts of variables
• creating large (but cheap) formulas
• creating and closing several prover environments
• creating and closing several contexts

This test is not intended to check the performance of a SAT/SMT engine, but only the basic data structures, e.g. for managing memory.

There are at least the following points to consider:

• stack size: some solvers (mainly Princess) heavily depend on stack size.
• heap memory: creating simple objects should be cheap and not exceed the available memory of about 2GB, for example.
• typical size of default data structures: we do not expect any user to create objects in a number of MAX_INT, but we (and the solvers) should be able to handle several thousand objects.

The following points appeared after a few tests:

• deep recursive methods without possible early abort.
  Example: Princess seems to call equals() (implemented recursive on the formula) sometimes without obvious reason and crashes, debugging needed.
• invalid choice of data structure.
  Example: SMTInterpol seems to track INT symbols in a ArrayList and removes each of them separately on pop in reverse order. -> quadratic runtime?

There might be more simple-to-catch problems.
We should report them to the corresponding solver developers.

[kfriedberger]

The implementation can be found in the branch https://github.com/sosy-lab/java-smt/tree/interaction_performance

[kfriedberger]

Info: The PR for SMTInterpol is here: ultimate-pa/smtinterpol#127 (merged on 2021-07-19)