Tool VeriAbs 1.3.10 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-10 16:50:17 CET 2018-12-10 20:34:10 CET 2018-12-10 21:22:10 CET 2018-12-10 21:27:56 CET 2018-12-12 21:52:30 CET 2018-12-10 19:33:41 CET 2018-12-10 20:40:20 CET
Run set veriabs.sv-comp19_prop-reachsafety.ReachSafety-Loops cpa-seq-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Loops uautomizer-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Loops uautomizer-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Loops
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
loops/array_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.0 1.2 150 29 .086 0      false(unreach-call) 1 wit inspect 4.6  2.5  250 0   0      false(unreach-call) 1 --- inspect 7.3   4.5   310   .66 0      unknown 0 --- inspect 4.4  2.6  250 0     0      true -32 --- inspect .56   .56   20    .049  0      - --- inspect - --- inspect
loops/bubble_sort_false-unreach-call.i false(unreach-call) 1 wit inspect 480   460   2200 3800 1.1   0      true -32 wit inspect 8.4  4.5  270 0   0      false(unreach-call) 1 --- inspect 15     7.7   570   .66 0      unknown 0 --- inspect 7.1  3.8  280 0     0      error (2) 0 --- inspect .84   .84   21    .053  0      - --- inspect - --- inspect
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 9.1 3.6 270 73 .12  0      false(unreach-call) 1 wit inspect 4.6  2.5  250 0   0      false(unreach-call) 1 --- inspect 7.9   4.4   300   .66 .0041 false(unreach-call) 1 --- inspect 4.2  2.4  250 0     0      false(unreach-call) 1 --- inspect .57   .57   20    .045  0      - --- inspect - --- inspect
loops/eureka_01_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 44   26   680 440 .50  0      timeout 0 wit inspect 97    81    2000 0   0      out of memory 0 --- inspect 72     47     7000   .63 0      unknown 0 --- inspect 5.6  3.1  250 0     .0041 error (2) 0 --- inspect .63   .65   21    .037  0      - --- inspect - --- inspect
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 14   5.0 270 99 .32  .16   false(unreach-call) 1 wit inspect 5.1  2.8  260 0   .0041 false(unreach-call) 1 --- inspect 7.3   4.1   310   .62 0      false(unreach-call) 1 --- inspect 3.7  2.2  250 0     0      false(unreach-call) 1 --- inspect .59   .59   21    .049  0      - --- inspect - --- inspect
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 430   410   4200 4000 .43  .0082 timeout 0 wit inspect 96    80    2000 0   0      false(unreach-call) 1 --- inspect 20     11     480   .62 0      unknown 0 --- inspect 5.1  2.9  260 0     0      false(unreach-call) 1 --- inspect .65   .64   21    .061  0      - --- inspect - --- inspect
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 28   13   290 210 1.9   0      timeout 0 wit inspect 96    81    2000 0   0      false(unreach-call) 1 --- inspect 9.2   5.6   400   .66 0      unknown 0 --- inspect 4.2  2.4  260 0     0      true -32 --- inspect .64   .64   21    .061  .0041 - --- inspect - --- inspect
loops/linear_search_false-unreach-call.i false(unreach-call) 0 wit inspect 18   6.5 280 130 .39  0      error (invalid witness file) 0 --- inspect 2.7  1.5  200 0   0      out of memory 0 --- inspect 62     39     7000   .95 0      error (invalid witness file) 0 --- inspect 3.0  1.7  200 0     0      error (1) 0 --- inspect .52   .52   21    .0041 0      - --- inspect - --- inspect
loops/ludcmp_false-unreach-call.i false(unreach-call) 0 wit inspect 31   18   1500 320 .69  0      true -32 wit inspect 13    7.5  460 0   0      true -32 --- inspect 42     32     830   .75 0      unknown 0 --- inspect 12    7.0  490 0     0      error (2) 0 --- inspect 3.4    3.4    21    .037  0      - --- inspect - --- inspect
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 510   480   9100 3600 1.6   .0082 timeout 0 wit inspect 97    87    1900 0   0      out of memory 0 --- inspect 59     38     7000   1.7  0      unknown 0 --- inspect 5.8  3.2  280 0     0      error (2) 0 --- inspect .61   .61   21    .037  0      - --- inspect - --- inspect
loops/n.c24_false-unreach-call.i timeout 0 --- inspect 900   880   3000 10000 .72  0      error (invalid witness file) 0 --- inspect .65 .40 40 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0      error (invalid witness file) 0 --- inspect .96 .63 48 0     0      error (invalid witness file) 0 --- inspect .0060 .0078 .53 0      0      - --- inspect - --- inspect
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 13   4.7 260 100 .16  0      false(unreach-call) 1 wit inspect 4.0  2.2  250 0   0      false(unreach-call) 1 --- inspect 7.6   4.8   320   .62 0      false(unreach-call) 1 --- inspect 3.8  2.2  250 0     0      false(unreach-call) 1 --- inspect .57   .57   20    .049  0      - --- inspect - --- inspect
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 19   7.2 290 140 .36  13      false(unreach-call) 1 wit inspect 3.9  2.2  250 0   0      false(unreach-call) 1 --- inspect 8.8   4.9   310   .66 0      unknown 0 --- inspect 3.7  2.1  250 0     0      error (2) 0 --- inspect .61   .61   20    .061  0      - --- inspect - --- inspect
loops/s3_false-unreach-call.i false(unreach-call) 0 wit inspect 92   67   870 1000 .65  0      true -32 wit inspect 6.5  3.5  300 0   .066  error (7) 0 --- inspect 14     8.4   290   .75 0      unknown 0 --- inspect 5.3  2.9  280 0     0      error (2) 0 --- inspect .80   .79   22    .29   0      - --- inspect - --- inspect
loops/string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 32   11   300 230 2.7   0      false(unreach-call) 1 wit inspect 5.4  3.0  270 0   0      false(unreach-call) 1 --- inspect 24     14     450   .75 0      unknown 0 --- inspect 4.2  2.3  250 0     0      true -32 --- inspect .64   .64   21    .061  0      - --- inspect - --- inspect
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 16   5.9 290 140 .32  0      false(unreach-call) 1 wit inspect 4.2  2.4  260 0   .0041 false(unreach-call) 1 --- inspect 9.0   5.3   310   .66 0      false(unreach-call) 1 --- inspect 3.9  2.3  250 0     0      false(unreach-call) 1 --- inspect .62   .62   21    .053  0      - --- inspect - --- inspect
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 15   5.7 290 120 .32  0      false(unreach-call) 1 wit inspect 5.2  2.9  250 0   0      false(unreach-call) 1 --- inspect 8.2   4.7   310   .62 .0041 false(unreach-call) 1 --- inspect 4.1  2.4  250 0     0      true -32 --- inspect .59   .59   21    .053  0      - --- inspect - --- inspect
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 16   6.0 300 140 .31  0      false(unreach-call) 1 wit inspect 4.7  2.6  260 0   0      false(unreach-call) 1 --- inspect 11     6.4   570   .66 0      false(unreach-call) 1 --- inspect 3.8  2.2  250 0     0      true -32 --- inspect .59   .59   21    .053  0      - --- inspect - --- inspect
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 15   5.7 310 130 .31  14      false(unreach-call) 1 wit inspect 4.6  2.5  260 0   0      out of memory 0 --- inspect 87     57     7000   .70 .0041 false(unreach-call) 1 --- inspect 4.6  2.6  250 0     .35   false(unreach-call) 1 --- inspect .59   .59   21    .045  0      - --- inspect - --- inspect
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 16   5.8 300 110 .31  0      false(unreach-call) 1 wit inspect 4.0  2.2  250 0   0      false(unreach-call) 1 --- inspect 6.7   4.3   300   .66 0      false(unreach-call) 1 --- inspect 3.6  2.1  250 0     0      false(unreach-call) 1 --- inspect .59   .59   21    .049  0      - --- inspect - --- inspect
loops/sum_array_false-unreach-call.i false(unreach-call) 1 wit inspect 3.0 1.3 140 27 .094 0      false(unreach-call) 1 wit inspect 4.9  2.7  260 0   0      true -32 --- inspect 6.8   3.9   320   .66 0      unknown 0 --- inspect 3.7  2.1  250 0     0      true -32 --- inspect .57   .57   20    .057  0      - --- inspect - --- inspect
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 8.7 3.5 270 78 .11  .0041 false(unreach-call) 1 wit inspect 4.1  2.3  240 0   0      false(unreach-call) 1 --- inspect 7.9   4.4   300   .66 0      false(unreach-call) 1 --- inspect 3.7  2.1  250 0     0      false(unreach-call) 1 --- inspect .57   .57   20    .045  0      - --- inspect - --- inspect
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 14   5.1 280 120 .32  13      false(unreach-call) 1 wit inspect 3.9  2.2  250 0   0      false(unreach-call) 1 --- inspect 7.0   4.0   310   .66 0      false(unreach-call) 1 --- inspect 3.4  2.0  240 0     0      false(unreach-call) 1 --- inspect .61   .60   20    .049  0      - --- inspect - --- inspect
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 9.0 3.5 270 74 .11  .0041 false(unreach-call) 1 wit inspect 4.4  2.5  250 0   0      false(unreach-call) 1 --- inspect 7.9   4.4   310   .66 0      false(unreach-call) 1 --- inspect 3.7  2.2  250 0     0      false(unreach-call) 1 --- inspect .57   .57   20    .045  0      - --- inspect - --- inspect
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 14   5.3 270 110 .32  .0041 false(unreach-call) 1 wit inspect 4.5  2.4  250 0   0      false(unreach-call) 1 --- inspect 7.0   4.4   310   .66 0      unknown 0 --- inspect 3.7  2.2  250 0     0      true -32 --- inspect .59   .59   20    .053  0      - --- inspect - --- inspect
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 13   4.8 270 96 .31  .0041 false(unreach-call) 1 wit inspect 3.6  2.0  250 0   0      false(unreach-call) 1 --- inspect 6.8   3.9   310   .66 0      unknown 0 --- inspect 4.4  2.5  250 0     0      true -32 --- inspect .60   .59   20    .053  0      - --- inspect - --- inspect
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 14   5.1 270 120 .32  0      false(unreach-call) 1 wit inspect 3.9  2.1  260 0   0      false(unreach-call) 1 --- inspect 6.9   4.4   300   .66 0      unknown 0 --- inspect 3.6  2.1  250 0     0      false(unreach-call) 1 --- inspect .57   .57   20    .049  0      - --- inspect - --- inspect
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 17   5.9 300 120 .36  0      false(unreach-call) 1 wit inspect 3.7  2.1  250 0   0      false(unreach-call) 1 --- inspect 12     6.6   340   .62 0      false(unreach-call) 1 --- inspect 3.4  2.0  250 0     0      false(unreach-call) 1 --- inspect .56   .56   20    .049  0      - --- inspect - --- inspect
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 29   17   280 270 .60  .0041 false(unreach-call) 1 wit inspect 4.3  2.4  250 0   0      false(unreach-call) 1 --- inspect 20     11     480   .66 0      unknown 0 --- inspect 4.4  2.5  250 0     0      true -32 --- inspect .58   .58   21    .057  0      - --- inspect - --- inspect
loops/vogal_false-unreach-call.i false(unreach-call) 1 wit inspect 62   46   370 680 .38  .37   false(unreach-call) 1 wit inspect 6.7  4.3  290 0   .0041 timeout 0 --- inspect 97     87     590   1.7  0      false(unreach-call) 1 --- inspect 4.6  2.6  260 0     0      false(unreach-call) 1 --- inspect .66   .67   21    .061  0      - --- inspect - --- inspect
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 14   4.9 300 100 .31  .012  false(unreach-call) 1 wit inspect 3.7  2.1  250 0   0      false(unreach-call) 1 --- inspect 6.6   3.8   310   .66 0      false(unreach-call) 1 --- inspect 3.6  2.1  240 0     0      false(unreach-call) 1 --- inspect .62   .62   20    .045  0      - --- inspect - --- inspect
loops/array_true-unreach-call_true-termination.i true 2 wit inspect 3.1 1.4 150 27 .086 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  290 0   0      true 2 --- inspect 12     6.9   380   .66 0     
loops/bubble_sort_true-unreach-call_true-termination.i true 2 wit inspect 17   7.7 430 140 170     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.1  2.8  270 0   0      true 2 --- inspect 8.7   5.1   310   .66 0     
loops/count_up_down_true-unreach-call_true-termination.i true 2 wit inspect 15   7.0 450 120 150     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 440    430    7000 0   0      true 2 --- inspect 37     32     470   .62 0     
loops/eureka_01_true-unreach-call.i true 2 wit inspect 140   83   1100 1500 140     6.4    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 82    67    1900 0   0      timeout 0 --- inspect 960     920     4900   .64 0     
loops/eureka_05_true-unreach-call_true-termination.i true 1 wit inspect 110   69   930 1000 140     6.5    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3800 0   0      timeout 0 --- inspect 960     920     880   1.5  0     
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 13   6.4 460 110 140     .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  280 0   0      true 2 --- inspect 7.4   4.6   310   .66 0     
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 13   6.4 460 110 150     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  280 0   0      true 2 --- inspect 8.4   4.7   310   .66 0     
loops/insertion_sort_true-unreach-call_true-termination.i unknown 0 --- inspect 790   760   6300 7400 11     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0      error (2) 0 --- inspect .024 .026 5.7 0    0     
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect 100   65   770 940 150     6.1    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    11    500 0   0      true 2 --- inspect 270     250     860   .62 0     
loops/linear_sea.ch_true-unreach-call.i true 1 wit inspect 130   68   1300 1400 140     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 630    610    7000 0   0      timeout 0 --- inspect 960     920     710   .65 0     
loops/lu.cmp_true-unreach-call.i true 2 wit inspect 64   39   3600 700 150     7.1    - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 110    99    7000 0   0      true 2 --- inspect 45     29     870   .62 0     
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect 28   11   510 230 140     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.6  3.1  290 0   0      error (7) 0 --- inspect 10     6.1   280   .74 0     
loops/n.c11_true-unreach-call_false-termination.i true 2 wit inspect 27   11   510 200 150     .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.0  2.7  290 0   0      true 2 --- inspect 12     7.0   350   .62 0     
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect 31   14   530 270 140     40      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  280 0   0      true 2 --- inspect 7.7   4.3   310   .66 0     
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect 32   15   510 270 150     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  280 0   0      true 2 --- inspect 8.0   4.5   310   .66 0     
loops/string_true-unreach-call_true-termination.i true 2 wit inspect 18   6.2 200 130 2.5   0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.7  3.7  290 0   0      true 2 --- inspect 12     6.7   400   .66 0     
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect 16   7.5 530 130 170     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 470    460    7000 0   0      true 2 --- inspect 11     6.6   340   .62 0     
loops/sum03_true-unreach-call_false-termination.i true 2 wit inspect 13   6.7 440 120 140     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.8  3.2  280 0   0      true 2 --- inspect 8.6   4.9   310   .62 0     
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect 17   7.8 580 140 150     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    450 0   0      true 2 --- inspect 10     6.2   340   .62 0     
loops/sum_array_true-unreach-call.i true 1 wit inspect 23   12   200 200 2.5   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3100 0   0      timeout 0 --- inspect 960     920     2500   .69 15     
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect 14   6.9 470 120 150     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.9  2.8  290 0   0      true 2 --- inspect 9.1   5.1   310   .66 0     
loops/terminator_03_true-unreach-call_true-termination.i true 2 wit inspect 13   6.7 450 120 150     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.7  280 0   0      true 2 --- inspect 7.8   4.3   310   .66 0     
loops/trex01_true-unreach-call_true-termination.i true 2 wit inspect 13   6.6 440 100 150     .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 41    27    1100 0   0      true 2 --- inspect 7.9   4.5   310   .66 0     
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect 13   6.6 450 110 140     .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.2  2.9  280 0   0      true 2 --- inspect 8.1   4.9   310   .66 0     
loops/trex03_true-unreach-call_true-termination.i true 2 wit inspect 14   7.0 470 120 140     .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.7  2.6  280 0   0      true 2 --- inspect 7.8   4.4   310   .66 0     
loops/trex04_true-unreach-call_false-termination.i true 2 wit inspect 13   6.6 460 110 140     .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.6  290 0   0      true 2 --- inspect 7.8   4.4   310   .66 0     
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect 18   8.0 470 170 150     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  270 0   0      true 2 --- inspect 8.4   5.2   310   .66 0     
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect 47   31   480 480 150     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 8.6  4.5  400 0   0      true 2 --- inspect 9.1   5.5   320   .66 0     
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect 18   7.8 470 150 140     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  280 0   0      true 2 --- inspect 9.0   5.0   320   .66 .0041
loops/vogal_true-unreach-call.i true 2 wit inspect 130   58   950 1200 140     6.1    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 69    57    1100 0   0      true 2 --- inspect 560     510     1100   .62 0     
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 13   6.4 460 94 140     .28   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.6  3.1  280 0   0      true 2 --- inspect 8.1   4.5   320   .66 .0041
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 12   6.3 420 110 140     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.5  3.1  270 0   0      true 2 --- inspect 7.4   4.6   310   .62 0     
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 2 wit inspect 12   6.4 440 110 150     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  270 0   0      true 2 --- inspect 8.6   4.8   320   .66 0     
loop-acceleration/array_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 240   220   1900 3400 .16  0      timeout 0 wit inspect 97    88    850 0   0      true -32 --- inspect 8.3   4.7   310   .56 0      false(unreach-call) 1 --- inspect 3.5  2.0  250 0     0      false(unreach-call) 1 --- inspect .56   .55   20    .045  0      - --- inspect - --- inspect
loop-acceleration/array_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 4.6 1.7 190 35 .090 0      timeout 0 --- inspect 97    87    1300 0   0      true -32 --- inspect 8.1   5.0   320   .62 .0041 false(unreach-call) 1 --- inspect 3.6  2.1  250 0     0      false(unreach-call) 1 --- inspect .56   .56   20    .045  .0041 - --- inspect - --- inspect
loop-acceleration/array_false-unreach-call3_true-termination.i false(unreach-call) 0 wit inspect 470   440   2000 6400 32     0      true -32 wit inspect 68    38    3100 0   0      out of memory 0 --- inspect 87     56     7000   .63 0      unknown 0 --- inspect 51    29    3100 0     0      timeout 0 --- inspect 96      96      170    .016  0      - --- inspect - --- inspect
loop-acceleration/const_false-unreach-call1.i false(unreach-call) 1 wit inspect 220   200   2500 3100 .11  0      false(unreach-call) 1 wit inspect 24    13    740 0   0      true -32 --- inspect 9.9   5.7   330   .66 0      false(unreach-call) 1 --- inspect 3.8  2.2  250 0     0      false(unreach-call) 1 --- inspect .55   .55   20    .045  0      - --- inspect - --- inspect
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect 48   33   590 580 .32  0      false(unreach-call) 1 wit inspect 5.3  2.9  280 0   0      out of memory 0 --- inspect 82     51     7000   .63 0      false(unreach-call) 1 --- inspect 4.4  2.5  260 0     0      false(unreach-call) 1 --- inspect .62   .65   22    .045  0      - --- inspect - --- inspect
loop-acceleration/functions_false-unreach-call1_true-termination.i unknown 0 --- inspect 41   26   280 390 14     0      error (invalid witness file) 0 --- inspect .58 .36 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0      error (invalid witness file) 0 --- inspect 1.2  .75 47 0     0      error (invalid witness file) 0 --- inspect .0035 .0046 .52 0      0      - --- inspect - --- inspect
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 9.0 3.6 270 76 .11  .0041 false(unreach-call) 1 wit inspect 4.5  2.5  250 0   0      false(unreach-call) 1 --- inspect 7.0   3.9   300   .66 0      false(unreach-call) 1 --- inspect 4.4  2.5  250 0     0      false(unreach-call) 1 --- inspect .58   .57   20    .045  0      - --- inspect - --- inspect
loop-acceleration/nested_false-unreach-call1.i false(unreach-call) 1 wit inspect 220   200   3100 2900 .11  13      timeout 0 wit inspect 98    84    1800 0   0      true -32 --- inspect 10     6.1   310   .66 0      false(unreach-call) 1 --- inspect 7.2  5.4  250 0     0      false(unreach-call) 1 --- inspect 3.4    3.4    20    .045  .0041 - --- inspect - --- inspect
loop-acceleration/phases_false-unreach-call1.i false(unreach-call) 1 wit inspect 370   360   9600 5000 120     0      timeout 0 wit inspect 98    83    1900 0   0      true -32 --- inspect 8.9   5.3   310   .66 0      false(unreach-call) 1 --- inspect 3.7  2.3  240 0     0      false(unreach-call) 1 --- inspect .84   .84   20    .045  0      - --- inspect - --- inspect
loop-acceleration/phases_false-unreach-call2_false-termination.i false(unreach-call) 1 wit inspect 8.7 3.4 270 80 .11  0      false(unreach-call) 1 wit inspect 3.6  2.0  250 0   0      false(unreach-call) 1 --- inspect 7.5   4.6   310   .66 0      false(unreach-call) 1 --- inspect 4.1  2.3  250 0     0      false(unreach-call) 1 --- inspect .58   .57   20    .045  0      - --- inspect - --- inspect
loop-acceleration/simple_false-unreach-call1.i false(unreach-call) 1 wit inspect 220   200   2100 2500 .11  0      timeout 0 wit inspect 97    86    1700 0   0      true -32 --- inspect 9.0   5.6   320   .62 0      false(unreach-call) 1 --- inspect 3.8  2.3  250 0     0      false(unreach-call) 1 --- inspect .79   .79   20    .045  .0041 - --- inspect - --- inspect
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 9.3 3.6 310 76 .11  .33   false(unreach-call) 1 wit inspect 3.7  2.0  250 0   0      false(unreach-call) 1 --- inspect 8.5   5.0   310   .66 0      true -32 --- inspect 3.6  2.1  250 0     0      false(unreach-call) 1 --- inspect .57   .58   20    .049  0      - --- inspect - --- inspect
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect 13   5.0 270 98 .31  0      false(unreach-call) 1 wit inspect 3.7  2.0  250 0   0      false(unreach-call) 1 --- inspect 6.8   3.8   300   .62 0      false(unreach-call) 1 --- inspect 3.8  2.2  250 0     0      false(unreach-call) 1 --- inspect .57   .57   20    .049  0      - --- inspect - --- inspect
loop-acceleration/simple_false-unreach-call4.i false(unreach-call) 1 wit inspect 220   200   2100 3200 .12  .14   timeout 0 wit inspect 98    85    1700 0   .0041 true -32 --- inspect 10     6.2   320   .66 0      false(unreach-call) 1 --- inspect 3.7  2.2  240 0     0      false(unreach-call) 1 --- inspect .80   .80   20    .045  0      - --- inspect - --- inspect
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 14   5.1 280 110 .31  0      false(unreach-call) 1 wit inspect 4.6  2.5  250 0   0      false(unreach-call) 1 --- inspect 11     6.2   380   .62 0      false(unreach-call) 1 --- inspect 3.8  2.2  250 0     0      false(unreach-call) 1 --- inspect .57   .57   21    .045  0      - --- inspect - --- inspect
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 9.1 3.6 280 77 .11  0      false(unreach-call) 1 wit inspect 4.2  2.3  250 0   0      false(unreach-call) 1 --- inspect 11     6.7   380   .66 0      false(unreach-call) 1 --- inspect 3.7  2.1  250 0     0      false(unreach-call) 1 --- inspect .60   .59   21    .045  0      - --- inspect - --- inspect
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 wit inspect 38   24   1200 410 150     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  280 0   0      true 2 --- inspect 12     8.2   350   .66 .0041
loop-acceleration/array_true-unreach-call2_true-termination.i true 1 wit inspect 4.2 1.6 190 30 .090 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    900    5000 0   0      timeout 0 --- inspect 960     930     660   .62 0     
loop-acceleration/array_true-unreach-call3_true-termination.i true 2 wit inspect 15   4.9 200 100 .74  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.1  2.8  280 0   .0041 true 2 --- inspect 11     6.3   380   .66 0     
loop-acceleration/array_true-unreach-call4_true-termination.i true 1 wit inspect 15   4.9 200 100 .87  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    6200 0   0      timeout 0 --- inspect 960     920     750   1.6  0     
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect 14   7.0 460 130 150     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.7  3.1  280 0   0      true 2 --- inspect 7.8   4.9   310   .66 .0041
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect 74   43   800 720 140     6.1    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 25    17    660 0   .0041 timeout 0 --- inspect 960     940     560   .65 0     
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect 51   31   850 510 150     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.4  3.5  300 0   0      true 2 --- inspect 490     470     640   .62 0     
loop-acceleration/functions_true-unreach-call1_true-termination.i true 2 wit inspect 120   65   1300 1400 140     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.8  3.2  280 0   0      true 2 --- inspect 16     9.8   470   .66 0     
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect 13   6.7 430 100 140     .0082 - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 440    430    7000 0   0      true 2 --- inspect 9.0   5.4   310   .62 0     
loop-acceleration/nested_true-unreach-call1.i true 2 wit inspect 43   34   550 450 140     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.9  4.4  300 0   .012  true 2 --- inspect 30     24     470   .62 0     
loop-acceleration/overflow_true-unreach-call1.i true 2 wit inspect 120   65   1300 1100 150     6.6    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.0  3.3  280 0   0      true 2 --- inspect 8.8   5.0   310   .66 .0041
loop-acceleration/phases_true-unreach-call1.i true 1 wit inspect 270   220   9800 3500 270     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    6100 0   0      false(unreach-call) -16 --- inspect 7.5   4.3   300   .66 0     
loop-acceleration/phases_true-unreach-call2_false-termination.i true 2 wit inspect 14   6.9 450 110 140     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    460 0   0      true 2 --- inspect 13     9.5   330   .66 0     
loop-acceleration/simple_true-unreach-call1.i true 2 wit inspect 120   65   1300 1200 150     .59   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  280 0   0      true 2 --- inspect 9.4   5.6   310   .66 0     
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect 12   6.2 460 110 150     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.3  2.9  280 0   0      true 2 --- inspect 7.4   4.7   310   .66 0     
loop-acceleration/simple_true-unreach-call3_true-termination.i true 2 wit inspect 120   66   1200 1300 140     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.7  280 0   0      true 2 --- inspect 10     6.7   330   .66 0     
loop-acceleration/simple_true-unreach-call4.i true 2 wit inspect 15   6.6 470 120 150     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  280 0   0      true 2 --- inspect 11     5.9   320   .66 0     
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect 29   16   600 240 140     .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.7  5.3  390 0   0      true 2 --- inspect 27     21     450   .62 0     
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect 14   6.7 470 130 140     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.7  3.1  280 0   0      true 2 --- inspect 12     6.9   390   .66 .0041
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i false(unreach-call) 1 wit inspect 300   290   6600 3600 .41  0      false(unreach-call) 1 wit inspect 4.3  2.4  260 0   0      false(unreach-call) 1 --- inspect 7.8   4.4   300   .66 0      true -32 --- inspect 3.5  2.0  250 0     0      true -32 --- inspect .58   .58   20    .049  0      - --- inspect - --- inspect
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i true 1 wit inspect 16   5.3 190 110 1.2   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4200 0   0      timeout 0 --- inspect 960     940     700   .65 0     
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i true 1 wit inspect 16   5.2 200 120 .92  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    900 0   0      timeout 0 --- inspect 960     940     930   .63 0     
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i true 1 wit inspect 16   5.2 190 100 1.2   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    6100 0   0      timeout 0 --- inspect 960     930     740   .65 .0041
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i true 2 wit inspect 17   6.6 200 140 3.8   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1800 0   0      true 2 --- inspect 22     16     400   .66 0     
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i true 2 wit inspect 14   6.7 450 110 150     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.8  3.2  280 0   0      true 2 --- inspect 7.8   4.9   320   .66 .041 
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i true 2 wit inspect 14   6.7 440 120 190     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.2  2.9  280 0   0      true 2 --- inspect 8.8   5.4   310   .66 0     
loop-crafted/simple_array_index_value_true-unreach-call4.i.v+lhb-reducer.c out of memory 0 --- inspect 49   42   15000 610 .23  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0      error (2) 0 --- inspect .020 .022 5.6 0    0     
loop-crafted/simple_array_index_value_true-unreach-call4.i.v+nlh-reducer.c out of memory 0 --- inspect 49   42   15000 600 .25  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .42 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 14   5.0 270 100 .32  0      false(unreach-call) 1 wit inspect 3.8  2.1  250 0   0      false(unreach-call) 1 --- inspect 7.1   4.5   310   .66 0      false(unreach-call) 1 --- inspect 4.4  2.5  240 0     .0041 false(unreach-call) 1 --- inspect .60   .60   21    .053  0      - --- inspect - --- inspect
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i true 2 wit inspect 16   7.7 480 140 150     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2700 0   0      true 2 --- inspect 12     7.1   390   .66 0     
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i true 2 wit inspect 16   7.4 500 140 150     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 650    630    7000 0   0      true 2 --- inspect 11     6.6   400   .66 0     
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i true 2 wit inspect 19   8.9 660 180 150     .0041 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2100 0   0      true 2 --- inspect 14     8.6   500   .62 0     
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1200 11000 .51  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0     
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i timeout 0 --- inspect 900   890   1900 10000 .52  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
loop-invgen/down_true-unreach-call_true-termination.i true 1 wit inspect 150   66   1500 1400 140     7.2    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    380 0   0      timeout 0 --- inspect 960     790     2700   .69 0     
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i true 1 wit inspect 12   4.1 200 85 .32  0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 520    470    7000 0   0      timeout 0 --- inspect 960     790     2800   .65 0     
loop-invgen/half_2_true-unreach-call_true-termination.i true 1 wit inspect 140   66   1200 1200 170     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    350 0   0      timeout 0 --- inspect 960     810     1700   .66 .0041
loop-invgen/heapsort_true-unreach-call_true-termination.i true 2 wit inspect 150   74   1000 1500 150     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1900 0   0      true 2 --- inspect 36     23     680   .62 0     
loop-invgen/id_build_true-unreach-call_true-termination.i true 2 wit inspect 14   6.7 480 130 150     4.4    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.7  3.1  290 0   0      true 2 --- inspect 9.7   5.5   310   .66 0     
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect 22   9.0 520 180 140     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.4  3.0  300 0   0      true 2 --- inspect 13     8.0   490