Michael Tautschnig

It seems the main problem is indeed the bounds check performed by `split_at`, which in turn results in a number of further operations that are conditional on that. What we...

> This might be happening again: > > * https://github.com/aws/s2n-quic/actions/runs/8742616782/job/23991319945?pr=2184 > > * https://github.com/aws/s2n-quic/actions/runs/8742616782/job/23993046067?pr=2184#step:3:36574 This wouldn't be too surprising to me: in https://github.com/model-checking/kani/pull/3117#issuecomment-2036616715 I logged that we appeared to be...

The symptoms point to a use of arrays of non-fixed size. It's not really obvious to me from `SmallVec`'s documentation why we newly should end up with such, so I'll...

> That's a good point. I have removed the nondeterministic scheduling strategies. No only the `RoundRobin` strategy is included. (And there's a test for it.) But wouldn't the non-deterministic schedules...

Resolving with following rationale: 1. We understand that it is the assert-followed-by-assume that increased the runtime (https://github.com/model-checking/kani/commit/ab0f2add72b9fd49a8410b7de981702cc3e784d6), but we do still want to keep that change. 2. The increased runtime...

With diffblue/cbmc#7230 on top of diffblue/cbmc@70b7cf7baf735f I get "Verification Time: 3.781643s" when it takes 471.05692s using diffblue/cbmc@70b7cf7baf735f and Kani revision 057926b83c.

Memory consumption appears to be below 250 MB :-)