Lucas C. Cordeiro

Hi Franz, Did you check this PR’s code? According to Mikhail’s comments, this guard affects the memory clean up check. Or did I get this wrong? After running this PR...

Actually, @mikhailramalho didn't mention the memory clean up check here. I think he told me face-to-face. @mikhailramalho: could you please clarify the motivation of this PR?

Dear all, What is the current status of this PR? BTW, it would be great to progress with the memory clean-up check.

@fbrausse: can I ask you whether you could look at this issue? This is a low-priority issue.

Thanks, @fbrausse. I'll merge this PR https://github.com/esbmc/esbmc/pull/749 to progress further with the performance fix, which is crucial for our industrial collaborator.

@fbrausse: I have just merged https://github.com/esbmc/esbmc/pull/749. Could you please submit the PR to fix the performance degradation with Z3?

@rafaelsamenezes: could you check these newer versions of Boolector? We should keep our regression over the SV-COMP benchmarks. In the past, we had situations where the newer Boolector versions suffered...

@shmarovfedor: Can I ask you to take a look at this issue?

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

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