Ramla Ijaz

**Full Output:** ``` Run verification on /home/ramla/Desktop/prusti-test/src/main.rs... Preparing verification run #1. Killing 0 processes. Run command '/home/ramla/prusti-dev/target/release/cargo-prusti --message-format=json' Spawned PID: 6728 Output from '/home/ramla/prusti-dev/target/release/cargo-prusti --message-format=json' (6.5s): ┌──── Begin stdout ────┐...

``` [stderr] [2022-05-06T13:49:17Z INFO prusti_common::stopwatch::log_level] [prusti-server] Starting: attach thread to JVM [stderr] [2022-05-06T13:49:17Z INFO prusti_common::stopwatch::log_level] [prusti-server] Completed: attach thread to JVM (0.000 seconds) [2022-05-06T13:49:17Z INFO prusti_server::process_verification] Verification request hash: 177752624514423564...

Hi, thanks for the quick reply. With the solution, I'm still getting an unexpected error: **Prusti assistant output:** ``` Run verification on /home/ramla/Desktop/prusti-test/src/main.rs... Preparing verification run #10. Killing 0 processes....

sure, where could I send the crate?

[prusti-test.zip](https://github.com/viperproject/prusti-dev/files/8641577/prusti-test.zip)

ok, I see. I actually have that flag enabled because I wanted to use bitwise operations.

If I remove it then yes, I get the same error.

so, is it correct to assume that generic types will not work when we enable bitwise operations?

I ran another very simple test where I creates a Volatile struct just for u32, so generics are out of the picture. Again, this only seems to work without bitwise...

I suppose my question is what are the limitation for using prusti with bitwise operations, since the code I'm aiming to verify uses them a lot.