diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 2e20c87f609994abbe5ea888efda2b9009527081..e1a4d022b51847f3e07d5f77f355ea37df86f5da 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -481,6 +481,9 @@ struct
   let add_vc
       target ?(warn=Warning.Set.empty) ?(deps=Property.Set.empty) pred vcs =
     let xs , hs , goal = introduction pred in
+    if Gmap.mem target vcs then
+      Wp_parameters.failure
+        "Multiple goals for the same target (%a)" TARGET.pretty target ;
     let hyps = Conditions.intros hs Conditions.nil in
     let vc = { empty_vc with goal ; vars=xs ; hyps ; warn ; deps } in
     Gmap.add target (Splitter.singleton vc) vcs