Tool symbiotic 6.0.3-77d4af47 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* [apollon013; apollon098] 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-07 21:42:05 CET 2018-12-08 23:40:56 CET 2018-12-09 00:46:04 CET 2018-12-09 01:29:54 CET 2018-12-12 21:10:03 CET 2018-12-08 22:46:12 CET 2018-12-08 23:47:25 CET
Run set symbiotic.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-BitVectors
Options --witness witness.graphml -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/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.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/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.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)
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i false(unreach-call) 1 wit inspect .35 .34 19 4.1 0     0      false(unreach-call) 1 wit inspect 4.6  2.5  250 0   0      true -32 --- inspect 7.7   4.8   300   .62 0   false(unreach-call) 1 --- inspect 3.9  2.3  250 0   0      false(unreach-call) 1 --- inspect .59   .59   20    .057 0      - --- inspect - --- inspect
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout (verification) 0 --- inspect 900    900    370 11000   .025 0      error (invalid witness file) 0 --- inspect .55 .34 40 0   0      error (2) 0 --- inspect .025 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .60 47 0   0      error (invalid witness file) 0 --- inspect .0065 .0083 .52 0     0      - --- inspect - --- inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .37 .36 18 4.5 0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 12    6.2  370 0   0      timeout 0 --- inspect 960     920     1000   .78 0     
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .36 .35 18 4.3 0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.8  5.4  370 0   0      timeout 0 --- inspect 960     920     1000   1.5  0     
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .51 .50 21 7.2 0     .28   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 11    8.6  320 0   0      timeout 0 --- inspect 960     950     540   .63 0     
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 26    26    42 350   0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 170    160    560 0   0      timeout 0 --- inspect 960     950     640   1.5  0     
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 33    33    42 530   0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 120    120    560 0   0      timeout 0 --- inspect 960     950     950   .65 0     
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .16 .16 15 1.5 0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.2  4.7  320 0   .0041 true 2 --- inspect 42     32     590   .62 0     
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .17 .17 18 2.1 0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 14    9.1  380 0   0      true 2 --- inspect 220     200     660   .71 0     
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i timeout (verification) 0 --- inspect 900    900    340 8100   .025 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0     
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i timeout (verification) 0 --- inspect 900    900    440 7300   .016 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 41 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0     
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i probably out of memory (killed (signal 9, verification)) 0 --- inspect 170    180    15000 2400   .21  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
bitvector/jain_5_true-unreach-call_true-no-overflow.i probably out of memory (killed (signal 9, verification)) 0 --- inspect 180    180    15000 2400   .16  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i probably out of memory (killed (signal 9, verification)) 0 --- inspect 170    180    15000 2700   .17  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0     
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i probably out of memory (killed (signal 9, verification)) 0 --- inspect 170    180    15000 3000   .094 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .47 41 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
bitvector/modulus_true-unreach-call_true-no-overflow.i timeout (verification) 0 --- inspect 900    900    150 11000   .029 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 40 0   0      error (2) 0 --- inspect .028 .028 5.5 0    0     
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .15 .15 15 1.7 0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.0  3.2  280 0   0      true 2 --- inspect 37     24     560   .71 0     
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .19 .19 17 2.2 0     .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.4  3.5  290 0   0      timeout 0 --- inspect 960     930     2200   .72 0     
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 26    26    25 360   0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 36    27    470 0   0      timeout 0 --- inspect 960     950     1100   .75 .074 
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout (verification) 0 --- inspect 900    900    380 10000   .025 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 1.3  1.3  20 18   0     0      false(unreach-call) 1 wit inspect 15    8.5  430 0   .041  true -32 --- inspect 8.4   5.2   310   .62 0   unknown 0 --- inspect 4.3  2.4  250 0   0      true -32 --- inspect .62   .62   20    .12  0      - --- inspect - --- inspect
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 1.8  1.8  20 23   0     0      false(unreach-call) 1 wit inspect 29    21    480 0   0      true -32 --- inspect 8.4   4.7   310   .66 0   unknown 0 --- inspect 5.6  3.2  260 0   0      true -32 --- inspect .65   .65   20    .11  0      - --- inspect - --- inspect
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect .52 .52 18 6.5 0     0      false(unreach-call) 1 wit inspect 9.6  5.1  420 0   0      true -32 --- inspect 8.4   4.8   310   .62 0   unknown 0 --- inspect 5.6  3.1  250 0   0      true -32 --- inspect .63   .63   20    .11  0      - --- inspect - --- inspect
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect .96 .96 18 12   0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 84    73    1000 0   0      true 2 --- inspect 45     27     780   .68 0     
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect .91 .91 18 14   0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    10    600 0   0      true 2 --- inspect 58     33     970   .71 0     
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect .92 .91 18 12   0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 15    8.3  550 0   0      true 2 --- inspect 31     18     820   .62 0     
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout (verification) 0 --- inspect 900    900    540 9900   .025 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0     
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c timeout (verification) 0 --- inspect 900    900    880 9400   .025 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .40 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout (verification) 0 --- inspect 900    900    150 8600   .025 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0     
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout (verification) 0 --- inspect 900    900    160 9100   .020 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 40 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0     
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout (verification) 0 --- inspect 900    900    230 11000   .025 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c timeout (verification) 0 --- inspect 900    900    220 11000   .025 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .49 42 0   0      error (2) 0 --- inspect .025 .025 5.6 0    0     
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c timeout (verification) 0 --- inspect 900    900    160 11000   .020 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 42 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 2.8  2.8  24 39   0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 760    690    7000 0   0      true 2 --- inspect 41     26     540   .66 0     
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 1 wit inspect 9.1  9.1  31 130   0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 800    740    7000 0   0      timeout 0 --- inspect 960     900     830   .79 .0041
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c timeout (verification) 0 --- inspect 900    900    41 11000   .025 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 2.8  2.8  24 34   0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 710    650    7000 0   0      true 2 --- inspect 27     16     590   .66 0     
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .18 .18 16 1.6 0     0      false(unreach-call) 1 wit inspect 4.0  2.2  250 0   0      false(unreach-call) 1 --- inspect 12     7.4   300   .68 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0      false(unreach-call) 1 --- inspect .57   .57   20    .041 .0041 - --- inspect - --- inspect
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .17 .17 16 2.7 0     0      false(unreach-call) 1 wit inspect 4.0  2.3  250 0   .0041 false(unreach-call) 1 --- inspect 6.7   3.8   300   .66 0   false(unreach-call) 1 --- inspect 4.3  2.5  250 0   0      false(unreach-call) 1 --- inspect .56   .56   20    .041 0      - --- inspect - --- inspect
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .16 .15 16 2.2 0     0      false(unreach-call) 1 wit inspect 4.4  2.4  250 0   0      false(unreach-call) 1 --- inspect 13     7.8   300   .71 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0      false(unreach-call) 1 --- inspect .56   .56   20    .041 .0041 - --- inspect - --- inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c timeout (verification) 0 --- inspect 900    900    660 11000   .025 0      error (invalid witness file) 0 --- inspect .56 .34 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .92 .60 49 0   0      error (invalid witness file) 0 --- inspect .0020 .0025 .52 0     0      - --- inspect - --- inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .16 .15 16 1.7 0     0      false(unreach-call) 1 wit inspect 4.4  2.5  250 0   0      false(unreach-call) 1 --- inspect 6.8   4.4   300   .62 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0      false(unreach-call) 1 --- inspect .56   .56   20    .045 0      - --- inspect - --- inspect
bitvector-regression/signextension_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .21 .20 16 1.7 0     0      false(unreach-call) 1 wit inspect 3.9  2.2  250 0   0      false(unreach-call) 1 --- inspect 6.8   3.9   310   .62 0   false(unreach-call) 1 --- inspect 3.4  1.9  250 0   .0041 false(unreach-call) 1 --- inspect .56   .57   20    .045 0      - --- inspect - --- inspect
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c true 2 wit inspect .14 .14 16 1.4 0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0      true 2 --- inspect 8.0   4.8   310   .66 0     
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true 2 wit inspect .14 .14 15 1.4 0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  250 0   0      true 2 --- inspect 12     7.5   300   .75 .13  
bitvector-regression/signextension2_true-unreach-call_true-termination.c true 2 wit inspect .17 .16 16 1.6 0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  250 0   0      true 2 --- inspect 7.8   4.4   310   .66 0     
bitvector-regression/signextension_true-unreach-call_true-termination.c true 2 wit inspect .14 .13 17 1.5 0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.0  2.7  250 0   0      true 2 --- inspect 7.3   4.5   310   .62 0     
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect .20 .20 17 2.6 0     0      false(unreach-call) 1 wit inspect 4.6  2.6  250 0   0      true -32 --- inspect 6.9   4.3   300   .62 0   false(unreach-call) 1 --- inspect 4.0  2.3  250 0   0      false(unreach-call) 1 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
bitvector-loops/overflow_false-unreach-call1.i false(unreach-call) 1 wit inspect .16 .16 16 2.2 0     0      timeout 0 wit inspect 98    84    1800 0   0      true -32 --- inspect 7.9   4.9   310   .62 0   false(unreach-call) 1 --- inspect 6.8  5.4  240 0   0      false(unreach-call) 1 --- inspect 4.1    4.1    20    .045 0      - --- inspect - --- inspect
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect .52 .52 18 7.4 0     0      timeout 0 wit inspect 92    88    740 0   0      true -32 --- inspect 7.0   4.1   310   .62 0   true -32 --- inspect 3.9  2.2  250 0   0      true -32 --- inspect .57   .58   20    .049 0      - --- inspect - --- inspect
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 50 50 13000    13000    65000 150000   .97 .29 14 10 280 220 5700 0   .045 14 -219 100 60 3700 7.7 0   14 -24 54   33   3100 0   .0041 14 -120 11   11   240 .75 .0082 36 34 2800 2500 29000 0   .0041 36 24 8200 7900 15000 15   .21
    correct results 30 49 100    100    590 1400   0    .28 10 10 84 51 3100 0   .045 5 5 45 27 1500 3.3 0   8 8 33   21   2000 0   .0041 8 8 8.1 8.1 160 .36 .0082 17 34 520 450 7100 0   .0041 12 24 540 400 6700 8.1 .13
        correct true 19 38 97    97    400 1400   0    .28 0 0 0 0 17 34 520 450 7100 0   .0041 12 24 540 400 6700 8.1 .13
        correct false 11 11 5.2  5.2  190 66   0    0    10 10 84 51 3100 0   .045 5 5 45 27 1500 3.3 0   8 8 33   21   2000 0   .0041 8 8 8.1 8.1 160 .36 .0082 0 0
    correct-unconfimed results 2 1 9.6  9.6  49 140   0    0    0 0 0 0 0 0
        correct-unconfirmed true 1 1 9.1  9.1  31 130   0    0    0 0 0 0 0 0
        correct-unconfirmed false 1 0 .52 .52 18 7.4 0    0    0 0 0 0 0 0
    incorrect results 0 0 7 -224 55 33 2100 4.4 0   1 -32 3.9 2.2 250 0   0      4 -128 2.5 2.5 81 .39 0      0 0
        incorrect true 0 0 7 -224 55 33 2100 4.4 0   1 -32 3.9 2.2 250 0   0      4 -128 2.5 2.5 81 .39 0      0 0
        incorrect false 0 0 0 0 0 0 0
score (50 tasks, max score: 86) 50 10 -219 -24 -120 34 24
Run set symbiotic.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-symbiotic.sv-comp19_prop-reachsafety.ReachSafety-BitVectors