Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux 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* [apollon073; apollon077; apollon078; apollon119; apollon130] apollon* [apollon077; apollon078; apollon091; apollon114] 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]
Date of execution 2017-12-01 12:59:33 CET 2017-12-02 09:20:19 CET 2017-12-02 10:53:45 CET 2017-12-02 11:06:16 CET 2017-12-02 11:21:21 CET 2017-12-02 06:57:43 CET 2017-12-02 09:56:59 CET
Run set esbmc-kind.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-BitVectors
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.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/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.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/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/esbmc-kind.2017-12-01_1259.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 1.2   29 14    false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 33     530   unknown 0 wit inspect 3.6  220 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     780 11000    error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .16  27 1.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 10    290 timeout 0 wit inspect 960     1100  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .15  27 1.8  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.7  330 timeout 0 wit inspect 960     1100  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .38  27 4.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.1  300 timeout 0 wit inspect 960     650  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 37     44 420    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 170    460 timeout 0 wit inspect 960     820  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 37     45 460    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 170    470 timeout 0 wit inspect 960     3300  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .53  32 8.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4  310 true 2 wit inspect 56     560  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .12  26 1.2  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9  300 true 2 wit inspect 150     610  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     1300 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .017 4.8
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     840 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .020 4.8
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     780 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .018 4.9
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     11000 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .019 4.9
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     750 8900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .020 4.9
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     1000 9300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 5.0
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect 200     330 2200    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    320 true 2 wit inspect 42     330  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .13  26 .91 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  270 true 2 wit inspect 56     630  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .14  26 .98 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  290 timeout 0 wit inspect 960     1100  
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 9.4   33 130    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 23    340 timeout 0 wit inspect 960     1000  
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 .74 43 error (2) 0 wit inspect .018 4.9
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 4.0   76 42    false(unreach-call) 1 wit inspect 4.5  280 true -32 wit inspect 6.2   260   unknown 0 wit inspect 3.0  220 true -32 wit inspect .63   19    - wit inspect - wit inspect
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 7.4   110 79    false(unreach-call) 1 wit inspect 3.4  280 true -32 wit inspect 6.0   260   unknown 0 wit inspect 3.2  230 true -32 wit inspect .67   19    - wit inspect - wit inspect
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 2.3   51 23    false(unreach-call) 1 wit inspect 4.7  290 true -32 wit inspect 4.1   270   unknown 0 wit inspect 3.9  220 true -32 wit inspect .62   18    - wit inspect - wit inspect
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 25     210 240    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 75    890 true 2 wit inspect 42     760  
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 13     170 120    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 16    430 true 2 wit inspect 44     920  
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 12     160 160    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    510 true 2 wit inspect 33     810  
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     290 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .45 44 error (2) 0 wit inspect .021 5.0
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     2400 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .023 4.8
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout 0 wit inspect 900     2100 8500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .018 4.8
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout 0 wit inspect 900     2000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .022 4.9
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     1700 9600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .018 4.9
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.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 .66 43 error (2) 0 wit inspect .022 4.9
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect .35  28 4.4  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6500 true 2 wit inspect 120     780  
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect .37  29 3.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 true 2 wit inspect 58     700  
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 1 wit inspect .71  30 7.9  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6300 timeout 0 wit inspect 960     770  
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 1.8   29 21    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 230    550 error (7) 0 wit inspect 66     670  
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect .36  29 3.8  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6300 true 2 wit inspect 28     630  
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .082 28 .86 false(unreach-call) 1 wit inspect 2.0  260 false(unreach-call) 1 wit inspect 9.0   230   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .10  28 .91 false(unreach-call) 1 wit inspect 2.6  260 false(unreach-call) 1 wit inspect 5.2   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 .13  28 1.2  false(unreach-call) 1 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 6.2   230   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .74  28 11    timeout 0 wit inspect 91    1700 true -32 wit inspect 11     290   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  28 .64 false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 5.3   220   unknown 0 wit inspect 2.0  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
bitvector-regression/signextension_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .078 28 .85 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 4.3   220   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c true 2 wit inspect .071 26 .80 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  240 true 2 wit inspect 5.2   250  
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true 2 wit inspect .076 26 .87 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 9.3   240  
bitvector-regression/signextension2_true-unreach-call_true-termination.c true 2 wit inspect .078 26 .77 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 5.9   260  
bitvector-regression/signextension_true-unreach-call_true-termination.c true 2 wit inspect .097 26 .84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  240 true 2 wit inspect 6.6   250  
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect .60  28 4.8  false(unreach-call) 1 wit inspect 4.2  260 false(unreach-call) 1 wit inspect 6.6   260   unknown 0 wit inspect 2.2  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
bitvector-loops/overflow_false-unreach-call1.i timeout 0 wit inspect 900     11000 12000    error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .65 48 error (invalid witness file) 0 wit inspect .0020 .26 - wit inspect - wit inspect
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 2.1   29 20    true -32 wit inspect 3.8  260 timeout 0 wit inspect 98     6000   unknown 0 wit inspect 2.3  220 true -32 wit inspect .58   19    - 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 56 14000    40000 160000   14 -22 130   4700 14 -121 200 9000 14 0 33 2600 14 -120 7.2 220 36 38 4400 33000 36 28 8400 18000
    correct results 33 55 350    1900 4000   10 10 34   2700 7 7 70 1900 0 8 8 4.7 150 19 38 770 7100 14 28 650 7700
        correct true 22 44 340    1400 3800   0 0 0 0 19 38 770 7100 14 28 650 7700
        correct false 11 11 17    460 180   10 10 34   2700 7 7 70 1900 0 8 8 4.7 150 0 0
    correct-unconfimed results 2 1 2.8  60 28   0 0 0 0 0 0
        correct-unconfirmed true 1 1 .71 30 7.9 0 0 0 0 0 0
        correct-unconfirmed false 1 0 2.1  29 20   0 0 0 0 0 0
    incorrect results 0 1 -32 3.8 260 4 -128 27 1100 0 4 -128 2.5 74 0 0
        incorrect true 0 1 -32 3.8 260 4 -128 27 1100 0 4 -128 2.5 74 0 0
        incorrect false 0 0 0 0 0 0 0
score (50 tasks, max score: 86) 56 -22 -121 0 -120 38 28
Run set esbmc-kind.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-BitVectors