Unsoundness with context-insensitive analyses: sv-comp tests "list_search"

[SchiJoha]

If all analyses are context insensitive, the sv-comp testcases list-properties/list_search-1.i and list-properties/list_search-2.i fail with the svcomp24.json configuration. (Similar to issue #1298)

During execution the error: [Error][Analyzer][Unsound] Both branches dead is thrown. This comes from the fact, that any traversal through the list is detected to be infinite. Hence the whole remaining code is declared dead.

To set all analyses context insensitive I changed the mCP.ml file in line 83 from cont_inse := map' find_id @@ get_string_list "ana.ctx_insens"; to cont_inse := xs;.
After compiling and executing the sv-comp testcase, Goblint incorrectly reports valid memory cleanup. The SV-COMP result is true, but false is expected.
I used those commands to run the testcases:
list_search-1:

./goblint --conf conf/svcomp24.json --sets ana.specification "CHECK( init(main()), LTL(G valid-memcleanup) )" ../../sv-benchmarks/c/list-properties/list_search-1.i 

list_search-2:

./goblint --conf conf/svcomp24.json --sets ana.specification "CHECK( init(main()), LTL(G valid-memcleanup) )" ../../sv-benchmarks/c/list-properties/list_search-2.i 

If only one of the analyses base, mallocWrapper, var_eq, apron, memLeak is analyzed context sensitively (and the remaining context insensitively), both tests produce the correct result (so the SV-COMP result is unknown). An overview can be found in the following picture.

[jerhard]

@SchiJoha and I found after some debugging that this issue seems to be due to a erroneous join in in the relational DHetero where the result of some bot_env and top_env values results in some bot_env value.