--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on August 2014 ---
= short answer = you should do frama-c -jessie mean.c and run Z3 on all goals using the GUI. It is advised to split the goals in parts using "Split" if running Z3 on a whole VC does not work. = longer answer = There is no (easy) way to run a given prover on each VC generated by Jessie/Why3. The reason is that Why3 should not be used using a single prover like this. By running the Why3 GUI, the user should interact with the goals, splitting them, try various provers, change the time limit for some goals, inline some symbols, and generally speaking apply transformations. The session mechanism of Why3 is there to memoize all these tasks and replay them easily when modifying the output program. hope this helps, - Claude Le 31/07/2014 16:24, Artem Kalinovsky a ?crit : > Hi! > > I want run Jessie with Z3 and Why3 > > Now my command looks like this: > frama-c -jessie -jessie-atp z3 mean.c. > > I checked out that -jessie-atp calls Why2. How can I call why3 instead > of why3? > > I was trying to find answer in "jessie tutorial" but there was no > solution for my issue. > > Thank you! > > > > _______________________________________________ > 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 > -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |