Tool ULTIMATE Kojak 0.1.23-3204b741 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*
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: 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]
Date of execution 2017-12-02 02:33:02 CET 2017-12-03 03:22:18 CET 2017-12-03 03:55:21 CET 2017-12-03 04:22:06 CET 2017-12-03 04:36:43 CET 2017-12-03 00:36:56 CET 2017-12-03 03:32:10 CET
Run set ukojak.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-BitVectors
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/ukojak.2017-12-02_0233.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 false(unreach-call) 1 wit inspect 31   490 280 false(unreach-call) 1 wit inspect 3.8  270 false(unreach-call) 1 wit inspect 36     590   unknown 0 wit inspect 5.2  220 true -32 wit inspect .61   19    - wit inspect - wit inspect
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   680 10000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .90 50 error (invalid witness file) 0 wit inspect .0018 .29 - wit inspect - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 720   1600 7700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    300 timeout 0 wit inspect 960     1100  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i timeout 0 wit inspect 900   1500 7600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .028 4.8
bitvector/gcd_1_true-unreach-call_true-no-overflow.i error (7) 0 wit inspect 660   670 4700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .024 4.9
bitvector/gcd_2_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   520 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 4.9
bitvector/gcd_3_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   500 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .022 5.0
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 11   580 97 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  300 true 2 wit inspect 46     580  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 100   2600 1100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5  310 true 2 wit inspect 130     680  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900   1700 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .018 5.0
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 16   330 170 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  280 true 2 wit inspect 21     300  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 6.2 320 50 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  280 true 2 wit inspect 6.3   270  
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   5200 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .020 4.9
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900   2100 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.8
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900   2900 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.9
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect 110   660 1500 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    320 true 2 wit inspect 9.4   280  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 120   470 1700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  290 true 2 wit inspect 52     640  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 240   780 2900 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5  280 timeout 0 wit inspect 960     1100  
bitvector/parity_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   720 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .018 4.9
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   740 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.9
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   6300 13000 error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   6200 13000 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .93 50 error (invalid witness file) 0 wit inspect .0015 .34 - wit inspect - wit inspect
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 88   1000 1100 true -32 wit inspect 6.8  280 false(unreach-call) 1 wit inspect 17     410   unknown 0 wit inspect 4.5  220 true -32 wit inspect .76   20    - wit inspect - wit inspect
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   6300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .019 4.8
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   6300 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   6000 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 45 error (2) 0 wit inspect .019 4.8
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   6400 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.8
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   6500 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .019 4.9
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout 0 wit inspect 910   6500 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .42 43 error (2) 0 wit inspect .020 4.9
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout 0 wit inspect 900   6400 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 4.9
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   6400 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.8
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   6500 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .019 4.9
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c timeout 0 wit inspect 900   1700 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .47 44 error (2) 0 wit inspect .018 4.8
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c timeout 0 wit inspect 900   1500 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .020 5.0
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c timeout 0 wit inspect 900   1400 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .025 4.8
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c timeout 0 wit inspect 900   1500 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.9
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c timeout 0 wit inspect 900   1600 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .018 4.9
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.1 240 70 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 12     230   unknown 0 wit inspect 3.1  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.2 240 39 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.9   220   unknown 0 wit inspect 3.5  180 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.2 240 74 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 6.8   220   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .78   18    - wit inspect - wit inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 120   1000 1500 false(unreach-call) 1 wit inspect 5.4  280 true -32 wit inspect 5.4   270   unknown 0 wit inspect 4.0  210 true -32 wit inspect .71   19    - wit inspect - wit inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.1 250 40 false(unreach-call) 1 wit inspect 3.0  250 false(unreach-call) 1 wit inspect 4.4   220   unknown 0 wit inspect 3.7  180 false(unreach-call) 1 wit inspect .75   18    - wit inspect - wit inspect
bitvector-regression/signextension_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.2 250 36 false(unreach-call) 1 wit inspect 3.1  250 false(unreach-call) 1 wit inspect 4.4   220   unknown 0 wit inspect 2.1  180 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c true 2 wit inspect 4.2 250 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.0   250  
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true 2 wit inspect 8.3 250 64 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 9.0   230  
bitvector-regression/signextension2_true-unreach-call_true-termination.c true 2 wit inspect 4.5 260 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 6.0   260  
bitvector-regression/signextension_true-unreach-call_true-termination.c true 2 wit inspect 4.4 260 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  240 true 2 wit inspect 5.4   250  
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect 5.9 300 52 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 6.7   270   unknown 0 wit inspect 4.2  210 true -32 wit inspect .63   18    - wit inspect - wit inspect
bitvector-loops/overflow_false-unreach-call1.i timeout 0 wit inspect 900   2000 11000 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0018 .29 - wit inspect - wit inspect
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i timeout 0 wit inspect 900   4600 13000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0013 .30 - 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 33 28000 110000 340000 14 -24 37   2600 14 -24 97   2700 14 0 38 2000 14 -123 6.1 170 36 24 88 4400 36 20 2200 6000
    correct results 21 33 1600 12000 19000 8 8 28   2100 8 8 92   2400 0 5 5 3.4 92 12 24 74 3300 10 20 290 3700
        correct true 12 24 1300 8300 15000 0 0 0 0 12 24 74 3300 10 20 290 3700
        correct false 9 9 270 4100 3200 8 8 28   2100 8 8 92   2400 0 5 5 3.4 92 0 0
    incorrect results 0 1 -32 6.8 280 1 -32 5.4 270 0 4 -128 2.7 76 0 0
        incorrect true 0 1 -32 6.8 280 1 -32 5.4 270 0 4 -128 2.7 76 0 0
        incorrect false 0 0 0 0 0 0 0
score (50 tasks, max score: 86) 33 -24 -24 0 -123 24 20
Run set ukojak.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-BitVectors