search

izlatkin / HornLauncher

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

Assertion failed: (varNum >= 0) for count_by_nondet.c #28

Closed izlatkin closed 2 years ago

izlatkin commented 3 years ago

see errors in the logs below for c-file https://github.com/sosy-lab/sv-benchmarks/blob/99d37c5b4072891803b9e5c154127c912477f705/c/loop-new/count_by_nondet.c

count_by_nondet.smt2.txt

/Users/ilyazlatkin/PycharmProjects/aeval/build/tools/tg/tg --inv-mode 0 --no-term --keys 8877 count_by_nondet.smt2 Assertion failed: (varNum >= 0), function exploreTracesTG, file /Users/ilyazlatkin/PycharmProjects/aeval/include/deep/BndExpl.hpp, line 252. Abort trap: 6

it worked before last fix. Also it doesn't work without --inv-mode 0 --no-term

izlatkin commented 3 years ago

same issue for loop2-2, loop4, loop5 /Users/ilyazlatkin/PycharmProjects/aeval/build/tools/tg/tg --inv-mode 0 --no-term --keys 4914,3423 loop2-2.smt2 Assertion failed: (varNum >= 0), function exploreTracesTG, file /Users/ilyazlatkin/PycharmProjects/aeval/include/deep/BndExpl.hpp, line 252. Abort trap: 6

/Users/ilyazlatkin/PycharmProjects/aeval/build/tools/tg/tg --inv-mode 0 --no-term --keys 1453,3412 loop5.smt2 Assertion failed: (varNum >= 0), function exploreTracesTG, file /Users/ilyazlatkin/PycharmProjects/aeval/include/deep/BndExpl.hpp, line 252. Abort trap: 6 

/Users/ilyazlatkin/PycharmProjects/aeval/build/tools/tg/tg --inv-mode 0 --no-term --keys 1446,3402 loop4.smt2
Assertion failed: (varNum >= 0), function exploreTracesTG, file /Users/ilyazlatkin/PycharmProjects/aeval/include/deep/BndExpl.hpp, line 252.
Abort trap: 6
izlatkin commented 3 years ago 
/Users/ilyazlatkin/PycharmProjects/aeval/build/tools/tg/tg --inv-mode 0 --no-term --keys 5253,5286 simple_array_index_value_4.smt2
Assertion failed: (varNum >= 0), function exploreTracesTG, file /Users/ilyazlatkin/PycharmProjects/aeval/include/deep/BndExpl.hpp, line 252.
Abort trap: 6
grigoryfedyukovich commented 3 years ago

Not reproducible.

izlatkin commented 2 years ago

loop2-2, loop4, loop5 - not supported

izlatkin commented 2 years ago

fixed image