Single-Property, Multi-Engine Distribution IFV now supports running multiple engines in parallel to prove assertions. You can take advantage of multi-core/multi-CPU machines to maximize performance and reduce proof runtimes. There is no need to experiment with engines and no need for multiple IFV runs with different engines. You now can run all available engines in parallel.
You can enable this capability by simply supplying a list of engines to the define engine command. Three engines (sword, axe and bow) are now supported in distribution. More engines will become available in subsequent IFV releases.
# Select 3 engines to run in parallel define engine sword axe bow
# Select 2 engines to run in parallel define engine sword axe
Note the following regarding distribution: