Skip to content
Snippets Groups Projects
Commit 87fb97cc authored by Allan Blanchard's avatar Allan Blanchard Committed by Loïc Correnson
Browse files

[wp] fix lemmas registration

parent 905a4863
No related branches found
No related tags found
No related merge requests found
......@@ -164,14 +164,16 @@ struct
begin fun () ->
LogicUsage.iter_lemmas VCG.register_lemma ;
List.iter (fun l ->
let wpo = VCG.compile_lemma l in
collection := Bag.add wpo !collection
if l.LogicUsage.lem_kind <> `Axiom then
let wpo = VCG.compile_lemma l in
collection := Bag.add wpo !collection
) (List.rev task.lemmas) ;
end () ;
List.iter
(fun (mode : CfgCalculus.mode) ->
WpContext.on_context (model,WpContext.Kf mode.kf)
begin fun () ->
LogicUsage.iter_lemmas VCG.register_lemma ;
let bhv =
if Cil.is_default_behavior mode.bhv then None
else Some mode.bhv.b_name in
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment