Lucas C. Cordeiro

@rafaelsamenezes: did you have a chance to run this PR over the sv-comp benchmarks?

These results are from the `master` branch using ESBMC incremental (timelimit="5 min" memlimit="6 GB"): ``` Statistics: 15455 Files correct: 6728 correct true: 3118 correct false: 3610 incorrect: 243 incorrect true:...

Before this PR: ``` Statistics: 1082 Files correct: 967 correct true: 182 correct false: 785 incorrect: 21 incorrect true: 14 incorrect false: 7 unknown: 94 Score: 589 (max: 1344) ```...

@fbrausse: do we have a PR to fix this issue? :-)

This PR: ``` Statistics: 15648 Files correct: 8435 correct true: 5129 correct false: 3306 incorrect: 53 incorrect true: 24 incorrect false: 29 unknown: 7160 Score: 12332 (max: 25567) ``` Master:...

> If it was guarded by a condition saying "object is still alive", I believe this would fix the issue. I agree.

Hi @fbrausse, What do you think if we produce the equation at the symex level? I believe our SMT backend should only convert the equations in SSA to SMT. This...

> I wonder why we don't just refer to the C-models when they're available, e.g., for memmove, strtok and friends. +1

@kunjsong01: can I ask you you for the status of this PR?

@MatildeMark: there are two files in conflict: