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-06 11:06:04 CET 2018-12-08 03:24:14 CET 2018-12-08 05:17:35 CET 2018-12-08 06:43:53 CET 2018-12-12 20:24:22 CET 2018-12-08 01:45:35 CET 2018-12-08 04:38:54 CET
Run set divine-smt.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-BitVectors
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/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-smt.2018-12-06_1106.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-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/divine-smt.2018-12-06_1106.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-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-smt.2018-12-06_1106.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) 0 wit inspect 29   17   440 320 0      0     timeout 0 wit inspect 96    78    1000 0   0      true -32 --- inspect 7.6   4.2   300   .66 0   unknown 0 --- inspect 4.6  2.7  240 0   0   true -32 --- inspect .65   .66   20    .057 0      - --- inspect - --- inspect
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   230   450 7900 .0041 0     error (invalid witness file) 0 --- inspect .63 .39 43 0   0      error (2) 0 --- inspect .025 .025 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .65 48 0   0   error (invalid witness file) 0 --- inspect .0050 .0062 .52 0     0      - --- inspect - --- inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 25   13   380 230 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 8.9  4.8  370 0   0   timeout 0 --- inspect 960     920     1000   .69 .19
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 27   13   380 280 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 11    5.8  370 0   0   timeout 0 --- inspect 960     920     1000   1.4  0   
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 14   9.9 380 160 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 10    8.1  320 0   0   timeout 0 --- inspect 960     940     1700   .65 0   
bitvector/gcd_2_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   230   520 8100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   
bitvector/gcd_3_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   230   530 9500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 41 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 8.0 8.0 370 99 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 8.6  5.7  320 0   0   true 2 --- inspect 35     26     610   .62 0   
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i unknown 0 --- inspect 8.2 8.2 430 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i timeout 0 --- inspect 900   230   580 9400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0   
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i timeout 0 --- inspect 900   230   710 9200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i timeout 0 --- inspect 900   230   730 8400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .024 .025 5.6 0    0   
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   230   3400 8300 .0041 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/jain_6_true-unreach-call_true-no-overflow_false-termination.i timeout 0 --- inspect 900   230   740 9200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i timeout 0 --- inspect 900   230   620 9600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 41 0   0   error (2) 0 --- inspect .022 .024 5.6 0    0   
bitvector/modulus_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   230   560 9100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 8.1 8.2 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.0  3.3  280 0   0   true 2 --- inspect 36     24     560   .71 0   
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   230   400 7000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 110   33   380 1200 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 28    21    470 0   0   timeout 0 --- inspect 960     950     1000   1.6  0   
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   230   440 8600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 --- inspect 16   12   430 200 0      0     error (invalid witness file) 0 --- inspect .71 .44 43 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .77 47 0   0   error (invalid witness file) 0 --- inspect .0051 .0062 .52 0     0      - --- inspect - --- inspect
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 --- inspect 16   12   440 220 0      0     error (invalid witness file) 0 --- inspect .63 .39 42 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .77 47 0   0   error (invalid witness file) 0 --- inspect .0020 .0034 .52 0     0      - --- inspect - --- inspect
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 --- inspect 28   18   440 320 0      0     error (invalid witness file) 0 --- inspect .77 .46 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .77 49 0   0   error (invalid witness file) 0 --- inspect .0055 .0067 .53 0     0      - --- inspect - --- inspect
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 --- inspect 16   12   430 210 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 42 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0   
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 --- inspect 16   12   430 190 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0   
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 --- inspect 28   18   440 370 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .38 41 0   0   error (2) 0 --- inspect .028 .029 5.7 0    0   
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 18 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 42 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 21 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .41 43 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 error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 22 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .40 41 0   0   error (2) 0 --- inspect .022 .022 5.7 0    0   
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c error - divine failed with signal 11 0 --- inspect 1.5 1.6 200 18 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0   error (2) 0 --- inspect .022 .023 5.7 0    0   
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 25 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/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 41 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0   
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c timeout 0 --- inspect 900   230   420 9600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .027 .028 5.8 0    0   
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c timeout 0 --- inspect 900   230   450 8900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 40 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0   
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c timeout 0 --- inspect 900   230   410 9700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 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 timeout 0 --- inspect 900   230   420 8900 .012  .020 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 42 0   0   error (2) 0 --- inspect .022 .022 5.7 0    0   
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c timeout 0 --- inspect 900   230   480 8900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 40 0   0   error (2) 0 --- inspect .025 .026 5.5 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 4.8  2.7  250 0   .0041 false(unreach-call) 1 --- inspect 14     8.2   310   .75 0   false(unreach-call) 1 --- inspect 4.4  2.6  240 0   0   false(unreach-call) 1 --- inspect .59   .62   20    .041 .0041 - --- inspect - --- inspect
bitvector-regression/implicitunsignedconversion_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 4.3  2.3  250 0   0      false(unreach-call) 1 --- inspect 8.1   4.8   300   .60 0   false(unreach-call) 1 --- inspect 4.2  2.5  240 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 8.0 8.1 430 120 0      0     false(unreach-call) 1 wit inspect 4.0  2.3  250 0   0      false(unreach-call) 1 --- inspect 16     9.2   300   .75 0   false(unreach-call) 1 --- inspect 3.5  2.1  240 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .041 0      - --- inspect - --- inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 39   21   440 440 0      0     timeout 0 --- inspect 92    76    1400 0   0      true -32 --- inspect 7.1   4.0   320   .62 0   unknown 0 --- inspect 4.6  2.7  250 0   0   true -32 --- inspect .58   .59   20    .049 .0041 - --- inspect - --- inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.2 8.2 430 79 0      0     false(unreach-call) 1 wit inspect 3.8  2.1  250 0   0      false(unreach-call) 1 --- inspect 8.5   4.7   300   .66 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0   false(unreach-call) 1 --- inspect .60   .59   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 100 0      0     false(unreach-call) 1 wit inspect 4.6  2.6  250 0   0      false(unreach-call) 1 --- inspect 8.7   5.1   300   .66 0   false(unreach-call) 1 --- inspect 3.7  2.2  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 7.9 8.0 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0   true 2 --- inspect 7.9   4.4   310   .62 0   
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true 2 wit inspect 8.0 8.0 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.0  250 0   0   true 2 --- inspect 15     9.0   300   .68 0   
bitvector-regression/signextension2_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.1 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0   true 2 --- inspect 8.3   5.1   320   .62 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 4.3  2.4  250 0   0   true 2 --- inspect 11     5.7   320   .66 0   
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect 21   14   430 240 0      0     false(unreach-call) 1 wit inspect 4.4  2.4  260 0   0      true -32 --- inspect 8.9   5.0   310   .66 0   unknown 0 --- inspect 4.9  2.9  250 0   0   true -32 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
bitvector-loops/overflow_false-unreach-call1.i timeout 0 --- inspect 900   230   3400 8400 .0041 0     error (invalid witness file) 0 --- inspect .83 .51 42 0   0      error (2) 0 --- inspect .028 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .92 .60 47 0   0   error (invalid witness file) 0 --- inspect .0041 .0067 .39 0     0      - --- inspect - --- inspect
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 54   29   450 620 0      0     timeout 0 wit inspect 92    88    960 0   .020  true -32 --- inspect 9.2   5.2   320   .66 0   true -32 --- inspect 4.7  2.7  250 0   0   true -32 --- inspect .57   .57   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 26 17000 4500 27000 160000 .082 .020 14 6 310 260 5100 0   .025  14 -123 88 50 2800 6.0 0   14 -27 44   26   2400 0   0   14 -123 5.3 5.4 190 .42 .0082 36 20 110 68 4200 0   0   36 12 4000 3800 7300 8.2 .19
    correct results 16 26 280 170 6300 3200 0     0     6 6 26 14 1500 0   .0041 5 5 55 32 1500 3.4 0   5 5 19   11   1200 0   0   5 5 2.9 2.9 100 .21 .0041 10 20 88 57 3100 0   0   6 12 110 74 2400 3.9 0   
        correct true 10 20 220 120 3700 2500 0     0     0 0 0 0 10 20 88 57 3100 0   0   6 12 110 74 2400 3.9 0   
        correct false 6 6 62 54 2600 750 0     0     6 6 26 14 1500 0   .0041 5 5 55 32 1500 3.4 0   5 5 19   11   1200 0   0   5 5 2.9 2.9 100 .21 .0041 0 0
    correct-unconfimed results 3 0 120 67 1300 1400 0     0     0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 3 0 120 67 1300 1400 0     0     0 0 0 0 0 0
    incorrect results 0 0 4 -128 33 18 1200 2.6 0   1 -32 4.7 2.7 250 0   0   4 -128 2.4 2.4 81 .20 .0041 0 0
        incorrect true 0 0 4 -128 33 18 1200 2.6 0   1 -32 4.7 2.7 250 0   0   4 -128 2.4 2.4 81 .20 .0041 0 0
        incorrect false 0 0 0 0 0 0 0
score (50 tasks, max score: 86) 26 6 -123 -27 -123 20 12
Run set divine-smt.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-BitVectors