2021-01-27 10:17 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000240Frama-CPlug-in > jessiepublic2010-12-22 18:04
Assigned Tocmarche 
Product VersionFrama-C Beryllium-20090901 
Target VersionFixed in VersionFrama-C Carbon-20101202-beta2 
Summary0000240: Problems with solver configuration
DescriptionUsing the prover named alt-ergo v 0.9 no proof can be computed.

Why-config recognizes alt-ergo as version 0.9 correctly.

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
TagsNo tags attached.
Attached Files




Christoph (reporter)

This one concernes the GUI of the jessie plugin.


signoles (manager)

Available in Why3.

-Issue History
Date Modified Username Field Change
2009-09-11 15:51 Christoph New Issue
2009-09-11 15:52 Christoph Note Added: 0000393
2009-09-12 07:16 signoles Category graphical user interface => plug-in > jessie
2009-09-12 07:16 signoles Description Updated
2009-09-12 07:16 signoles Status new => assigned
2009-09-12 07:16 signoles Assigned To => cmarche
2010-09-16 14:51 cmarche Status assigned => resolved
2010-09-16 14:51 cmarche Resolution open => fixed
2010-09-16 14:51 cmarche Description Updated
2010-09-16 14:51 cmarche Additional Information Updated
2010-12-22 18:04 signoles Note Added: 0001351
2010-12-22 18:04 signoles Status resolved => closed
2010-12-22 18:04 signoles Fixed in Version => Frama-C Carbon-20101202-beta2
+Issue History