Problems with solver configuration
ID0000240: This issue was created automatically from Mantis Issue 240. Further discussion may take place here.
|ID0000240||Frama-C||Plug-in > jessie||public||2009-09-11||2010-12-22|
|Product Version||Frama-C Beryllium-20090901||Target Version||-||Fixed in Version||Frama-C Carbon-20101202-beta2|
Using the prover named alt-ergo v 0.9 no proof can be computed.
Why-config recognizes alt-ergo as version 0.9 correctly.
Solution?!: Renaming alt-ergo to ergo, the proof can be computed.
In both cases the GUI shows version 0.8 instead of 0.9.
But, since alt-ergo and ergo are both valid, which will be used?
(I would like to be able to add multiple version of alt ergo and to distinguish them by the names I have given them .)
Additional Information :
using multiple versions of the same prover will be available in Why3, released in december.
This will not be available in Why2