Bruno Farias

I also think it's a good idea to manage this through lists within each test.desc file.

Great initiative. If the ownership of the pointers isn't truly shared among different components/threads, switching from shared_ptr to unique_ptr could be an option. Perhaps it's worth taking a look at...

I have submitted a first part of the fix in #1045.

@kunjsong01, After merging #1045 we are crashing due to the abort() on this [line](https://github.com/esbmc/esbmc/blob/dd2f6295017a8ffe0233b20b764f3a146eb438ba/src/util/language_file.cpp#L227) It is possible to reproduce with the following snippet: ```cpp struct Foo { virtual void bar();...

>Did you include the ESBMC's C++ operational models in the command? something like "-I /library" I was not using this parameter.

Running **CPA-witness2test** with: `../../CPAchecker-2.2.1-svn-44999-unix/scripts/cpa_witness2test.py -timelimit 90s -stats -spec ../../sv-benchmarks/c/properties/unreach-call.prp -32 -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness witness-fixed.graphml ../../sv-benchmarks/c/floats-cdfpl/newton_1_4.i` I had the following output: ```...

Hi @haru-02, I've just sent you a message on our Slack to discuss how we could organize the documentation and address your questions. Thanks.