Optimize or disable simplify_trivial_quantification
The transformation simplify_trivial_quantification
has been disabled in most drivers back in 2011 (see 54cd6e48).
But this transformation is enabled in the colibri driver.
When investigating a ticket on the SPARK side about Why3 running at full processor capacity without calling any prover for 30+ minutes, the bottleneck seemed to be this transformation.
Still on the SPARK side, I have tried to launch the complete testsuite with and without this transformation in the colibri driver: the runtime of the complete testsuite drops from 66 minutes to 38 minutes with only few proof regressions.
I create a ticket to discuss whether we want to investigate further why this transformation is taking so long, or if we simply want to disable it in all drivers.