Open MathieuSoysal opened 4 months ago
The error message is reporting that the string used in the println!
is not supported. At the moment, there is not much that we do to veryify I/O or string properties. To work around the error you could mark play_game
as #[trusted]
, meaning that it won't be verified.
If you still want to prove some properties about it you could, for example, add a parameter to counts how many times the play_game
function has been executed. This makes it possible to prove properties in the code that calls play_game
. However, it depends a lot on what you want to do.
#[trusted]
#[ensures(*counter == old(*counter) + 1)]
pub fn play_game(n: u32, counter: &mut usize) {
println!("{}", fizz_buzz_fibonacci(n));
counter += 1;
}
Current code:
But I obtain this error:
Someone know how to fix it ?