Lucas C. Cordeiro

@fbrausse: Can I ask you for the status of this PR?

@rafaelsamenezes: could you please answer @mikhailramalho's question?

@rafaelsamenezes: I have just updated the stats file at https://github.com/esbmc/esbmc/blob/master/scripts/competitions/svcomp/stats-300s.txt. Next time, before merging the PR, can I ask you to update this file?

> What do you think? It looks good to me.

It is going to be a bit tricky to solve this issue. In this particular example posted by @rafaelsamenezes, the method `tuple_get_rec` is called with the following: ``` (declare-fun |smt_conv::c:reduce2.c@149@F@main@f?1!0&0#0..c.__opaque0|...

@rafaelsamenezes: How shall we proceed with this PR?

I have just started a run of this PR over the SV-COMP benchmarks: https://github.com/esbmc/esbmc/actions/runs/2487747413

This PR: ``` Statistics: 15648 Files correct: 8449 correct true: 5119 correct false: 3330 incorrect: 54 incorrect true: 25 incorrect false: 29 unknown: 7145 Score: 12304 (max: 25567) ``` Master:...

@fbrausse: Can I ask you whether you could add the diff here?

Hi @mikhailramalho, @fbrausse, @rafaelsamenezes: Can I ask you how we could proceed with this PR? This PR is quite relevant since we get rid of unnecessary guards in the final...