Lucas C. Cordeiro

You can use the option `--force-malloc-success` to ensure that malloc always succeeds.

You can use c-reduce to reduce the program so that we can find out the root cause of this issue: https://github.com/esbmc/esbmc/wiki/Reducing-C-Programs ```` #!/bin/bash esbmc race-1_1-join.c --incremental-bmc --context-bound 2 --no-pointer-check --no-bounds-check...

@fbrausse: Remarkable improvement!

@brcfarias: could you please give some directions to address this issue (lack of documentation for our python frontend)?

@intrigus-lgtm: Can I ask you for the status of this PR?

@rafaelsamenezes: could you please fix this issue?

The results look promising :-) Rafael's PR: ```` Statistics: 26459 Files correct: 14654 correct true: 8504 correct false: 6150 incorrect: 64 incorrect true: 35 incorrect false: 29 unknown: 11741 Score:...

A run with 300 seconds using geometric-k-step: https://github.com/esbmc/esbmc/actions/runs/5707324732

Rafael's PR for 300 seconds: GitHub actions: https://github.com/esbmc/esbmc/actions/runs/5707324732 ```` Statistics: 26459 Files correct: 15955 correct true: 9168 correct false: 6787 incorrect: 95 incorrect true: 50 incorrect false: 45 unknown: 10409...

@Anthonysdu will lead the development and evaluation of the geometric k-step. We must be able to define the growth rate via the command line (e.g., 1.1, 1.2,...., 2). @Anthonysdu will...