search

izlatkin / HornLauncher

scripts and reports for executions seahorn and test generation
0 stars 0 forks source link

SeaHorn bug for sv-benchmarks/c/loops/sum03-1.c #15

Closed izlatkin closed 2 years ago

izlatkin commented 3 years ago

Looks like encoding issue

/app/sum03-1 $ ../smt_run.sh /app/sum03-1/sum03-1.c /app/sum03-1/sum03-1.smt2 WARNING: main function not found so program is trivially safe.

but the main method exists

https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loops/sum03-1.c

izlatkin commented 3 years ago

https://github.com/seahorn/seahorn/issues/65

izlatkin commented 2 years ago

other tools can't handle this case, seems that the benchmark is broken