I tried running the run_exp_gpt4.sh script in the code2inv/ directory with the following arguments:

./run_exp_gpt4.sh ./benchmarks/code2inv/c/1

and I got the following exception:

Traceback (most recent call last):
  File "/mnt/c/Users/user/repos/Lemur-program-verification/code2inv/./src/run.py", line 41, in <module>
    v = Verifier(task, VERIFIERS, args)
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/mnt/c/Users/user/repos/Lemur-program-verification/code2inv/src/verifier.py", line 38, in __init__
    self.program = Program(r.lines_to_verify, r.replacement)
                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/mnt/c/Users/user/repos/Lemur-program-verification/code2inv/src/program.py", line 61, in __init__
    if line.strip().split()[0] in ["for", "do", "while"]:
       ~~~~~~~~~~~~~~~~~~~~^^^
IndexError: list index out of range

Before running the run_exp_gpt4.sh script, I installed the packages in requirements.txt and ran the ./build.sh script.
I tried running the tool with python 3.11 and python 3.8

Is there any additional setup I need to complete for the tool before running it? Or pass any other CLI arguments?

Hi,

Fantastic work! I have a small question regarding the selection of 47 benchmarks from SV-COMP: What is the specific implementation of the sampling? Or is there any available code that we can reimplement the sampling? Thank you so much!

I'm trying to reproduce the results.

When I run the command ./run_exp_gpt3.sh ./benchmarks/code2inv/c/117, I got the following error:

This looks like the postcondition information is missing during the inference.

I've followed your README.md to download the required package and installed the required tools with ./build.sh.

I'm looking forward to your favourable reply.