Execution of counter-example fails with pattern matching
With the following program
type option = None | Some int
let f (a: option) : unit
ensures {
match a with
| None -> false
| Some a -> true
end
}
= ()
why3 fails to execute the counter-example return by the prover with the option --check-ce
.
My command line is why3 prove -P CVC4,1.8,counterexamples --rac-prover=cvc4 --check-ce fails.mlw
and I get the error anomaly: (Failure "model term has no location")
.
If I rewrite this code without pattern matching (ensures { a <> None }
), the model is executable.