Variants and soundness guarantees
predicate p (x y : unit) = true
let rec function foo (x : unit) : unit
variant { x with p } ensures { false } = foo x
goal g : false
As far as I understand it, the rule of thumb has always been that, in absence of axiom
or val
, the system should be sound. So either this rule should also exclude the use of custom variant
, or Why3 should generate a proof obligation for the wellfoundedness of such relations.