Lucas C. Cordeiro

why not? :-) Is there some particular commit that you removed?

> Is there a way to let SV-COMP run ESBMC on the .c files at least where a model of a library that does not define its own types is...

@fbrausse: Can I ask you whether you could submit a merge request for SV-COMP (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks) to fix the benchamrk?

I agree with @mikhailramalho. @fbrausse: could you please submit a merge request to SV-COMP and fix our regression?

@DestyNova: Can I ask you to try this version? https://drive.google.com/file/d/1y79T4YOpgp6X2jPjyjp0ol6PMusBOf-r/view?usp=sharing @rafaelsamenezes has fixed this issue (not ideally yet), which is available in this specific branch https://github.com/esbmc/esbmc/tree/ucode.

@DestyNova: This is the correct link: https://drive.google.com/file/d/1y79T4YOpgp6X2jPjyjp0ol6PMusBOf-r/view?usp=sharing

@rafaelsamenezes: Is this issue still valid?

``` char *strcpy(char *dst, const char *src) { __ESBMC_HIDE:; char *cp = dst; while((*cp++ = *src++)) ; return dst; } ``` Properties: ``` Claim 1: file syserr.c line 108 function...

Full verification result: ``` Malvinas:lixo lucasccordeiro$ esbmc vanderson.c --unwind 10 ESBMC version 6.4.0 64-bit x86_64 macos file vanderson.c: Parsing Converting Generating GOTO Program GOTO program creation time: 0.378s GOTO program...

I have run ``` (1) $ esbmc vanderson.c --unwind 10 --no-simplify --program-only > original-model.txt (2) $ esbmc vanderson.c --unwind 10 --no-simplify --program-only > simplified-model.txt ``` (1) ``` char *strcpy(char *dst,...