Support benchmark sets with files with equal names

[PhilippWendler]

Currently, each input file in a benchmark set needs to have a unique name, it is not sufficient to have equally-named files in different directories. The reason is that the file name is used for the log-file name. BenchExec should support having files dir1/file.c and dir2/file.c in a single benchmark.
This can be achieved by putting the log files into ...logfiles/dir1/file.c.log and ...logfiles/dir2/file.c.log instead of ...logfiles/file.c.log.

[joe-hauns]

Hi!
I know this is a very old post, but I am having the very same issue currently. I think this is not a took uncomon problem tbh.
I'm running benchmarks of the SMT-LIB dataset, where there is a couple of clashes, e.g.

• $SMTLIB/AUFLIRA/misc/list4.smt2
• $SMTLIB/UFLIA/misc/list4.smt2
  Benchexec in this case generates a *.logfiles.zip that contains the file <solver>.list4.smt2.log twice, which is very unpractical.
  As this is a benchmark set from an external source, I can't start renaming all the files.

Sooo I wanted to ask whether there is some workaround benchexec provides. Like some sort of naming logfiles by their full path, or giving ids to files, etc.

[PhilippWendler]

Yes, we are aware that this is problematic, but unfortunately we have not yet found a good solution, and it would be backwards incompatible so it needs good planning. It is unlikely that there is a quick fix.

As a workaround, one can split the benchmark set over several BenchExec executions, this is possible in two variants:

• Either use several <tasks> tags like this (this makes sense anyway):

  <tasks name="AUFLIRA">
    <include>AUFLIRA/*/*.smt2</include>
  </tasks>
  <tasks name="UFLIA">
    <include>UFLIA/*/*.smt2</include>
  </tasks>

  Then use benchexec -t AUFLIRA ..., benchexec -t UFLIA ... etc.
• Or put each of the tasks tags into its own <rundefinition>:

  <rundefinition name="AUFLIRA">
    <tasks><include>AUFLIRA/*/*.smt2</include></tasks>
  </rundefinition>
  <rundefinition name="UFLIA">
    <tasks><include>UFLIA/*/*.smt2</include></tasks>
  </rundefinition>

  Then you can simply start BenchExec as usual because the name of the rundefinition will be added to the log-file name.

In both cases, you will get more than on XML file with the results. In order to get proper tables, use a table definition with a <union> tag, which allows you to create a single result column from several XML files.

Does this help you?

[joe-hauns]

Using the rundefinition is definitely a good workaround! Thanks!