Tool symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 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* [apollon005; apollon043; apollon077; apollon078; apollon087; apollon118] [apollon061; apollon077; apollon078; apollon086; apollon134] [apollon038; apollon077; apollon078; apollon083] [apollon077; apollon078; apollon161] 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 22:41:19 CET 2017-12-02 21:10:50 CET 2017-12-02 22:39:24 CET 2017-12-02 22:51:52 CET 2017-12-02 23:01:21 CET 2017-12-02 19:44:15 CET 2017-12-02 21:36:25 CET
Run set symbiotic.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-BitVectors
Options --witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.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/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.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/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/symbiotic.2017-12-01_2241.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 12 4.0 false(unreach-call) 1 wit inspect 3.0  270 true -32 wit inspect 5.2   250   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout (timeout) 0 wit inspect 900    790 13000   error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0037 .28 - wit inspect - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .32 12 3.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8  290 timeout 0 wit inspect 960     1100  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .35 12 4.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  340 timeout 0 wit inspect 960     1000  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .42 12 5.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    300 timeout 0 wit inspect 960     640  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 9.8  15 130   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 150    460 timeout 0 wit inspect 960     600  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 9.4  15 120   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 170    460 timeout 0 wit inspect 960     2400  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .17 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6  300 true 2 wit inspect 41     560  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .16 12 2.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.2  310 true 2 wit inspect 150     620  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i timeout (timeout) 0 wit inspect 900    75 8700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .023 4.9
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i timeout (timeout) 0 wit inspect 900    94 8500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .020 4.9
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i timeout (timeout) 0 wit inspect 900    15000 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .018 4.9
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout (timeout) 0 wit inspect 900    15000 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .023 4.8
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i timeout (timeout) 0 wit inspect 900    15000 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.8
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i timeout (timeout) 0 wit inspect 900    15000 14000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.8
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect 640    57 8600   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    320 true 2 wit inspect 18     340  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .17 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  270 true 2 wit inspect 54     640  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .17 12 2.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  270 timeout 0 wit inspect 960     1100  
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.4  13 99   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 23    320 timeout 0 wit inspect 960     1000  
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout (timeout) 0 wit inspect 900    770 9900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .035 4.8
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect .42 13 4.7 false(unreach-call) 1 wit inspect 13    360 true -32 wit inspect 4.2   260   unknown 0 wit inspect 3.6  210 true -32 wit inspect .62   18    - wit inspect - wit inspect
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect .61 14 8.0 false(unreach-call) 1 wit inspect 34    380 true -32 wit inspect 5.6   250   unknown 0 wit inspect 3.5  210 true -32 wit inspect .62   18    - wit inspect - wit inspect
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect .28 12 3.5 false(unreach-call) 1 wit inspect 5.1  420 true -32 wit inspect 4.1   270   unknown 0 wit inspect 3.5  210 true -32 wit inspect .66   18    - wit inspect - wit inspect
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect .59 13 7.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 66    890 true 2 wit inspect 38     790  
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect .62 13 6.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 19    450 true 2 wit inspect 40     880  
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect .62 13 6.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    520 true 2 wit inspect 32     800  
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout (timeout) 0 wit inspect 900    400 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .048 4.9
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c timeout (timeout) 0 wit inspect 900    1100 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .021 4.8
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout (timeout) 0 wit inspect 900    130 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .42 44 error (2) 0 wit inspect .023 5.0
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout (timeout) 0 wit inspect 900    220 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.9
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout (timeout) 0 wit inspect 900    210 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .020 4.8
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c timeout (timeout) 0 wit inspect 900    210 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .022 4.8
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 680    160 9200   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 true 2 wit inspect 120     750  
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 2.8  15 38   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6300 true 2 wit inspect 57     710  
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 1 wit inspect 4.7  18 62   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6300 timeout 0 wit inspect 960     750  
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c timeout (timeout) 0 wit inspect 900    45 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .024 4.9
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 2.7  16 35   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6300 true 2 wit inspect 25     610  
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14 11 1.6 false(unreach-call) 1 wit inspect 2.9  280 false(unreach-call) 1 wit inspect 8.9   240   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .16 11 1.7 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.6   220   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14 11 1.4 false(unreach-call) 1 wit inspect 4.2  260 false(unreach-call) 1 wit inspect 6.0   240   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c timeout (timeout) 0 wit inspect 900    2500 11000   error (invalid witness file) 0 wit inspect .42 44 error (2) 0 wit inspect .048 4.9 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .13 11 1.7 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 3.0   210   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
bitvector-regression/signextension_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .16 11 1.5 false(unreach-call) 1 wit inspect 2.2  250 false(unreach-call) 1 wit inspect 3.1   220   unknown 0 wit inspect 2.0  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 .12 11 1.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.0  250 true 2 wit inspect 4.9   250  
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true 2 wit inspect .15 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 12     240  
bitvector-regression/signextension2_true-unreach-call_true-termination.c true 2 wit inspect .12 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 5.2   260  
bitvector-regression/signextension_true-unreach-call_true-termination.c true 2 wit inspect .15 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.6   260  
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect .16 11 2.0 false(unreach-call) 1 wit inspect 2.3  260 true -32 wit inspect 4.9   230   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
bitvector-loops/overflow_false-unreach-call1.i false(unreach-call) 1 wit inspect .16 11 1.6 timeout 0 wit inspect 92    1600 true -32 wit inspect 3.5   260   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect 3.9    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 .41 13 5.3 timeout 0 wit inspect 91    830 true -32 wit inspect 3.5   240   unknown 0 wit inspect 2.0  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 54 16000    67000 200000   14 10 260 5500 14 -219 57 2900 14 0 33 2500 14 -120 10   220 36 36 4200 32000 36 28 8300 16000
    correct results 32 53 1400    590 18000   10 10 74 3000 5 5 26 1100 0 8 8 8.0 150 18 36 510 6500 14 28 610 7700
        correct true 21 42 1400    460 18000   0 0 0 0 18 36 510 6500 14 28 610 7700
        correct false 11 11 2.7  130 32   10 10 74 3000 5 5 26 1100 0 8 8 8.0 150 0 0
    correct-unconfimed results 2 1 5.1  31 67   0 0 0 0 0 0
        correct-unconfirmed true 1 1 4.7  18 62   0 0 0 0 0 0
        correct-unconfirmed false 1 0 .41 13 5.3 0 0 0 0 0 0
    incorrect results 0 0 7 -224 31 1800 0 4 -128 2.5 74 0 0
        incorrect true 0 0 7 -224 31 1800 0 4 -128 2.5 74 0 0
        incorrect false 0 0 0 0 0 0 0
score (50 tasks, max score: 86) 54 10 -219 0 -120 36 28
Run set symbiotic.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-BitVectors