Segmentation Fault Encountered While Generating a Proof

[RaoulSchaffranek]

NOTICE: I moved this issue here from the https://github.com/runtimeverification/hs-backend-booster repository.

I'm facing a segmentation fault issue when attempting to generate a proof using the kevm foundry-prove command in our Symbolic Solidity Debugger project. Although this is not directly related to the ongoing Blockswap project, it's crucial for the Symbolic Solidity Debugger. However, I want to emphasize that this issue is not of high priority.

Reproduction Steps:

The following command triggers the issue. This issue occurs irrespective of the flags --no-simplify-init and --use-booster.

> git clone https://github.com/runtimeverification/_audits_bswap-eng_gateway-kernel
> cd _audits_bswap-eng_gateway-kernel
> export FOUNDRY_PROFILE=k
> kevm foundry-kompile --with-llvm-library
> kevm foundry-prove --max-depth 10000 --max-iterations 10000 --bmc-depth 3 --workers 1 --verbose --break-every-step --test DepositTest.testDepositRevertsIffNotInDomain
...
...
INFO 2023-09-13 13:21:08,236 pyk.ktool.kprint - Invoking kast_to_kore
INFO 2023-09-13 13:21:08,305 pyk.kore.rpc - Sending request to localhost:34175: 2 - simplify
INFO 2023-09-13 13:24:12,544 pyk.kore.rpc - Received response from localhost:34175: 2 - simplify
/nix/store/bylyxgwa7g05919jc01wk9riidv0pgg4-kevm-dirty/bin/.kevm-wrapped: line 9: 23241 Segmentation fault      /nix/store/1wzsgx4ir4z2iyn58gwghzf48gdjrjrp-python3.10-kevm-pyk-1.0.289/bin/kontrol "$@"

• I'm not entirely sure whether this issue resides in the backend or elsewhere, but I'm running out of troubleshooting ideas.
• Could someone from your team please look into this when convenient?

The full bug report can be found here: https://github.com/runtimeverification/_audits_bswap-eng_gateway-kernel/issues/1