--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on April 2019 ---
Hi I've been eyeing over the ACSL spec and the frama-c manpage to see if it's possible to keep/reuse expensive proofs, or generate ACSL code corresponding to them, in some human-readable format. I currently have one assertion in a function that computes an average that takes 30 seconds for Z3 to prove, which is a bit annoying. I gave -save and -load a try, but those mostly seem to exist to be able to resume a frama-c run. Likewise -session doesn't seem to do much. I feel like I'm missing something obvious.. My invocation currently looks like this: frama-c -wp -wp-rte -wp-timeout 30 -warn-unsigned-overflow -wp-prover z3,cvc4,alt-ergo,qed proven.c What am I missing? /Tomas