izlatkin / HornLauncher

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

[TG] Invalid query argument, expected uinterpreted function name, but argument is interpreted #33

Open izlatkin opened 2 years ago

izlatkin commented 2 years ago

for sum03-1.c and sum03-2.c https://github.com/sosy-lab/sv-benchmarks/blob/99d37c5b4072891803b9e5c154127c912477f705/c/loops/sum03-1.c https://github.com/sosy-lab/sv-benchmarks/blob/99d37c5b4072891803b9e5c154127c912477f705/c/loops/sum03-2.c

TG returns following error " Invalid query argument, expected uinterpreted function name, but argument is interpreted" smt2 attached sum03-1.smt2.txt full log:

`[16:43:21:791868] docker exec unruffled_lederberg bash -c cd /app/sum03-1; ../smt_run.sh /app/sum03-1/sum03-1.c /app/sum03-1/sum03-1.smt2 [16:43:21:980922] docker exec unruffled_lederberg bash -c cd /app/sum03-1; ../smt_run.sh /app/sum03-1/sum03-1.c /app/sum03-1/sum03-1.smt2 0 b''

b'WARNING: main function not found so program is trivially safe. '

[16:43:

21:981216] /home/fmfsu/aeval/build/tools/tg/tg --phase-prop --inv-mode 0 --no-term --keys 21117,62168 sum03-1.smt2 [16:43:22:098143] /home/fmfsu/aeval/build/tools/tg/tg --phase-prop --inv-mode 0 --no-term --keys 21117,62168 sum03-1.smt2 -11 b'(error "line 3 column 12: Invalid query argument, expected uinterpreted function name, but argument is interpreted") '

b''

[16:43:22:098630] total time: 0.35450005531311035 seconds`