Felipe R. Monteiro

Thanks, @kunjsong01! That solved the issue. Why is this necessary for macOS in the first place? It'd be helpful to add this as a comment to the release/building notes (unless...

Hi @fbrausse! > We usually rely on Clang's default include paths. Could you run ESBMC with `--verbosity 7` (and w/o the -I parameter)? This should print the include search paths...

> Maybe we can find a way on macos to build against the system clang directly. Short of that, the macos-wrapper.sh should still work. Does it? @fbrausse @kunjsong01 wouldn't be...

Is there any discussion to include `__VERIFIER_base_pointer` in the competition rules? ESBMC is currently reporting wrong verification results in some cases of AWS C Common benchmarks due to the lack...

> Wasn't this issue solved by some recent pull request? @dbeyer PR #993 simply removed all the `__VERIFIER_base_pointer` calls, but I believe this issue will only be solved once we...

@karkhaz can we close this PR?

`__CPROVER_is_fresh` was only designed to be used inside function contracts. @zhassan-aws @zpzigi754 You can see documentation for `__CPROVER_is_fresh` [here](https://diffblue.github.io/cbmc/contracts-memory-predicates.html). I'm not sure what you are trying to achieve with `ffi_CPROVER_DYNAMIC_OBJECT`...

https://github.com/model-checking/kani/pull/3107 solves this issue.

@markrtuttle I guess this is not our plan anymore. Shall we close this issue?

Thanks for the report, @rod-chapman! These are generic CBMC errors, not specific to contracts. They do not affect your analysis. ``` symbol '__CPROVER_alloca_object' already has an initial value symbol '__CPROVER_new_object'...