Tool DIVINE 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 10:00:20 CET 2018-12-10 10:48:16 CET 2018-12-10 11:10:44 CET 2018-12-10 11:13:11 CET 2018-12-12 20:23:24 CET 2018-12-10 10:29:49 CET 2018-12-10 10:51:28 CET
Run set divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-BitVectors
Options --no-symbolic -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/divine-explicit.2018-12-10_1000.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-explicit.2018-12-10_1000.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/divine-explicit.2018-12-10_1000.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/divine-explicit.2018-12-10_1000.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/divine-explicit.2018-12-10_1000.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-explicit.2018-12-10_1000.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 unknown 0 --- inspect 8.2 8.2 430 140 0      0      error (invalid witness file) 0 --- inspect .63 .39 41 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .61 46 0   0   error (invalid witness file) 0 --- inspect .0064 .0082 .52 0     0      - --- inspect - --- inspect
bitvector/sum02_false-unreach-call_true-no-overflow.i unknown 0 --- inspect 8.1 8.2 430 110 0      .0041 error (invalid witness file) 0 --- inspect .62 .38 41 0   0      error (2) 0 --- inspect .020 .022 5.7 0    0   error (invalid witness file) 0 --- inspect .98 .64 49 0   0   error (invalid witness file) 0 --- inspect .0017 .0026 .54 0     0      - --- inspect - --- inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i unknown 0 --- inspect 8.2 8.2 430 110 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .44 41 0   0   error (2) 0 --- inspect .051 .052 5.5 0    0  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i unknown 0 --- inspect 8.4 8.4 430 110 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 42 0   0   error (2) 0 --- inspect .029 .030 5.6 0    0  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i unknown 0 --- inspect 8.2 8.2 430 99 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i unknown 0 --- inspect 8.3 8.3 430 110 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i unknown 0 --- inspect 8.1 8.2 430 96 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .052 .055 5.5 0    0  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 7.9 7.9 370 100 0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.9  4.5  320 0   0   true 2 --- inspect 35     26     500   .62 0  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i unknown 0 --- inspect 8.2 8.2 430 87 0      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  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i unknown 0 --- inspect 8.3 8.3 430 120 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 43 0   0   error (2) 0 --- inspect .033 .034 5.6 0    0  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i unknown 0 --- inspect 8.0 8.0 430 110 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 42 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i unknown 0 --- inspect 8.1 8.1 430 120 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .054 .056 5.5 0    0  
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   230   3400 8600 .0041 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .020 .020 5.7 0    0  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i unknown 0 --- inspect 8.2 8.2 430 90 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 42 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i unknown 0 --- inspect 8.3 8.3 430 120 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 40 0   0   error (2) 0 --- inspect .023 .023 5.6 0    0  
bitvector/modulus_true-unreach-call_true-no-overflow.i unknown 0 --- inspect 8.1 8.2 430 97 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 8.2 8.2 370 110 0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.0  2.7  280 0   0   true 2 --- inspect 31     20     560   .68 0  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i unknown 0 --- inspect 8.3 8.3 430 100 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
bitvector/parity_true-unreach-call_true-no-overflow.i unknown 0 --- inspect 8.3 8.4 430 95 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .022 .023 5.7 0    0  
bitvector/sum02_true-unreach-call_true-no-overflow.i unknown 0 --- inspect 8.0 8.1 430 96 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .39 40 0   0   error (2) 0 --- inspect .019 .021 5.6 0    0  
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 --- inspect 8.4 8.4 430 120 0      0      error (invalid witness file) 0 --- inspect .60 .39 41 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .62 46 0   0   error (invalid witness file) 0 --- inspect .0058 .0075 .54 0     0      - --- inspect - --- inspect
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 --- inspect 8.4 8.4 430 120 0      0      error (invalid witness file) 0 --- inspect .64 .40 41 0   0      error (2) 0 --- inspect .052 .052 5.5 0    0   error (invalid witness file) 0 --- inspect .95 .61 47 0   0   error (invalid witness file) 0 --- inspect .0069 .0086 .54 0     0      - --- inspect - --- inspect
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 --- inspect 8.2 8.2 430 95 0      0      error (invalid witness file) 0 --- inspect .59 .37 41 0   0      error (2) 0 --- inspect .033 .034 5.5 0    0   error (invalid witness file) 0 --- inspect .96 .63 47 0   0   error (invalid witness file) 0 --- inspect .0063 .0081 .53 0     0      - --- inspect - --- inspect
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 --- inspect 8.3 8.3 430 130 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .39 41 0   0   error (2) 0 --- inspect .042 .045 5.6 0    0  
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 --- inspect 8.4 8.4 430 110 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .020 .021 5.7 0    0  
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 --- inspect 8.2 8.2 430 100 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 --- inspect 8.3 8.3 430 100 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 41 0   0   error (2) 0 --- inspect .031 .031 5.5 0    0  
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 --- inspect 8.4 8.3 430 100 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .41 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c unknown 0 --- inspect 8.4 8.4 430 110 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c unknown 0 --- inspect 8.4 8.4 430 91 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0   error (2) 0 --- inspect .036 .037 5.6 0    0  
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 --- inspect 8.2 8.2 430 97 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 41 0   0   error (2) 0 --- inspect .020 .027 5.6 0    0  
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 --- inspect 8.4 8.4 430 110 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .41 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c unknown 0 --- inspect 8.2 8.2 430 91 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .036 .037 5.5 0    0  
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c unknown 0 --- inspect 8.5 8.5 430 120 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 42 0   0   error (2) 0 --- inspect .051 .052 5.5 0    0  
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c unknown 0 --- inspect 8.2 8.2 430 100 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c unknown 0 --- inspect 8.3 8.3 430 120 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .050 .051 5.5 0    0  
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c unknown 0 --- inspect 8.1 8.1 430 100 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .020 .020 5.7 0    0  
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.1 8.1 430 100 0      0      false(unreach-call) 1 wit inspect 3.5  2.0  250 0   0      false(unreach-call) 1 --- inspect 11     7.4   290   .71 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .041 .0082 - --- inspect - --- inspect
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.0 8.0 430 100 0      0      false(unreach-call) 1 wit inspect 3.5  2.0  250 0   0      false(unreach-call) 1 --- inspect 6.9   3.9   310   .62 0   false(unreach-call) 1 --- inspect 3.3  2.0  240 0   0   false(unreach-call) 1 --- inspect .60   .60   20    .041 0      - --- inspect - --- inspect
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.1 8.1 430 99 0      0      false(unreach-call) 1 wit inspect 3.5  2.0  250 0   0      false(unreach-call) 1 --- inspect 12     6.7   300   .68 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .56   .56   20    .041 0      - --- inspect - --- inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c unknown 0 --- inspect 8.2 8.3 430 99 0      0      error (invalid witness file) 0 --- inspect .60 .38 41 0   0      error (2) 0 --- inspect .033 .034 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .60 47 0   0   error (invalid witness file) 0 --- inspect .0056 .0068 .53 0     0      - --- inspect - --- inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.1 8.1 430 110 0      0      false(unreach-call) 1 wit inspect 3.6  2.0  250 0   0      false(unreach-call) 1 --- inspect 6.3   4.0   290   .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 8.2 8.2 430 95 0      0      false(unreach-call) 1 wit inspect 3.5  1.9  250 0   .0041 false(unreach-call) 1 --- inspect 6.3   4.1   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/implicitunsignedconversion_true-unreach-call_true-termination.c true 2 wit inspect 8.2 8.2 370 120 0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.1  1.8  250 0   0   true 2 --- inspect 8.2   4.9   310   .66 0  
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true 2 wit inspect 8.0 8.0 370 96 0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.3  1.9  250 0   0   true 2 --- inspect 12     7.4   300   .68 0  
bitvector-regression/signextension2_true-unreach-call_true-termination.c true 2 wit inspect 8.2 8.2 370 110 0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 7.0   4.0   310   .40 0  
bitvector-regression/signextension_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.1 370 100 0      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 7.2   4.5   310   .62 0  
bitvector-loops/diamond_false-unreach-call2.i unknown 0 --- inspect 8.2 8.2 430 120 0      0      error (invalid witness file) 0 --- inspect .61 .38 41 0   0      error (2) 0 --- inspect .052 .053 5.5 0    0   error (invalid witness file) 0 --- inspect .98 .66 47 0   0   error (invalid witness file) 0 --- inspect .0044 .0059 .55 0     0      - --- inspect - --- inspect
bitvector-loops/overflow_false-unreach-call1.i timeout 0 --- inspect 900   230   3500 8400 .0041 0      error (invalid witness file) 0 --- inspect .63 .41 41 0   0      error (2) 0 --- inspect .041 .042 5.5 0    0   error (invalid witness file) 0 --- inspect .97 .64 47 0   0   error (invalid witness file) 0 --- inspect .0018 .0023 .53 0     0      - --- inspect - --- inspect
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i unknown 0 --- inspect 8.2 8.2 430 98 0      0      error (invalid witness file) 0 --- inspect .63 .40 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .61 47 0   0   error (invalid witness file) 0 --- inspect .0021 .0029 .54 0     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 17 2200 860 27000 22000 .0082 .0041 14 5 23 13   1600 0   .0041 14 5 43 26 1500 3.3 0   14 5 26 16 1700 0   0   14 5 2.9 2.9 110 .21 .0082 36 12 44 26 2800 0   0   36 12 100 68 2400 3.7 0  
    correct results 11 17 89 89 4400 1200 0      0      5 5 18 9.9 1200 0   .0041 5 5 43 26 1500 3.3 0   5 5 17 10 1200 0   0   5 5 2.9 2.9 100 .21 .0082 6 12 26 15 1600 0   0   6 12 100 67 2300 3.7 0  
        correct true 6 12 49 49 2200 640 0      0      0 0 0 0 6 12 26 15 1600 0   0   6 12 100 67 2300 3.7 0  
        correct false 5 5 40 40 2100 510 0      0      5 5 18 9.9 1200 0   .0041 5 5 43 26 1500 3.3 0   5 5 17 10 1200 0   0   5 5 2.9 2.9 100 .21 .0082 0 0
    incorrect results 0 0 0 0 0 0 0
        incorrect true 0 0 0 0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (50 tasks, max score: 86) 17 5 5 5 5 12 12
Run set divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-BitVectors