search

izlatkin / HornLauncher

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

inv-mode 2 vs inv-mode 0 #41

Open izlatkin opened 2 years ago

izlatkin commented 2 years ago

Below is the list of benchmarks that have lower coverage for inv-mode 2 then inv-mode 0:

Benchs:                              degradation in coverage:
deep-nested.c                   -5,55556%
sum_array-1.c                    -10%
trex03-2.c                          -16%

TG doesn't generate any tests for inv-mode 2: ./loop-invgen/apache-get-tag.i.p+nlh-reducer.c execution time (103.61) < timeout (900) ./loop-invgen/apache-get-tag.i.p+sep-reducer.c execution time == timeout (900) ./loop-invgen/heapsort.c execution time (599) < timeout (900)

results location:

scp fmfsu@grigory1.cs.fsu.edu:~/results/inv_mode_0_no_term.zip .
scp fmfsu@grigory1.cs.fsu.edu:~/results/inv_mode_2_no_term.zip .
grigoryfedyukovich commented 2 years ago

Fixed for sum_array-1.c