izlatkin / HornLauncher

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

[tg tool] non digit in array inp_3653[] = {1, __loc_var_7, -3653, 0}; #17

Closed izlatkin closed 3 years ago

izlatkin commented 3 years ago

For c. file https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loop-invariants/const.c const.smt2.txt testgen_3.h.txt

testgen_3 contains static const int inp_3653[] = {1, **__loc_var_7**, -3653, 0};

izlatkin commented 3 years ago

same problem https://github.com/sosy-lab/sv-benchmarks/blob/99d37c5b4072891803b9e5c154127c912477f705/c/loop-zilu/benchmark03_linear.c

benchmark03_linear.smt2.txt testgen.h.txt Main.c.txt

grigoryfedyukovich commented 3 years ago

Should be fixed in the new commit

izlatkin commented 3 years ago

image

passed