Jaisurya Nanduri

Relevant PR is in the extension repo.

https://github.com/model-checking/kani/pull/2353 Adds an E2E unit test that also runs the generated unit test to get the output. (The test for generating the unit test is already present in the UI...

Related PR: https://github.com/model-checking/cbmc-viewer/pull/147 & https://github.com/model-checking/kani/pull/2879

Replicating this issue in a ubuntu environment, gave this response - `../../../github/home/.rustup/toolchains/nightly-2023-09-19-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/builders.rs:33:16 in function ::write_str` What this tells me is that, the path to the toolchain is being hardcoded from...

The changes suggested here have been merged in other PR's referred above with modifications. I think this issue can be closed. Thanks @sanjit-bhat for your work!

Ran into this issue while adding the concrete playback button for the extension, this causes all cfg(test) or #[test] cases to crash and it gives the same underlying error.

Would removing the transmute theoretically remove the dependency on nightly features entirely? If so, that seems like the cleanest solution and option. But i imagine, we need `incomplete_features` for Arbitrary...

> I think I'm having the same issue here. I'm trying to run a basic harness that imports a struct with a lot of dependencies. I run it with `cargo...

Branch with progress so far: https://github.com/jaisnan/kani/tree/turn-clause-to-contract

Hi @weaversa , is there any information about your invocation that you can provide that could help us reproduce this crash? Some details that would be useful are 1. The...