Adrian Palacios

I don't object neither.

Removing the soundness label since this is not strictly a soundness issue. Adding this check would introduce many failures that aren't part of the user code, because offset operations often...

According to @tautschnig , this is due to https://github.com/diffblue/cbmc/pull/6902 but the intended behavior was to get the following message instead: ``` - Status: FAILURE - Description: "undefined function should be...

I cannot reproduce this in my laptop (running macOS 12.4). Maybe because you're running on Apple silicon?

Doesn't reproduce with a macOS 12 regression neither, see [this run](https://github.com/model-checking/kani/runs/7697385658?check_suite_focus=true). This error could be related to how we handle dependencies in Apple silicon, so I would like to loop...

Reminder: As a workaround, you can define the environment variable `KANI_REGRESSION_KEEP_GOING` when launching the regression script.

> The tests compile under Kani now, but they take a very long time. I stopped the first harness (`io_chain.rs`) after two hours. I saw you're using `[kani::unwind(32)]` for all...

Recent data (in #1400) has shown that SIMD intrinsics are among the top unsupported features. Some popular crates impacted by this unsupported feature are `rand` (random number generation) and `regex`...

Just heard about a project that would be interested in using an action like this. By default, it should run `cargo kani`. But we should also provide the option to...

Hi @ssoudan , thank you for opening the issue! You're right: The CBMC model for the sine function is an over-approximation that returns 0 if the argument is 0, and...