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 1 3.0 1.2 150 29 .086 0      1 4.6  2.5  250 0   0      1 7.3   4.5   310   .66 0      0 4.4  2.6  250 0     0      -32 .56   .56   20    .049  0      - -
loops/bubble_sort_false-unreach-call.i 1 480   460   2200 3800 1.1   0      -32 8.4  4.5  270 0   0      1 15     7.7   570   .66 0      0 7.1  3.8  280 0     0      0 .84   .84   21    .053  0      - -
loops/count_up_down_false-unreach-call_true-termination.i 1 9.1 3.6 270 73 .12  0      1 4.6  2.5  250 0   0      1 7.9   4.4   300   .66 .0041 1 4.2  2.4  250 0     0      1 .57   .57   20    .045  0      - -
loops/eureka_01_false-unreach-call_true-termination.i 0 44   26   680 440 .50  0      0 97    81    2000 0   0      0 72     47     7000   .63 0      0 5.6  3.1  250 0     .0041 0 .63   .65   21    .037  0      - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i 1 14   5.0 270 99 .32  .16   1 5.1  2.8  260 0   .0041 1 7.3   4.1   310   .62 0      1 3.7  2.2  250 0     0      1 .59   .59   21    .049  0      - -
loops/insertion_sort_false-unreach-call_true-termination.i 1 430   410   4200 4000 .43  .0082 0 96    80    2000 0   0      1 20     11     480   .62 0      0 5.1  2.9  260 0     0      1 .65   .64   21    .061  0      - -
loops/invert_string_false-unreach-call_true-termination.i 1 28   13   290 210 1.9   0      0 96    81    2000 0   0      1 9.2   5.6   400   .66 0      0 4.2  2.4  260 0     0      -32 .64   .64   21    .061  .0041 - -
loops/linear_search_false-unreach-call.i 0 18   6.5 280 130 .39  0      0 2.7  1.5  200 0   0      0 62     39     7000   .95 0      0 3.0  1.7  200 0     0      0 .52   .52   21    .0041 0      - -
loops/ludcmp_false-unreach-call.i 0 31   18   1500 320 .69  0      -32 13    7.5  460 0   0      -32 42     32     830   .75 0      0 12    7.0  490 0     0      0 3.4    3.4    21    .037  0      - -
loops/matrix_false-unreach-call_true-termination.i 0 510   480   9100 3600 1.6   .0082 0 97    87    1900 0   0      0 59     38     7000   1.7  0      0 5.8  3.2  280 0     0      0 .61   .61   21    .037  0      - -
loops/n.c24_false-unreach-call.i 0 900   880   3000 10000 .72  0      0 .65 .40 40 0   0      0 .026 .028 5.6 0    0      0 .96 .63 48 0     0      0 .0060 .0078 .53 0      0      - -
loops/nec11_false-unreach-call_false-termination.i 1 13   4.7 260 100 .16  0      1 4.0  2.2  250 0   0      1 7.6   4.8   320   .62 0      1 3.8  2.2  250 0     0      1 .57   .57   20    .049  0      - -
loops/nec20_false-unreach-call_true-termination.i 1 19   7.2 290 140 .36  13      1 3.9  2.2  250 0   0      1 8.8   4.9   310   .66 0      0 3.7  2.1  250 0     0      0 .61   .61   20    .061  0      - -
loops/s3_false-unreach-call.i 0 92   67   870 1000 .65  0      -32 6.5  3.5  300 0   .066  0 14     8.4   290   .75 0      0 5.3  2.9  280 0     0      0 .80   .79   22    .29   0      - -
loops/string_false-unreach-call_true-termination.i 1 32   11   300 230 2.7   0      1 5.4  3.0  270 0   0      1 24     14     450   .75 0      0 4.2  2.3  250 0     0      -32 .64   .64   21    .061  0      - -
loops/sum01_bug02_false-unreach-call_true-termination.i 1 16   5.9 290 140 .32  0      1 4.2  2.4  260 0   .0041 1 9.0   5.3   310   .66 0      1 3.9  2.3  250 0     0      1 .62   .62   21    .053  0      - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i 1 15   5.7 290 120 .32  0      1 5.2  2.9  250 0   0      1 8.2   4.7   310   .62 .0041 1 4.1  2.4  250 0     0      -32 .59   .59   21    .053  0      - -
loops/sum01_false-unreach-call_true-termination.i 1 16   6.0 300 140 .31  0      1 4.7  2.6  260 0   0      1 11     6.4   570   .66 0      1 3.8  2.2  250 0     0      -32 .59   .59   21    .053  0      - -
loops/sum03_false-unreach-call_true-termination.i 1 15   5.7 310 130 .31  14      1 4.6  2.5  260 0   0      0 87     57     7000   .70 .0041 1 4.6  2.6  250 0     .35   1 .59   .59   21    .045  0      - -
loops/sum04_false-unreach-call_true-termination.i 1 16   5.8 300 110 .31  0      1 4.0  2.2  250 0   0      1 6.7   4.3   300   .66 0      1 3.6  2.1  250 0     0      1 .59   .59   21    .049  0      - -
loops/sum_array_false-unreach-call.i 1 3.0 1.3 140 27 .094 0      1 4.9  2.7  260 0   0      -32 6.8   3.9   320   .66 0      0 3.7  2.1  250 0     0      -32 .57   .57   20    .057  0      - -
loops/terminator_01_false-unreach-call_true-termination.i 1 8.7 3.5 270 78 .11  .0041 1 4.1  2.3  240 0   0      1 7.9   4.4   300   .66 0      1 3.7  2.1  250 0     0      1 .57   .57   20    .045  0      - -
loops/terminator_02_false-unreach-call_true-termination.i 1 14   5.1 280 120 .32  13      1 3.9  2.2  250 0   0      1 7.0   4.0   310   .66 0      1 3.4  2.0  240 0     0      1 .61   .60   20    .049  0      - -
loops/terminator_03_false-unreach-call_true-termination.i 1 9.0 3.5 270 74 .11  .0041 1 4.4  2.5  250 0   0      1 7.9   4.4   310   .66 0      1 3.7  2.2  250 0     0      1 .57   .57   20    .045  0      - -
loops/trex01_false-unreach-call_true-termination.i 1 14   5.3 270 110 .32  .0041 1 4.5  2.4  250 0   0      1 7.0   4.4   310   .66 0      0 3.7  2.2  250 0     0      -32 .59   .59   20    .053  0      - -
loops/trex02_false-unreach-call_true-termination.i 1 13   4.8 270 96 .31  .0041 1 3.6  2.0  250 0   0      1 6.8   3.9   310   .66 0      0 4.4  2.5  250 0     0      -32 .60   .59   20    .053  0      - -
loops/trex03_false-unreach-call_true-termination.i 1 14   5.1 270 120 .32  0      1 3.9  2.1  260 0   0      1 6.9   4.4   300   .66 0      0 3.6  2.1  250 0     0      1 .57   .57   20    .049  0      - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i 1 17   5.9 300 120 .36  0      1 3.7  2.1  250 0   0      1 12     6.6   340   .62 0      1 3.4  2.0  250 0     0      1 .56   .56   20    .049  0      - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i 1 29   17   280 270 .60  .0041 1 4.3  2.4  250 0   0      1 20     11     480   .66 0      0 4.4  2.5  250 0     0      -32 .58   .58   21    .057  0      - -
loops/vogal_false-unreach-call.i 1 62   46   370 680 .38  .37   1 6.7  4.3  290 0   .0041 0 97     87     590   1.7  0      1 4.6  2.6  260 0     0      1 .66   .67   21    .061  0      - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i 1 14   4.9 300 100 .31  .012  1 3.7  2.1  250 0   0      1 6.6   3.8   310   .66 0      1 3.6  2.1  240 0     0      1 .62   .62   20    .045  0      - -
loops/array_true-unreach-call_true-termination.i 2 3.1 1.4 150 27 .086 0      - - - - 2 4.3  2.4  290 0   0      2 12     6.9   380   .66 0     
loops/bubble_sort_true-unreach-call_true-termination.i 2 17   7.7 430 140 170     0      - - - - 2 5.1  2.8  270 0   0      2 8.7   5.1   310   .66 0     
loops/count_up_down_true-unreach-call_true-termination.i 2 15   7.0 450 120 150     0      - - - - 0 440    430    7000 0   0      2 37     32     470   .62 0     
loops/eureka_01_true-unreach-call.i 2 140   83   1100 1500 140     6.4    - - - - 2 82    67    1900 0   0      0 960     920     4900   .64 0     
loops/eureka_05_true-unreach-call_true-termination.i 1 110   69   930 1000 140     6.5    - - - - 0 900    880    3800 0   0      0 960     920     880   1.5  0     
loops/for_infinite_loop_1_true-unreach-call_false-termination.i 2 13   6.4 460 110 140     .0041 - - - - 2 4.3  2.4  280 0   0      2 7.4   4.6   310   .66 0     
loops/for_infinite_loop_2_true-unreach-call_false-termination.i 2 13   6.4 460 110 150     0      - - - - 2 4.4  2.4  280 0   0      2 8.4   4.7   310   .66 0     
loops/insertion_sort_true-unreach-call_true-termination.i 0 790   760   6300 7400 11     0      - - - - 0 .58 .35 40 0   0      0 .024 .026 5.7 0    0     
loops/invert_string_true-unreach-call_true-termination.i 2 100   65   770 940 150     6.1    - - - - 2 17    11    500 0   0      2 270     250     860   .62 0     
loops/linear_sea.ch_true-unreach-call.i 1 130   68   1300 1400 140     0      - - - - 0 630    610    7000 0   0      0 960     920     710   .65 0     
loops/lu.cmp_true-unreach-call.i 2 64   39   3600 700 150     7.1    - - - - 0 110    99    7000 0   0      2 45     29     870   .62 0     
loops/matrix_true-unreach-call_true-termination.i 2 28   11   510 230 140     0      - - - - 2 5.6  3.1  290 0   0      0 10     6.1   280   .74 0     
loops/n.c11_true-unreach-call_false-termination.i 2 27   11   510 200 150     .0041 - - - - 2 5.0  2.7  290 0   0      2 12     7.0   350   .62 0     
loops/n.c40_true-unreach-call_true-termination.i 2 31   14   530 270 140     40      - - - - 2 4.5  2.5  280 0   0      2 7.7   4.3   310   .66 0     
loops/nec40_true-unreach-call_true-termination.i 2 32   15   510 270 150     0      - - - - 2 4.2  2.3  280 0   0      2 8.0   4.5   310   .66 0     
loops/string_true-unreach-call_true-termination.i 2 18   6.2 200 130 2.5   0      - - - - 2 6.7  3.7  290 0   0      2 12     6.7   400   .66 0     
loops/sum01_true-unreach-call_true-termination.i 2 16   7.5 530 130 170     0      - - - - 0 470    460    7000 0   0      2 11     6.6   340   .62 0     
loops/sum03_true-unreach-call_false-termination.i 2 13   6.7 440 120 140     0      - - - - 2 5.8  3.2  280 0   0      2 8.6   4.9   310   .62 0     
loops/sum04_true-unreach-call_true-termination.i 2 17   7.8 580 140 150     0      - - - - 0 900    900    450 0   0      2 10     6.2   340   .62 0     
loops/sum_array_true-unreach-call.i 1 23   12   200 200 2.5   0      - - - - 0 900    890    3100 0   0      0 960     920     2500   .69 15     
loops/terminator_02_true-unreach-call_true-termination.i 2 14   6.9 470 120 150     0      - - - - 2 4.9  2.8  290 0   0      2 9.1   5.1   310   .66 0     
loops/terminator_03_true-unreach-call_true-termination.i 2 13   6.7 450 120 150     0      - - - - 2 4.8  2.7  280 0   0      2 7.8   4.3   310   .66 0     
loops/trex01_true-unreach-call_true-termination.i 2 13   6.6 440 100 150     .0041 - - - - 2 41    27    1100 0   0      2 7.9   4.5   310   .66 0     
loops/trex02_true-unreach-call_true-termination.i 2 13   6.6 450 110 140     .0041 - - - - 2 5.2  2.9  280 0   0      2 8.1   4.9   310   .66 0     
loops/trex03_true-unreach-call_true-termination.i 2 14   7.0 470 120 140     .0041 - - - - 2 4.7  2.6  280 0   0      2 7.8   4.4   310   .66 0     
loops/trex04_true-unreach-call_false-termination.i 2 13   6.6 460 110 140     .0041 - - - - 2 4.8  2.6  290 0   0      2 7.8   4.4   310   .66 0     
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i 2 18   8.0 470 170 150     0      - - - - 2 4.4  2.4  270 0   0      2 8.4   5.2   310   .66 0     
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i 2 47   31   480 480 150     0      - - - - 2 8.6  4.5  400 0   0      2 9.1   5.5   320   .66 0     
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i 2 18   7.8 470 150 140     0      - - - - 2 4.5  2.5  280 0   0      2 9.0   5.0   320   .66 .0041
loops/vogal_true-unreach-call.i 2 130   58   950 1200 140     6.1    - - - - 2 69    57    1100 0   0      2 560     510     1100   .62 0     
loops/while_infinite_loop_1_true-unreach-call_false-termination.i 2 13   6.4 460 94 140     .28   - - - - 2 5.6  3.1  280 0   0      2 8.1   4.5   320   .66 .0041
loops/while_infinite_loop_2_true-unreach-call_false-termination.i 2 12   6.3 420 110 140     0      - - - - 2 5.5  3.1  270 0   0      2 7.4   4.6   310   .62 0     
loops/while_infinite_loop_3_true-unreach-call_false-termination.i 2 12   6.4 440 110 150     0      - - - - 2 4.1  2.3  270 0   0      2 8.6   4.8   320   .66 0     
loop-acceleration/array_false-unreach-call1_true-termination.i 1 240   220   1900 3400 .16  0      0 97    88    850 0   0      -32 8.3   4.7   310   .56 0      1 3.5  2.0  250 0     0      1 .56   .55   20    .045  0      - -
loop-acceleration/array_false-unreach-call2_true-termination.i 1 4.6 1.7 190 35 .090 0      0 97    87    1300 0   0      -32 8.1   5.0   320   .62 .0041 1 3.6  2.1  250 0     0      1 .56   .56   20    .045  .0041 - -
loop-acceleration/array_false-unreach-call3_true-termination.i 0 470   440   2000 6400 32     0      -32 68    38    3100 0   0      0 87     56     7000   .63 0      0 51    29    3100 0     0      0 96      96      170    .016  0      - -
loop-acceleration/const_false-unreach-call1.i 1 220   200   2500 3100 .11  0      1 24    13    740 0   0      -32 9.9   5.7   330   .66 0      1 3.8  2.2  250 0     0      1 .55   .55   20    .045  0      - -
loop-acceleration/diamond_false-unreach-call1.i 1 48   33   590 580 .32  0      1 5.3  2.9  280 0   0      0 82     51     7000   .63 0      1 4.4  2.5  260 0     0      1 .62   .65   22    .045  0      - -
loop-acceleration/functions_false-unreach-call1_true-termination.i 0 41   26   280 390 14     0      0 .58 .36 41 0   0      0 .020 .021 5.6 0    0      0 1.2  .75 47 0     0      0 .0035 .0046 .52 0      0      - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i 1 9.0 3.6 270 76 .11  .0041 1 4.5  2.5  250 0   0      1 7.0   3.9   300   .66 0      1 4.4  2.5  250 0     0      1 .58   .57   20    .045  0      - -
loop-acceleration/nested_false-unreach-call1.i 1 220   200   3100 2900 .11  13      0 98    84    1800 0   0      -32 10     6.1   310   .66 0      1 7.2  5.4  250 0     0      1 3.4    3.4    20    .045  .0041 - -
loop-acceleration/phases_false-unreach-call1.i 1 370   360   9600 5000 120     0      0 98    83    1900 0   0      -32 8.9   5.3   310   .66 0      1 3.7  2.3  240 0     0      1 .84   .84   20    .045  0      - -
loop-acceleration/phases_false-unreach-call2_false-termination.i 1 8.7 3.4 270 80 .11  0      1 3.6  2.0  250 0   0      1 7.5   4.6   310   .66 0      1 4.1  2.3  250 0     0      1 .58   .57   20    .045  0      - -
loop-acceleration/simple_false-unreach-call1.i 1 220   200   2100 2500 .11  0      0 97    86    1700 0   0      -32 9.0   5.6   320   .62 0      1 3.8  2.3  250 0     0      1 .79   .79   20    .045  .0041 - -
loop-acceleration/simple_false-unreach-call2_true-termination.i 1 9.3 3.6 310 76 .11  .33   1 3.7  2.0  250 0   0      1 8.5   5.0   310   .66 0      -32 3.6  2.1  250 0     0      1 .57   .58   20    .049  0      - -
loop-acceleration/simple_false-unreach-call3_true-termination.i 1 13   5.0 270 98 .31  0      1 3.7  2.0  250 0   0      1 6.8   3.8   300   .62 0      1 3.8  2.2  250 0     0      1 .57   .57   20    .049  0      - -
loop-acceleration/simple_false-unreach-call4.i 1 220   200   2100 3200 .12  .14   0 98    85    1700 0   .0041 -32 10     6.2   320   .66 0      1 3.7  2.2  240 0     0      1 .80   .80   20    .045  0      - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i 1 14   5.1 280 110 .31  0      1 4.6  2.5  250 0   0      1 11     6.2   380   .62 0      1 3.8  2.2  250 0     0      1 .57   .57   21    .045  0      - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i 1 9.1 3.6 280 77 .11  0      1 4.2  2.3  250 0   0      1 11     6.7   380   .66 0      1 3.7  2.1  250 0     0      1 .60   .59   21    .045  0      - -
loop-acceleration/array_true-unreach-call1_true-termination.i 2 38   24   1200 410 150     0      - - - - 2 4.4  2.4  280 0   0      2 12     8.2   350   .66 .0041
loop-acceleration/array_true-unreach-call2_true-termination.i 1 4.2 1.6 190 30 .090 0      - - - - 0 910    900    5000 0   0      0 960     930     660   .62 0     
loop-acceleration/array_true-unreach-call3_true-termination.i 2 15   4.9 200 100 .74  0      - - - - 2 5.1  2.8  280 0   .0041 2 11     6.3   380   .66 0     
loop-acceleration/array_true-unreach-call4_true-termination.i 1 15   4.9 200 100 .87  0      - - - - 0 900    890    6200 0   0      0 960     920     750   1.6  0     
loop-acceleration/const_true-unreach-call1.i 2 14   7.0 460 130 150     0      - - - - 2 5.7  3.1  280 0   0      2 7.8   4.9   310   .66 .0041
loop-acceleration/diamond_true-unreach-call1_true-termination.i 2 74   43   800 720 140     6.1    - - - - 2 25    17    660 0   .0041 0 960     940     560   .65 0     
loop-acceleration/diamond_true-unreach-call2.i 2 51   31   850 510 150     0      - - - - 2 6.4  3.5  300 0   0      2 490     470     640   .62 0     
loop-acceleration/functions_true-unreach-call1_true-termination.i 2 120   65   1300 1400 140     0      - - - - 2 5.8  3.2  280 0   0      2 16     9.8   470   .66 0     
loop-acceleration/multivar_true-unreach-call1_true-termination.i 2 13   6.7 430 100 140     .0082 - - - - 0 440    430    7000 0   0      2 9.0   5.4   310   .62 0     
loop-acceleration/nested_true-unreach-call1.i 2 43   34   550 450 140     0      - - - - 2 7.9  4.4  300 0   .012  2 30     24     470   .62 0     
loop-acceleration/overflow_true-unreach-call1.i 2 120   65   1300 1100 150     6.6    - - - - 2 6.0  3.3  280 0   0      2 8.8   5.0   310   .66 .0041
loop-acceleration/phases_true-unreach-call1.i 1 270   220   9800 3500 270     0      - - - - 0 910    890    6100 0   0      -16 7.5   4.3   300   .66 0     
loop-acceleration/phases_true-unreach-call2_false-termination.i 2 14   6.9 450 110 140     0      - - - - 0 900    900    460 0   0      2 13     9.5   330   .66 0     
loop-acceleration/simple_true-unreach-call1.i 2 120   65   1300 1200 150     .59   - - - - 2 4.2  2.3  280 0   0      2 9.4   5.6   310   .66 0     
loop-acceleration/simple_true-unreach-call2_true-termination.i 2 12   6.2 460 110 150     0      - - - - 2 5.3  2.9  280 0   0      2 7.4   4.7   310   .66 0     
loop-acceleration/simple_true-unreach-call3_true-termination.i 2 120   66   1200 1300 140     0      - - - - 2 4.8  2.7  280 0   0      2 10     6.7   330   .66 0     
loop-acceleration/simple_true-unreach-call4.i 2 15   6.6 470 120 150     0      - - - - 2 4.4  2.4  280 0   0      2 11     5.9   320   .66 0     
loop-acceleration/underapprox_true-unreach-call1_true-termination.i 2 29   16   600 240 140     .0041 - - - - 2 7.7  5.3  390 0   0      2 27     21     450   .62 0     
loop-acceleration/underapprox_true-unreach-call2_true-termination.i 2 14   6.7 470 130 140     0      - - - - 2 5.7  3.1  280 0   0      2 12     6.9   390   .66 .0041
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i 1 300   290   6600 3600 .41  0      1 4.3  2.4  260 0   0      1 7.8   4.4   300   .66 0      -32 3.5  2.0  250 0     0      -32 .58   .58   20    .049  0      - -
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i 1 16   5.3 190 110 1.2   0      - - - - 0 900    890    4200 0   0      0 960     940     700   .65 0     
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i 1 16   5.2 200 120 .92  0      - - - - 0 900    900    900 0   0      0 960     940     930   .63 0     
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i 1 16   5.2 190 100 1.2   0      - - - - 0 910    890    6100 0   0      0 960     930     740   .65 .0041
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i 2 17   6.6 200 140 3.8   0      - - - - 0 900    890    1800 0   0      2 22     16     400   .66 0     
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i 2 14   6.7 450 110 150     0      - - - - 2 5.8  3.2  280 0   0      2 7.8   4.9   320   .66 .041 
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i 2 14   6.7 440 120 190     0      - - - - 2 5.2  2.9  280 0   0      2 8.8   5.4   310   .66 0     
loop-crafted/simple_array_index_value_true-unreach-call4.i.v+lhb-reducer.c 0 49   42   15000 610 .23  0      - - - - 0 .59 .36 41 0   0      0 .020 .022 5.6 0    0     
loop-crafted/simple_array_index_value_true-unreach-call4.i.v+nlh-reducer.c 0 49   42   15000 600 .25  0      - - - - 0 .70 .42 41 0   0      0 .020 .021 5.6 0    0     
loop-invgen/id_trans_false-unreach-call_true-termination.i 1 14   5.0 270 100 .32  0      1 3.8  2.1  250 0   0      1 7.1   4.5   310   .66 0      1 4.4  2.5  240 0     .0041 1 .60   .60   21    .053  0      - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i 2 16   7.7 480 140 150     0      - - - - 0 900    890    2700 0   0      2 12     7.1   390   .66 0     
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i 2 16   7.4 500 140 150     0      - - - - 0 650    630    7000 0   0      2 11     6.6   400   .66 0     
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i 2 19   8.9 660 180 150     .0041 - - - - 0 900    890    2100 0   0      2 14     8.6   500   .62 0     
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i 0 900   890   1200 11000 .51  0      - - - - 0 .75 .46 41 0   0      0 .027 .028 5.6 0    0     
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i 0 900   890   1900 10000 .52  0      - - - - 0 .58 .36 41 0   0      0 .021 .022 5.6 0    0     
loop-invgen/down_true-unreach-call_true-termination.i 1 150   66   1500 1400 140     7.2    - - - - 0 900    900    380 0   0      0 960     790     2700   .69 0     
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i 1 12   4.1 200 85 .32  0      - - - - 0 520    470    7000 0   0      0 960     790     2800   .65 0     
loop-invgen/half_2_true-unreach-call_true-termination.i 1 140   66   1200 1200 170     0      - - - - 0 900    900    350 0   0      0 960     810     1700   .66 .0041
loop-invgen/heapsort_true-unreach-call_true-termination.i 2 150   74   1000 1500 150     0      - - - - 0 900    890    1900 0   0      2 36     23     680   .62 0     
loop-invgen/id_build_true-unreach-call_true-termination.i 2 14   6.7 480 130 150     4.4    - - - - 2 5.7  3.1  290 0   0      2 9.7   5.5   310   .66 0     
loop-invgen/large_const_true-unreach-call_true-termination.i 2 22   9.0 520 180 140     0      - - - - 2 5.4  3.0  300 0   0      2 13     8.0   490   .66 0     
loop-invgen/nest-if3_true-unreach-call_true-termination.i 2 14   6.7 450 110 140     0      - - - - 0 900    890    1300 0   0      2 7.9   4.4   310   .62 0     
loop-invgen/nested6_true-unreach-call_true-termination.i 0 900   890   2600 7900 2.2   .39   - - - - 0 .62 .40 41 0   0      0 .020 .021 5.6 0    0     
loop-invgen/nested9_true-unreach-call_true-termination.i 2 19   8.4 620 170 140     .43   - - - - 0 570    540    7000 0   0      2 20     12     450   .66 0     
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i 1 820   800   1800 8900 150     0      - - - - 0 900    890    7000 0   .0041 -16 7.5   4.2   310   .66 0     
loop-invgen/seq_true-unreach-call_true-termination.i 1 150   68   1100 1500 140     6.3    - - - - 0 900    900    500 0   0      0 960     790     1100   .63 .0041
loop-invgen/string_concat-noarr_true-unreach-call_false-termination.i 1 150   67   1400 1400 150     6.3    - - - - 0 900    880    5800 0   0      0 960     830     3100   1.5  0     
loop-invgen/up_true-unreach-call_true-termination.i 1 150   66   1500 1400 150     .0041 - - - - 0 900    900    510 0   0      0 960     790     2900   .68 0     
loop-invgen/SpamAssassin-loop_true-unreach-call.i.v+cfa-reducer.c 0 900   890   670 8000 .54  0      - - - - 0 .78 .48 42 0   0      0 .023 .023 5.6 0    0     
loop-invgen/apache-escape-absolute_true-unreach-call.i.v+cfa-reducer.c 0 900   880   1000 11000 .45  0      - - - - 0 .75 .46 41 0   0      0 .020 .021 5.6 0    0     
loop-invgen/apache-get-tag_true-unreach-call.i.p+lhb-reducer.c 0 900   880   820 9300 .61  0      - - - - 0 .59 .36 42 0   0      0 .021 .022 5.6 0    0     
loop-invgen/apache-get-tag_true-unreach-call.i.p+nlh-reducer.c 0 900   880   1200 10000 .95  0      - - - - 0 .62 .38 41 0   0      0 .026 .026 5.6 0    0     
loop-invgen/apache-get-tag_true-unreach-call.i.p+sep-reducer.c 0 900   870   6700 13000 1.6   0      - - - - 0 .71 .43 40 0   0      0 .026 .027 5.6 0    0     
loop-invgen/apache-get-tag_true-unreach-call.i.v+lhb-reducer.c 0 900   890   870 10000 .40  0      - - - - 0 .79 .47 41 0   0      0 .022 .023 5.6 0    0     
loop-invgen/apache-get-tag_true-unreach-call.i.v+nlh-reducer.c 0 900   880   840 11000 .39  0      - - - - 0 .76 .47 41 0   0      0 .021 .022 5.6 0    0     
loop-invgen/id_build_true-unreach-call.i.p+nlh-reducer.c 0 900   880   1200 8700 .88  0      - - - - 0 .82 .49 43 0   0      0 .024 .025 5.6 0    0     
loop-invgen/id_build_true-unreach-call.i.p+sep-reducer.c 0 900   880   1600 9000 .90  0      - - - - 0 .64 .40 41 0   0      0 .023 .025 5.6 0    0     
loop-invgen/id_build_true-unreach-call.i.v+lhb-reducer.c 0 900   890   740 7900 .50  0      - - - - 0 .79 .47 41 0   0      0 .021 .022 5.6 0    0     
loop-lit/afnp2014_true-unreach-call_true-termination.c.i 2 6.1 2.3 200 48 .10  0      - - - - 0 430    420    7000 0   0      2 8.4   5.3   320   .66 0     
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i 2 19   11   570 170 140     0      - - - - 0 900    900    750 0   0      2 10     5.8   310   .66 0     
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i 2 15   7.2 460 150 140     0      - - - - 0 900    900    380 0   0      2 9.4   5.4   330   .66 0     
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i 2 16   7.4 460 120 150     0      - - - - 0 410    400    7000 0   0      2 8.4   5.3   320   .66 0     
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i 2 6.5 2.5 220 50 .10  0      - - - - 2 4.8  2.6  280 0   0      2 8.2   4.7   310   .62 0     
loop-lit/css2003_true-unreach-call_true-termination.c.i 2 6.3 2.5 200 51 .11  0      - - - - 2 5.7  3.1  280 0   0      2 7.4   4.7   310   .66 0     
loop-lit/ddlm2013_true-unreach-call.i 2 770   750   1500 9000 .71  0      - - - - 0 360    340    7000 0   0      2 11     6.4   390   .62 0     
loop-lit/gj2007_true-unreach-call_true-termination.c.i 2 81   39   1500 880 140     6.1    - - - - 0 900    900    410 0   0      2 110     71     960   .62 .0041
loop-lit/gj2007b_true-unreach-call_true-termination.c.i 2 20   8.6 460 150 140     0      - - - - 0 900    890    2500 0   0      2 11     6.6   350   .66 0     
loop-lit/gr2006_true-unreach-call_true-termination.c.i 2 110   47   1700 990 150     0      - - - - 2 11    5.9  430 0   0      2 41     28     870   .66 0     
loop-lit/gsv2008_true-unreach-call_true-termination.c.i 2 380   360   1100 4200 .44  .0041 - - - - 0 900    890    3200 0   .0041 2 8.4   4.7   320   .66 0     
loop-lit/hhk2008_true-unreach-call_true-termination.c.i 2 15   7.2 480 120 140     0      - - - - 0 420    410    7000 0   0      2 11     6.0   330   .66 0     
loop-lit/jm2006_true-unreach-call_true-termination.c.i 2 15   7.2 450 120 150     0      - - - - 0 470    460    7000 0   0      2 8.6   4.9   310   .66 0     
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i 2 15   7.4 440 110 140     .41   - - - - 0 420    410    7000 0   0      2 11     6.1   330   .66 0     
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i 1 150   83   1300 1400 140     6.9    - - - - 0 900    890    5200 0   0      0 960     930     910   .63 0     
loop-lit/gcnr2008_false-unreach-call_false-termination.i 1 14   5.4 270 100 .33  0      1 4.3  2.4  250 0   0      1 7.0   3.9   310   .62 0      1 4.7  2.7  250 0     0      1 .63   .62   20    .057  0      - -
loop-lit/gj2007_true-unreach-call.c.i.p+lhb-reducer.c 2 86   41   1400 790 140     7.4    - - - - 0 910    790    4900 0   0      2 100     67     1100   .62 0     
loop-lit/gj2007_true-unreach-call.c.i.p+nlh-reducer.c 2 89   41   1100 790 150     0      - - - - 0 910    800    4300 0   0      2 100     72     1000   .62 0     
loop-lit/gsv2008_true-unreach-call.c.i.p+cfa-reducer.c 2 440   430   1200 4600 150     0      - - - - 0 900    890    3200 0   0      2 9.4   5.6   320   .66 0     
loop-lit/gsv2008_true-unreach-call.c.i.v+cfa-reducer.c 2 450   430   1100 4700 160     0      - - - - 0 900    890    3300 0   0      2 10     5.9   310   .66 0     
loop-lit/gsv2008_true-unreach-call.c.i.v+lhb-reducer.c 0 840   830   940 7500 .70  .39   - - - - 0 .60 .37 43 0   0      0 .024 .025 5.6 0    0     
loop-lit/jm2006_true-unreach-call.c.i.v+cfa-reducer.c 0 740   730   710 7400 .77  0      - - - - 0 .65 .40 42 0   0      0 .026 .027 5.6 0    0     
loop-new/count_by_1_true-unreach-call_true-termination.i 2 14   6.6 460 110 140     .0041 - - - - 2 5.5  3.0  280 0   0      2 9.4   5.6   310   .66 0     
loop-new/count_by_1_variant_true-unreach-call_true-termination.i 2 18   8.1 450 150 150     .0082 - - - - 2 5.1  2.8  280 0   0      2 9.8   5.8   320   .66 0     
loop-new/count_by_2_true-unreach-call_true-termination.i 2 140   65   1300 1400 140     0      - - - - 2 5.7  3.2  280 0   0      2 10     5.8   340   .66 0     
loop-new/count_by_k_true-unreach-call_true-termination.i 1 120   65   1100 1500 150     .049  - - - - 0 910    890    5600 0   .0041 0 960     840     1300   .67 0     
loop-new/count_by_nondet_true-unreach-call_true-termination.i 0 900   890   1200 9800 .45  0      - - - - 0 .74 .45 42 0   0      0 .021 .022 5.6 0    0     
loop-new/gauss_sum_true-unreach-call_true-termination.i 1 33   27   200 380 .45  .0082 - - - - 0 910    890    5100 0   0      0 960     830     820   .67 0     
loop-new/half_true-unreach-call_true-termination.i 0 590   570   1200 6700 11     0      - - - - 0 .62 .38 41 0   0      0 .021 .022 5.6 0    0     
loop-new/nested_true-unreach-call_true-termination.i 0 900   890   720 8100 .61  0      - - - - 0 .72 .45 41 0   0      0 .025 .026 5.6 0    0     
loop-new/gauss_sum_true-unreach-call.i.p+cfa-reducer.c 1 400   300   1800 4400 150     .020  - - - - 0 910    890    5100 0   0      0 960     890     770   .63 0     
loop-new/gauss_sum_true-unreach-call.i.p+lhb-reducer.c 1 400   300   1600 4500 150     .020  - - - - 0 910    890    5100 0   0      0 960     860     800   .63 0     
loop-new/gauss_sum_true-unreach-call.i.v+cfa-reducer.c 1 350   280   1400 4200 150     6.1    - - - - 0 910    890    6100 0   0      0 960     880     930   .63 0     
loop-industry-pattern/aiob_1_true-unreach-call.c 2 89   49   1100 700 150     0      - - - - 2 72    63    1300 0   0      0 12     6.4   290   .73 0     
loop-industry-pattern/aiob_2_true-unreach-call.c 2 88   48   1300 630 170     0      - - - - 2 78    67    1300 0   0      0 11     6.0   290   .73 0     
loop-industry-pattern/aiob_3_true-unreach-call.c 2 89   48   1300 640 170     0      - - - - 2 93    79    1300 0   0      0 13     7.7   290   .75 0     
loop-industry-pattern/aiob_4_true-unreach-call.c 2 85   47   1300 700 150     6.6    - - - - 2 63    51    1200 0   0      0 11     6.5   280   .75 0     
loop-industry-pattern/aiob_4_true-unreach-call.c.v+cfa-reducer.c 2 99   50   1300 910 150     0      - - - - 2 82    70    1900 0   0      2 19     12     470   .66 0     
loop-industry-pattern/aiob_4_true-unreach-call.c.v+lh-reducer.c 2 95   49   1200 680 150     0      - - - - 2 84    70    1500 0   0      2 18     12     480   .66 0     
loop-industry-pattern/aiob_4_true-unreach-call.c.v+lhb-reducer.c 2 110   53   1300 840 150     0      - - - - 2 100    84    2000 0   0      2 29     18     530   .66 0     
loop-industry-pattern/aiob_4_true-unreach-call.c.v+nlh-reducer.c 2 71   31   1700 700 150     0      - - - - 2 8.6  4.5  280 0   0      2 35     23     810   .66 0     
loop-industry-pattern/mod3_true-unreach-call.c 2 29   21   450 300 150     0      - - - - 2 6.7  4.6  320 0   0      0 11     6.2   280   .74 0     
loop-industry-pattern/mod3_true-unreach-call.c.v+cfa-reducer.c 0 770   760   740 8000 .75  0      - - - - 0 .58 .36 40 0   0      0 .020 .021 5.7 0    0     
loop-industry-pattern/mod3_true-unreach-call.c.v+lhb-reducer.c 0 900   890   720 11000 .41  0      - - - - 0 .61 .37 41 0   0      0 .024 .025 5.7 0    0     
loop-industry-pattern/mod3_true-unreach-call.c.v+sep-reducer.c 0 900   890   630 8600 .45  .56   - - - - 0 .76 .47 41 0   0      0 .027 .028 5.6 0    0     
loop-industry-pattern/nested_true-unreach-call.c 2 75   34   1600 680 140     .0041 - - - - 0 900    890    2300 0   0      2 70     47     910   .62 0     
loop-industry-pattern/ofuf_1_true-unreach-call.c 2 30   13   470 280 150     0      - - - - 0 5.0  2.7  260 0   0      2 11     6.3   360   .66 0     
loop-industry-pattern/ofuf_2_true-unreach-call.c 2 27   11   500 240 140     0      - - - - 0 4.9  2.6  260 0   0      2 10     6.1   350   .66 0     
loop-industry-pattern/ofuf_3_true-unreach-call.c 2 27   11   500 220 150     0      - - - - 0 5.8  3.2  260 0   0      2 11     6.3   330   .62 0     
loop-industry-pattern/ofuf_4_true-unreach-call.c 2 27   11   500 240 140     0      - - - - 0 5.0  2.7  260 0   0      2 11     6.1   350   .62 0     
loop-industry-pattern/ofuf_5_true-unreach-call.c 2 28   11   510 250 140     0      - - - - 0 6.1  3.3  260 0   0      2 10     6.2   330   .66 0     
loops/heavy_true-unreach-call.c 2 110   37   6600 720 140     0      - - - - 0 880    880    7000 0   0      2 25     14     2700   .62 0     
loops/compact_false-unreach-call.c 0 15   4.9 190 100 .23  0      0 97    85    2000 0   0      -32 11     5.8   600   .66 0      0 3.9  2.3  250 0     0      0 .57   .57   20    .045  0      - -
loops/heavy_false-unreach-call.c 0 220   210   5500 2600 .16  0      0 97    85    2500 0   0      -32 24     14     2700   .66 0      0 97    95    250 .025 0      0 96      96      20    1.5    0      - -
loops-crafted-1/Mono1_false-unreach-call1.c 1 370   360   11000 5800 120     0      0 97    79    1900 0   0      -32 8.3   5.2   310   .62 0      1 4.5  2.7  250 0     0      1 .69   .69   20    .045  0      - -
loops-crafted-1/Mono3_false-unreach-call1.c 1 640   620   11000 7500 .32  .25   0 97    78    1900 0   .0041 -32 8.1   5.0   310   .66 0      1 3.5  2.0  250 0     0      1 .57   .57   20    .045  0      - -
loops-crafted-1/Mono4_false-unreach-call1.c 1 620   600   9200 7600 .34  0      0 98    84    1900 0   0      -32 9.2   5.2   320   .66 0      1 3.6  2.1  250 0     0      1 .57   .57   20    .045  0      - -
loops-crafted-1/Mono5_false-unreach-call1.c 1 370   360   9600 4900 120     .0041 0 97    79    1700 0   0      -32 7.9   4.3   310   .66 0      1 3.6  2.1  250 0     0      1 .59   .59   20    .045  0      - -
loops-crafted-1/Mono6_false-unreach-call1.c 1 380   360   9700 4800 120     0      0 98    82    1900 0   0      -32 7.9   4.9   320   .66 0      1 3.4  2.0  250 0     0      1 .59   .59   20    .045  0      - -
loops-crafted-1/nested3_false-unreach-call.c 1 220   200   2500 2600 .11  0      0 97    82    1900 0   0      -32 12     6.9   310   .66 0      1 4.1  2.6  250 0     0      1 1.0    1.0    20    .045  0      - -
loops-crafted-1/nested5_false-unreach-call.c 1 220   200   2000 2700 .11  0      0 97    84    1700 0   0      -32 7.4   4.2   310   .66 0      1 3.9  2.4  250 0     0      1 1.0    1.0    20    .045  0      - -
loops-crafted-1/Mono1_true-unreach-call1.c 1 270   220   11000 3100 320     20      - - - - 0 730    720    7000 0   0      -16 6.8   3.9   290   .66 0     
loops-crafted-1/nested3_true-unreach-call.c 2 52   36   680 520 140     6.3    - - - - 0 900    880    3700 0   0      2 290     260     1400   .62 0     
loops-crafted-1/nested5_true-unreach-call.c 2 28   20   480 280 170     0      - - - - 2 7.5  4.1  290 0   0      2 35     27     470   .66 0     
loop-invariants/bin-suffix-5_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c 2 13   6.6 440 100 140     .57   - - - - 0 960    920    3400 0   0      2 14     7.8   290   .75 .0082
loop-invariants/const_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c 2 13   6.5 470 120 150     0      - - - - 2 5.7  3.1  290 0   0      2 7.6   4.3   310   .62 0     
loop-invariants/eq1_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c 2 14   7.0 470 120 150     0      - - - - 0 900    900    690 0   0      2 8.5   5.2   310   .66 0     
loop-invariants/eq2_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c 2 14   6.7 470 130 140     .0041 - - - - 0 420    410    7000 0   0      2 12     7.7   310   .66 0     
loop-invariants/even_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c 2 140   66   1400 1400 150     0      - - - - 2 4.7  2.6  280 0   0      2 9.0   5.5   310   .66 0     
loop-invariants/mod4_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c 2 140   65   1400 1600 140     6.1    - - - - 2 5.2  2.9  290 0   0      2 7.8   4.4   310   .66 0     
loop-invariants/odd_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c 1 140   65   1400 1500 150     0      - - - - 0 5.5  3.1  280 0   0      -16 6.4   4.1   300   .66 0     
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)
total 208 275 38000 33000 310000 400000 17000 230      59 -95 2100 1700 48000 0   .086 59 -545 1100 690 63000 40 .016  59 -28 380   260   17000 .025 .36 59 -283 230   230   1300 4.4  .016  149 124 46000 44000 280000 0   .033 149 122 24000 22000 78000 84   16    
    correct results 150 251 12000 9600 180000 130000 14000 170      33 33 160 91 8900 0   .012 31 31 300 170 11000 20 .0082 36 36 140   85   8900 0     .35 37 37 26   26   760 1.8  .012  62 124 1100 820 30000 0   .020 93 186 3100 2400 42000 60   .078
        correct true 101 202 6200 4100 79000 61000 14000 120      0 0 0 0 62 124 1100 820 30000 0   .020 93 186 3100 2400 42000 60   .078
        correct false 49 49 6000 5500 98000 72000 490 54      33 33 160 91 8900 0   .012 31 31 300 170 11000 20 .0082 36 36 140   85   8900 0     .35 37 37 26   26   760 1.8  .012  0 0
    correct-unconfimed results 32 24 5400 4100 61000 58000 2700 59      0 0 0 0 0 0
        correct-unconfirmed true 24 24 4100 2900 41000 43000 2700 59      0 0 0 0 0 0
        correct-unconfirmed false 8 0 1400 1200 20000 15000 36 .0082 0 0 0 0 0 0
    incorrect results 0 4 -128 96 54 4100 0   .066 18 -576 210 130 8900 12 .0041 2 -64 7.1 4.1 500 0     0    10 -320 5.9 5.9 200 .55 .0041 0 4 -64 28 16 1200 2.6 0    
        incorrect true 0 4 -128 96 54 4100 0   .066 18 -576 210 130 8900 12 .0041 2 -64 7.1 4.1 500 0     0    10 -320 5.9 5.9 200 .55 .0041 0 0
        incorrect false 0 0 0 0 0 0 4 -64 28 16 1200 2.6 0    
score (208 tasks, max score: 357) 275 -95 -545 -28 -283 124 122
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