Frama-C Bug Tracking System - Frama-C
View Issue Details
0001683Frama-CPlug-in > wppublic2014-03-12 16:072016-01-26 08:52
jens 
correnson 
normalminoralways
closedfixed 
Frama-C Fluorine-20130601 
Frama-C Magnesium 
0001683: Number of discharged Qed goals counted multiple times
Here are the last lines of output produced by WP when verifying the copy algorithm. It appears that the Qed goals are counted several times. [wp] Proved goals: 16 / 16 Qed: 12 (2ms-8ms) Alt-Ergo: 11 (25ms-81ms) (70) cvc4: 1 (460ms-460ms)
In fact, I am running Frama-C Neon...
No tags attached.
Issue History
2014-03-12 16:07jensNew Issue
2014-03-12 16:07jensStatusnew => assigned
2014-03-12 16:07jensAssigned To => correnson
2014-04-03 15:16jensNote Added: 0005025
2014-10-13 13:49corrensonNote Added: 0005508
2014-10-13 13:49corrensonStatusassigned => resolved
2014-10-13 13:49corrensonResolutionopen => fixed
2015-03-17 22:17signolesFixed in Version => Frama-C Sodium
2015-03-17 22:18signolesStatusresolved => closed
2015-05-20 15:34corrensonNote Added: 0005921
2015-05-20 15:34corrensonStatusclosed => resolved
2016-01-26 08:51signolesFixed in VersionFrama-C Sodium => Frama-C Magnesium
2016-01-26 08:52signolesStatusresolved => closed

Notes
(0005025)
jens   
2014-04-03 15:16   
CVC4 results are also not correctly handled by -wp-report
(0005508)
correnson   
2014-10-13 13:49   
Fix committed to master branch.
(0005921)
correnson   
2015-05-20 15:34   
Fix committed to master branch.