--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on March 2015 ---
Hi, There seems to be something wrong with Frama-C/WP (Sodium) with 5 or more existential variables in the specification. // dummy.c void dummy() { double d = 7; //@ assert \exists real r1, r2, r3, r4, r5; d == r1 + r2 + r3 + r4 + r5; } > frama-c -wp dummy.c [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing dummy.c (with preprocessing) [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] 1 goal scheduled [wp] Proved goals: 0 / 1 In the example above, Frama-C/WP doesn't try to prove it. In addition, for the command below, it generate nothing. > frama-c -wp -wp-prover why3 -wp-gen -wp-out dummy dummy.c With 4 existential variables instead of 5, Frama-C/WP works fine. Am I missing something? Or, is it an issue of the new version of Frama-C? Thanks, Junkil -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150329/d9b033b4/attachment.html>