diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index d6bc77f086a4b5a1202344190d8a0425ff607b53..12bdacececdc8d4b81f3e63d20815cb4348c9357 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -244,11 +244,17 @@ let get_terminates_hyp kf =
| Defined (_, p) -> false, p
| Assumed p -> true, p
+let check_variant_relation = function
+ | (_, None) -> ()
+ | (_, Some rel) ->
+ Wp_parameters.hypothesis ~once:true
+ "'%a' relation must be well-founded" Cil_printer.pp_logic_info rel
+
let get_decreases_goal kf =
let defined t = WpPropId.mk_decrease_id kf Kglobal t, t in
match Annotations.decreases ~populate:false kf with
| None -> None
- | Some v -> Some (defined v)
+ | Some v -> check_variant_relation v ; Some (defined v)
let get_decreases_hyp kf =
Annotations.decreases ~populate:false kf
@@ -475,6 +481,7 @@ let mk_variant_properties kf s ca v =
(vpos_id, vpos), (vdecr_id, vdecr)
let mk_variant_relation_property kf s ca v li =
+ check_variant_relation (v, Some li) ;
let vid = WpPropId.mk_var_id kf s ca in
let loc = v.term_loc in
let lcurr = Clabels.to_logic (Clabels.loop_current s) in
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index a0ce9b9ceb9002717941b0b7eb8ba911a7147c6c..1bece5f01aec932f3af778a959cd5f43e5a90461 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1153,11 +1153,12 @@ struct
Kernel_function.pretty kf
| (_, r), Some (_, r')
when not @@ Option.equal Logic_utils.is_same_logic_info r r' ->
+ let none : Pretty_utils.sformat = "<None>" in
Warning.error
"On call to %a, relation (%a) does not match caller (%a)"
Kernel_function.pretty kf
- (Pretty_utils.pp_opt Cil_printer.pp_logic_info) r
- (Pretty_utils.pp_opt Cil_printer.pp_logic_info) r'
+ (Pretty_utils.pp_opt ~none Cil_printer.pp_logic_info) r
+ (Pretty_utils.pp_opt ~none Cil_printer.pp_logic_info) r'
| (caller_d, rel), Some (callee_d,_ ) ->
let rel caller callee = match rel with
| None ->
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
index 767145c220c03197a7224d2ec0bdde5dfb30e024..1c0241e1df554d73e7532ba44337a17271391de2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
@@ -2,7 +2,9 @@
[kernel] Parsing decreases.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp:hypothesis] decreases.i:108: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:71: Warning: No decreases clause for missing_2
+[wp:hypothesis] decreases.i:108: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
[wp] decreases.i:105: Warning:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
index 337093493a982ac42bbbb4a4f3356b75a2460d2a..503c417688228f6147615930e14def6d47a18997 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
@@ -2,7 +2,9 @@
[kernel] Parsing decreases.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp:hypothesis] decreases.i:108: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:71: Warning: No decreases clause for missing_2
+[wp:hypothesis] decreases.i:108: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
[wp] decreases.i:105: Warning:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
index 7f2d6c08cd7b533456c5a10be2a2672df999650a..d9bd70618f767ce264637cc140e5ee6199eadd5d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
@@ -2,6 +2,8 @@
[kernel] Parsing terminates_formulae.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp:hypothesis] terminates_formulae.i:90: Warning:
+ 'Rel' relation must be well-founded
[wp] [CFG] Goal general_variant_terminates : Valid (Trivial)
[wp] [CFG] Goal variant_terminates : Valid (Trivial)
[wp] terminates_formulae.i:90: Warning:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.0.res.oracle
index a1c4020be5c7a8588d970801ea395150ab465677..62e79688690128fd49abbc91e54a2e4c560df53d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.0.res.oracle
@@ -2,7 +2,9 @@
[kernel] Parsing decreases.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp:hypothesis] decreases.i:108: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:71: Warning: No decreases clause for missing_2
+[wp:hypothesis] decreases.i:108: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
[wp] decreases.i:105: Warning:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
index 915be052f0a124108d616c119cefce648b34c930..63e3fba1f7426ce524df7c0e5c5f319d6f557091 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
@@ -2,7 +2,9 @@
[kernel] Parsing decreases.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp:hypothesis] decreases.i:108: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:71: Warning: No decreases clause for missing_2
+[wp:hypothesis] decreases.i:108: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
[wp] decreases.i:105: Warning:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
index 06ea7290c298cdd98ad984e8ba91747fe6475396..cf90d39ba3fc26032ba408a35e80cd1c1badb88a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
@@ -2,6 +2,8 @@
[kernel] Parsing terminates_formulae.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp:hypothesis] terminates_formulae.i:90: Warning:
+ 'Rel' relation must be well-founded
[wp] [CFG] Goal general_variant_terminates : Valid (Trivial)
[wp] [CFG] Goal variant_terminates : Valid (Trivial)
[wp] terminates_formulae.i:90: Warning: