--- layout: fc_discuss_archives title: Message 85 from Frama-C-discuss on October 2013 ---
Thank you for your reply. However, we need to prove without the pragma JessieFloatModel(math). What is the problem? Best regards, Luciana 2013/10/22 Eugene Kornykhin <kornevgen at gmail.com> > Hi! You can use pragma to ask Jessie interpret floats as unbounded reals > # pragma JessieFloatModel(math) > > After that Alt-Ergo discharges all VCs succesfully. > > > Eugene > > > On 21 October 2013 16:03, Luciana Burgareli <luciana.burgareli at gmail.com>wrote: > >> Hi, >> >> This is a very simple example, but it was not proved. >> >> If we slightly modify the code and we add an assignment to the Ang2[1] >> (and the related assigns and ensures clauses), both the ensures clauses are >> proved. >> >> Why is not the attached example proved? >> >> How to solve this problem? >> >> We are using the Jessie Plugin, Why3 Verification Platform 0.81, >> Fluorine-20130601 and the provers Alt-Ergo 0.95.2, CVC3 2.4.1, Gappa 1.0.0 >> and Z3 4.3.2. >> >> >> Luciana >> >> >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss at lists.gforge.inria.fr >> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss >> > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131024/a9b2478a/attachment.html>