Tool skink CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
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* [apollon077; apollon078; apollon155] [apollon030; apollon077; apollon078] [apollon077; apollon078] apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 4, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33554 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 22:03:39 CET 2017-12-02 00:36:21 CET 2017-12-02 01:00:42 CET 2017-12-02 01:03:22 CET 2017-12-02 01:04:20 CET 2017-12-02 00:04:19 CET 2017-12-02 00:40:05 CET
Run set skink.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-BitVectors
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -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 --full-output --validate ../../results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i unknown 0 wit inspect 47   730 600 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0041 .26 - wit inspect - wit inspect
bitvector/sum02_false-unreach-call_true-no-overflow.i unknown 0 wit inspect 110   730 1500 error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0015 .28 - wit inspect - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i unknown 0 wit inspect 35   700 370 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .018 4.8
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i unknown 0 wit inspect 31   710 360 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .024 4.8
bitvector/gcd_1_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 84   950 730 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.8
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 27   900 250 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 160    460 timeout 0 wit inspect 960     2600  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 82   870 1200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 46 error (2) 0 wit inspect .018 4.9
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 25   700 260 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.2  310 true 2 wit inspect 44     590  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.6 370 66 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3  310 true 2 wit inspect 160     530  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 20   690 190 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5700 true 2 wit inspect 5.3   260  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 26   730 320 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 780    7000 true 2 wit inspect 6.6   250  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 4.5 260 38 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 780    7000 true 2 wit inspect 5.2   260  
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 1 wit inspect 4.0 320 35 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1700 timeout 0 wit inspect 960     660  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 4.0 250 39 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 660    7000 true 2 wit inspect 21     270  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 4.1 250 43 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6700 true 2 wit inspect 6.3   260  
bitvector/modulus_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 46   730 530 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 45 error (2) 0 wit inspect .022 4.8
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 3.9 240 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  270 true 2 wit inspect 62     610  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.3 300 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  280 timeout 0 wit inspect 960     1100  
bitvector/parity_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 150   740 1800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .021 4.8
bitvector/sum02_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 130   770 1800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 82   780 980 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect - wit inspect
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 45   720 530 error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 39   710 470 error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 100   840 1300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .027 5.0
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 89   760 940 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .024 4.8
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 54   720 650 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .024 5.0
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   1400 9200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .019 4.8
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 62   730 610 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .018 4.9
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c unknown 0 wit inspect 16   660 130 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .46 44 error (2) 0 wit inspect .020 4.9
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c unknown 0 wit inspect 12   640 100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .019 4.8
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 79   980 990 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 4.9
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 15   650 130 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .020 4.9
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c unknown 0 wit inspect 17   650 140 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .019 4.9
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c unknown 0 wit inspect 20   680 180 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.8
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c unknown 0 wit inspect 19   660 170 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .019 4.8
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c unknown 0 wit inspect 18   640 180 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.8
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c unknown 0 wit inspect 22   700 200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.9
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.9 300 46 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 6.3   240   unknown 0 wit inspect 1.9  190 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.9 290 41 false(unreach-call) 1 wit inspect 3.2  270 false(unreach-call) 1 wit inspect 4.9   220   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.7 290 45 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 6.2   210   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c unknown 0 wit inspect 3.8 240 35 error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .69 50 error (invalid witness file) 0 wit inspect .0018 .28 - wit inspect - wit inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.0 300 45 false(unreach-call) 1 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 3.1   230   unknown 0 wit inspect 2.0  180 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
bitvector-regression/signextension_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.9 300 44 false(unreach-call) 1 wit inspect 3.2  250 false(unreach-call) 1 wit inspect 3.1   220   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c true 2 wit inspect 3.6 230 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.5   250  
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true 2 wit inspect 3.7 230 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.3  250 true 2 wit inspect 9.2   230  
bitvector-regression/signextension2_true-unreach-call_true-termination.c true 2 wit inspect 3.7 220 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 5.7   260  
bitvector-regression/signextension_true-unreach-call_true-termination.c true 2 wit inspect 3.9 240 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  240 true 2 wit inspect 5.4   260  
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect 5.6 320 50 false(unreach-call) 1 wit inspect 3.5  260 true -32 wit inspect 3.8   260   unknown 0 wit inspect 2.2  210 true -32 wit inspect .61   18    - wit inspect - wit inspect
bitvector-loops/overflow_false-unreach-call1.i false(unreach-call) 1 wit inspect 4.9 300 41 timeout 0 wit inspect 92    1900 true -32 wit inspect 3.7   260   unknown 0 wit inspect 1.9  190 false(unreach-call) 1 wit inspect 4.0    18    - wit inspect - wit inspect
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 13   460 130 true -32 wit inspect 3.8  260 true -32 wit inspect 4.1   230   unknown 0 wit inspect 2.8  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 50 36 2500   29000 28000 14 -26 120   3900 14 -91 35 1900 14 0 22 1800 14 -58 8.0 150 36 18 5100 39000 36 24 3200 8500
    correct results 21 35 180   7700 1700 6 6 18   1600 5 5 24 1100 0 6 6 6.8 110 9 18 200 2600 12 24 340 4000
        correct true 14 28 140   5600 1400 0 0 0 0 9 18 200 2600 12 24 340 4000
        correct false 7 7 35   2100 310 6 6 18   1600 5 5 24 1100 0 6 6 6.8 110 0 0
    correct-unconfimed results 2 1 17   770 170 0 0 0 0 0 0
        correct-unconfirmed true 1 1 4.0 320 35 0 0 0 0 0 0
        correct-unconfirmed false 1 0 13   460 130 0 0 0 0 0 0
    incorrect results 0 1 -32 3.8 260 3 -96 12 750 0 2 -64 1.2 37 0 0
        incorrect true 0 1 -32 3.8 260 3 -96 12 750 0 2 -64 1.2 37 0 0
        incorrect false 0 0 0 0 0 0 0
score (50 tasks, max score: 86) 36 -26 -91 0 -58 18 24
Run set skink.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-BitVectors