If the extension throws an error message for a harness that looks like this
You can inspect the crash logs by going to the output channel and searching for a channel called Error (Kani) ...
.
If there is no helpful information available there, please file an issue.
The extension runs on Cargo packges exclusively. For standalone Rust files, Kani is only available on the command line.
You can create a new Cargo package using cargo init
or cargo new
.
If verification seems to be taking too much time, stop the verification using the stop button that looks like a square on the testing panel.
If the output seems unexpected, it might be because of an old result cached in. It helps to run cargo clean
and re-running the harness.
If the screen seems frozen, or inactive, try reloading the vscode window.