Ted Kaminski

Programmatic tools are APIs like `wait4` maybe https://github.com/lu-zero/wait4-rs

> I would suggest that you make this option to print the metadata but without interrupting the verification flow. You can use --only-codegen if you want to interrupt the flow....

Thank you again for sitting down and debugging this with me! **Workaround:** `rustup default stable` and things should now work. The appears (I haven't finished debugging) to be a result...

That PR turned `assert` into `assert-assume`. Normally we'd think of it as pruning branches, and so I'd assume it'd improve performance if anything. But perhaps it's complicating the state with...

Possibly this should be written less as patterns and more as "writing specifications" A reasonable progression might start with: 1. No assertion in harness. ("What Kani checks for" so we...

Good point. I believe this was the `time` crate?

Hmm. This is possibly not yet completely solved. It did fix most of the issues I saw but I ran into this: ``` error: `std::fmt::Arguments::

Reproduction steps: ``` $ cargo new time-test Created binary (application) `time-test` package $ cd time-test/ $ cargo add time --features formatting [..SNIP..] $ cargo kani Compiling itoa v1.0.3 Compiling time...

This got hit again: https://github.com/time-rs/time/issues/521

This appears to generate irep that looks like this currently: ``` { "id": "code", "sub": [ { "id": "symbol", "namedSub": { "identifier": { "id": "_RNvMs2_NtCs2ybv9YpAGK_4core3fmtNtB5_9Arguments6new_v1Cs53OqACNvaXJ_11simple_test::1::var_24" }, "type": {...} } },...