Kani produces no output on non-termination

[tedinski]

When running RMC on code with loops and without an --unwind bound, RMC will often not terminate.

But, it presently produces no output at all during this infinite loop, whereas CBMC produces continuous stream of logging data that helps indicate what's gone wrong.

I believe this is because at some point we're buffering stdout from cbmc and only printing it once it's finished. We should allow these log messages to stream to the terminal, so we can see them during a non-termination problem.

[adpaco-aws]

Note that this issue may also appear in examples without loops. Running with --unwind 0 will allow the example to terminate. The dashboard has had problems with this (see #482 and its fix #492) and I would expect some more.

We could also consider running --unwind 0 by default. Thoughts?

[tedinski]

That's an interesting idea. The current default was presumably for soundness, but now we have unwinding assertions, right?

[adpaco-aws]

Yes, unwinding assertions are on by default so in principle passing --unwind 0 (or higher) will assert if it is not enough.

[jaisnan]

We're planning on addressing this issue by -

1. Piping the output instead of writing it to a file within the rust code.
2. Add functionality to read from stream in the Python Post processing.