diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml index 72ab4fc4ef117ae2e07833a2f68f9ecfc901e415..513c205deeacdeef55bdc3c3f05713a9800eb399 100644 --- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml +++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml @@ -54,7 +54,8 @@ let run () = pred_content = Cil_types.Ptrue; } in - let annot = Logic_const.new_code_annotation (AAssert ([],Assert,pred)) in + let pred = Logic_const.toplevel_predicate pred in + let annot = Logic_const.new_code_annotation (AAssert ([],pred)) in let po = Wpo.{ po_gid = ""; po_leg = "";