Mikhail R. Gadelha

Yeah, the problem is how we call esbmc from the esbmc-wrapper.py script. Today, we use the following function: def run(cmd_line): print "Verifying with ESBMC" print "Command: " + cmd_line the_args...

Doesn't jenkins get the script from the repo? If so, we just need to change the script on master.

Not sure why the argc and argv are not initialized there, they are supposed to always be initialized in https://github.com/esbmc/esbmc/blob/master/src/clang-c-frontend/clang_c_main.cpp#L125

> Is there a way to make static builds of camada and release them? This would simplify a lot of the build process of ESBMC. Do you mean a static...

> > > I mean remove the dependencies of external solvers from ESBMC and only use > camada. If we don't use any specific function from a solver it should...

> > - 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...

Yeah, this has been highly debated in the past. We can open a PR fixing the benchmarks, i.e., changing the test definition to use the original c files instead of...

Can you replace the header definitions with includes and create a new .c file? Em qua., 16 de fev. de 2022 às 10:08, Franz Brauße ***@***.***> escreveu: > I've submitted...

Could you provide the list of properties being checked in each case?

That's weird, your log states that there are 10 properties being checked in the first case and none in the second. Can you provide the 41 properties from the first...