Tool ULTIMATE Taipan 0.1.23-635dfa2a 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-08 14:19:36 CET 2018-12-09 20:52:23 CET 2018-12-09 21:15:16 CET 2018-12-09 21:17:48 CET 2018-12-12 21:23:28 CET 2018-12-09 20:12:13 CET 2018-12-09 20:55:36 CET
Run set utaipan.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-utaipan.sv-comp19_prop-reachsafety.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-utaipan.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-reachsafety.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-utaipan.sv-comp19_prop-reachsafety.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-utaipan.sv-comp19_prop-reachsafety.ReachSafety-BitVectors
Options --full-output -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/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2018-12-08_1419.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/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2018-12-08_1419.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 180   120   840 2000 .71 0      true -32 wit inspect 4.9  2.7  260 0   0   false(unreach-call) 1 --- inspect 28     17     520   .68 0      unknown 0 --- inspect 5.3  3.0  260 0   0      true -32 --- inspect .66   .68   21    .057 0      - --- inspect - --- inspect
bitvector/sum02_false-unreach-call_true-no-overflow.i unknown 0 --- inspect 12   5.3 390 110 .66 .13   error (invalid witness file) 0 --- inspect .63 .39 41 0   0   error (2) 0 --- inspect .019 .020 5.6 0    0      error (invalid witness file) 0 --- inspect .93 .63 47 0   0      error (invalid witness file) 0 --- inspect .0056 .0071 .52 0     0      - --- inspect - --- inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i timeout 0 --- inspect 900   860   1000 13000 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0     error (2) 0 --- inspect .031 .034 5.7 0    0     
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i timeout 0 --- inspect 900   850   1000 12000 .72 .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 41 0   0     error (2) 0 --- inspect .021 .021 5.5 0    0     
bitvector/gcd_1_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   880   1400 7900 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0     error (2) 0 --- inspect .023 .024 5.6 0    0     
bitvector/gcd_2_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   890   1200 11000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0     error (2) 0 --- inspect .023 .024 5.7 0    0     
bitvector/gcd_3_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   710   8700 8700 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 41 0   0     error (2) 0 --- inspect .027 .032 5.7 0    0     
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i timeout 0 --- inspect 900   880   2300 11000 .69 16      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 42 0   0     error (2) 0 --- inspect .023 .024 5.6 0    0     
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 140   130   710 1700 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 15    10    410 0   0     true 2 --- inspect 180     170     660   .68 0     
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 80   74   400 950 .62 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.6  3.1  290 0   0     true 2 --- inspect 42     39     340   .62 0     
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 59   52   420 830 .62 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.4  3.0  290 0   0     true 2 --- inspect 39     34     360   .62 0     
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 8.7 3.0 380 72 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.0  3.3  290 0   0     true 2 --- inspect 37     31     390   .62 0     
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 2 wit inspect 9.0 3.4 380 69 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.7  3.1  290 0   0     true 2 --- inspect 11     7.0   380   .66 0     
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 11   5.0 380 100 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.2  3.4  290 0   0     true 2 --- inspect 21     16     370   .62 0     
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 11   5.5 370 110 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.9  3.4  290 0   0     true 2 --- inspect 17     12     350   .62 0     
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect 23   17   480 290 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    14    340 0   0     true 2 --- inspect 13     8.5   330   .62 .0041
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 40   22   660 410 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.9  3.7  290 0   0     true 2 --- inspect 36     24     570   .71 .0041
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   870   1900 12000 .73 .14   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 43 0   0     error (2) 0 --- inspect .027 .027 5.6 0    0     
bitvector/parity_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   890   1100 12000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 42 0   0     error (2) 0 --- inspect .027 .028 5.6 0    0     
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   890   590 13000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0     error (2) 0 --- inspect .022 .023 5.7 0    0     
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 31   9.8 620 250 .75 0      false(unreach-call) 1 wit inspect 8.7  4.6  340 0   0   false(unreach-call) 1 --- inspect 20     12     410   .71 0      unknown 0 --- inspect 10    5.4  310 0   0      true -32 --- inspect 1.1    1.1    22    .12  .041  - --- inspect - --- inspect
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 34   10   670 300 .75 .041  false(unreach-call) 1 wit inspect 10    5.3  380 0   0   false(unreach-call) 1 --- inspect 21     12     490   .71 0      unknown 0 --- inspect 11    5.7  360 0   0      true -32 --- inspect 1.2    1.2    23    .11  0      - --- inspect - --- inspect
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 29   9.7 660 230 .75 0      false(unreach-call) 1 wit inspect 7.2  3.8  290 0   0   false(unreach-call) 1 --- inspect 20     12     390   .68 0      unknown 0 --- inspect 7.3  4.0  290 0   0      true -32 --- inspect .91   .91   22    .11  0      - --- inspect - --- inspect
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 47   17   990 390 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 97    83    1000 0   .041 true 2 --- inspect 51     30     770   .68 .0041
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 47   16   1200 370 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 21    13    590 0   0     true 2 --- inspect 52     29     940   .68 0     
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 39   10   1200 310 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    11    570 0   0     out of memory 0 --- inspect 140     89     7000   .64 0     
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 --- inspect 900   780   5900 12000 .64 .18   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0     
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 65   27   1800 500 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    4300 0   0     true 2 --- inspect 45     26     890   .62 0     
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c true 2 wit inspect 52   17   1800 420 .66 .045  - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    4300 0   0     true 2 --- inspect 40     22     950   .66 0     
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c true 2 wit inspect 52   16   1600 480 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4400 0   0     true 2 --- inspect 84     51     1500   .62 0     
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 50   16   1400 440 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    6200 0   0     true 2 --- inspect 38     22     970   .62 .045 
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 52   16   1800 440 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    5400 0   0     true 2 --- inspect 41     23     930   .62 0     
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 270   230   880 3800 .71 .012  - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    850    5000 0   0     true 2 --- inspect 150     130     790   .71 0     
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 62   28   940 590 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 870    800    7000 0   0     true 2 --- inspect 36     25     680   .62 0     
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c timeout 0 --- inspect 900   830   890 11000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .48 42 0   0     error (2) 0 --- inspect .050 .051 5.5 0    0     
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 830   780   900 9700 .71 .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 98    93    530 0   0     true 2 --- inspect 340     310     770   .68 0     
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 50   28   810 560 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 840    770    7000 0   0     true 2 --- inspect 28     17     610   .62 0     
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 13   4.8 350 97 .75 0      false(unreach-call) 1 wit inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect 12     7.0   310   .68 0      false(unreach-call) 1 --- inspect 3.7  2.2  250 0   0      false(unreach-call) 1 --- inspect .56   .56   20    .041 0      - --- inspect - --- inspect
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.0 2.6 360 71 .66 .0041 false(unreach-call) 1 wit inspect 4.0  2.3  250 0   0   false(unreach-call) 1 --- inspect 7.3   4.2   290   .62 0      false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0      false(unreach-call) 1 --- inspect .62   .62   20    .041 0      - --- inspect - --- inspect
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 12   4.7 360 97 .75 0      false(unreach-call) 1 wit inspect 3.8  2.1  250 0   0   false(unreach-call) 1 --- inspect 12     6.8   290   .68 0      false(unreach-call) 1 --- inspect 3.7  2.1  250 0   0      false(unreach-call) 1 --- inspect .56   .56   20    .041 .0041 - --- inspect - --- inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 420   360   870 3900 .71 0      false(unreach-call) 1 wit inspect 6.6  3.6  280 0   0   true -32 --- inspect 8.3   4.4   310   .62 0      false(unreach-call) 1 --- inspect 4.8  2.8  260 0   0      true -32 --- inspect .61   .61   21    .049 0      - --- inspect - --- inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.0 2.7 350 57 .66 0      false(unreach-call) 1 wit inspect 4.0  2.2  250 0   0   false(unreach-call) 1 --- inspect 6.5   3.7   300   .62 0      false(unreach-call) 1 --- inspect 3.8  2.2  240 0   0      false(unreach-call) 1 --- inspect .56   .56   20    .045 .0041 - --- inspect - --- inspect
bitvector-regression/signextension_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.9 2.6 370 61 .66 0      false(unreach-call) 1 wit inspect 3.8  2.1  250 0   0   false(unreach-call) 1 --- inspect 6.5   4.2   300   .62 .0041 false(unreach-call) 1 --- inspect 3.4  2.0  250 0   .0041 false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c true 2 wit inspect 8.0 2.8 340 49 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  250 0   0     true 2 --- inspect 8.2   4.6   310   .66 0     
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true 2 wit inspect 13   5.0 360 96 .75 15      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.6  250 0   0     true 2 --- inspect 14     7.7   300   .71 0     
bitvector-regression/signextension2_true-unreach-call_true-termination.c true 2 wit inspect 8.1 2.8 370 63 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0     true 2 --- inspect 7.8   4.4   300   .62 .0041
bitvector-regression/signextension_true-unreach-call_true-termination.c true 2 wit inspect 7.6 2.9 340 56 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  250 0   0     true 2 --- inspect 7.6   4.3   310   .62 0     
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect 26   17   530 280 .66 0      false(unreach-call) 1 wit inspect 4.1  2.3  260 0   0   false(unreach-call) 1 --- inspect 7.8   4.7   310   .62 0      false(unreach-call) 1 --- inspect 4.5  2.6  250 0   0      true -32 --- inspect .58   .58   21    .049 0      - --- inspect - --- inspect
bitvector-loops/overflow_false-unreach-call1.i timeout 0 --- inspect 900   870   630 10000 .63 0      error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0      error (invalid witness file) 0 --- inspect .95 .61 47 0   0      error (invalid witness file) 0 --- inspect .0046 .0058 .53 0     0      - --- inspect - --- inspect
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 330   310   590 4300 .62 0      false(unreach-call) 1 wit inspect 5.4  3.1  280 0   0   timeout 0 --- inspect 97     85     820   .65 0      unknown 0 --- inspect 4.2  2.4  250 0   0      true -32 --- inspect .59   .59   21    .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 62 14000 13000 55000 170000 34   31     14 -21 67   37   3400 0   0   14 -22 250   170   4800 7.9  .0041 14 7 67 38 3300 0   .0041 14 -219 8.5 8.5 250 .76 .049  36 34 7500 7100 51000 0   .041 36 48 1500 1100 22000 16 .061
    correct results 37 62 3100 2400 28000 34000 25   15     11 11 61   33   3100 0   0   10 10 140   83   3600 6.6  .0041 7 7 27 16 1700 0   .0041 5 5 2.9 2.9 100 .21 .0082 17 34 330 260 6500 0   .041 24 48 1300 1000 15000 16 .061
        correct true 25 50 2000 1500 21000 23000 17   15     0 0 0 0 17 34 330 260 6500 0   .041 24 48 1300 1000 15000 16 .061
        correct false 12 12 1100 860 6600 12000 8.4 .045 11 11 61   33   3100 0   0   10 10 140   83   3600 6.6  .0041 7 7 27 16 1700 0   .0041 5 5 2.9 2.9 100 .21 .0082 0 0
    incorrect results 0 1 -32 4.9 2.7 260 0   0   1 -32 8.3 4.4 310 .62 0      0 7 -224 5.6 5.6 150 .54 .041  0 0
        incorrect true 0 1 -32 4.9 2.7 260 0   0   1 -32 8.3 4.4 310 .62 0      0 7 -224 5.6 5.6 150 .54 .041  0 0
        incorrect false 0 0 0 0 0 0 0
score (50 tasks, max score: 86) 62 -21 -22 7 -219 34 48
Run set utaipan.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-utaipan.sv-comp19_prop-reachsafety.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-utaipan.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-reachsafety.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-reachsafety.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-utaipan.sv-comp19_prop-reachsafety.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-utaipan.sv-comp19_prop-reachsafety.ReachSafety-BitVectors