Solver Reuse for Symbolic Execution and SMG2

Currently we create a new SMT solver (prover) every time we want to check the satisfiability of a formula, e.g. a path-formula in Symbolic Execution and SMG2. But using the incremental mode of SMT solvers, we can improve performance in many cases by not destroying a solvers prover and rebuilding it, but reusing it with the previously added formulas and learned lemmas.

This MR adds the option to choose how ConstraintsSolver uses its SMT solver:

• No Reuse (creates a new ProverEnvironment every time)
• Reuse the existing solver instance (ProverEnvironment). This builds your ProverEnvironment from the longest prefix of shared constraints already known to the solver.

Some benchmarks run on this branch vs. main can be inspected here. Note: runs with Incremental_common_prefix use the final solver reuse method.

The option for reusing solvers is per default now enabled, increasing solver performance. The option resolveDefinites is now disabled per default, as it brings only minor improvements in few cases while reducing the performance in significantly more cases, see #1352.