Sanjit Bhat

@tedinski you're right that the bits are consistently interpreted in the current implementation. The bit patterns are relevant in the following test: https://github.com/model-checking/kani/pull/1488/files#diff-d6edfd434ccfd2ab84a988fbf2909ad26a6e1d7553f909d268a463e29faa9d03R9-R10 with expected output here: https://github.com/model-checking/kani/pull/1488/files#diff-0f14a3452f9e948e47159f2f28eddffe6f7a951d8c87bea823ba980045a55906R7-R10 This test...

@zhassan-aws It's a limitation of the test cases for the executable trace feature. This limitation might be removed in the future once I add additional test functionality to run the...

Hm, that verifies, even if I replace `as` with `transmute`. I'm confused why that's the case. I thought the underlying bit pattern (the `let byte = u8::any()`) can be any...

Ah, that makes sense now. Thanks everyone for helping to clarify that! @tedinski @celinval @zhassan-aws I updated the title to reflect the fact that this issue is not a problem...

## Performance eval of switching to new `any::()` Configurations: 1. rectangle example: stretched_rectangle_can_hold_original_fixed 2. firecracker: requirement_2642 3. vecdeque-cve: minimal_example_with_cve_fixed For each configuration, I show numbers for a) verification time, b)...

I had this issue as well. I'm on macOS 12.4. Here's a snippet of the output error. ``` /Users/sanjitbh/.cargo/registry/src/github.com-1ecc6299db9ec823/ppv-lite86-0.2.16/src/generic.rs: In function 'guts::init_chacha': /Users/sanjitbh/.cargo/registry/src/github.com-1ecc6299db9ec823/ppv-lite86-0.2.16/src/generic.rs:800:30: error: error: conflicting function declarations 'rand_chacha::guts::init_chacha' old...

Also refactor code to allow insertion of multiple unit tests.

I'm working on this issue right now.

Note: it looks like simply commenting out that assertion doesn't work. While it passes the AST Generalization phase, the unparser then throws this error: ```python-traceback Traceback (most recent call last):...

Re: the original question, the Linux developers changed the kernel build system for single target builds. With their change, things like `make kernel/bpf/verifier.i` won't work by default. See [this discussion](https://lkml.org/lkml/2020/3/31/1043)...