Lucas C. Cordeiro

@kunjsong01: ESBMC still crashes for this C++ program (issue created on Sep 9, 2016). Can I ask you please to check it?

Thanks for reducing this program. @XLiZHI and @fbrausse: Can I ask you whether you could check this issue?

Thanks, @fbrausse ;-) Your memory is much better than mine :-) Please remind me to discuss this issue later in our meeting.

That's great, @fbrausse. This example shows that they must improve the existing validators.

Unfortunately, we are limited by these tools unless we develop our own witness checker :-(

I think it is fshell, right, @mikhailramalho ?

@fbrausse: you can post this example in the mailing list to show how broken are these witness validators.

Let's try to simplify the validator's task. By feeding all the nodes and edges leading from the entry point to the property violation, we might enhance the chances of the...

@brcfarias: can you please check whether we're missing some node/edge in the witness file? You could also try with the option `--no-slice` instead of `--compact-trace`.

Excellent 👏🏻