Unused variables are not in the model
use int.Int
let f (t : int) (x : int) : unit =
check { 0 <= x /\ x <= 0 };
()
Unused variables are not kept in the model. Here t
is not kept in the model. Thus, if we tried to execute the program to check the counter-example, we get (why3 prove -a split_vc -P CVC4,1.8,counterexamples -L share/ f.mlw --check-ce --rac-prover=cvc4
)
The following counterexample model could not be verified
(both RAC terminated because missing value for parameter `t`)
If we add an underscore in the parameter _t
, this time it is kept in the model and the model can be checked.