Tool ULTIMATE Automizer 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]
Date of execution 2017-12-02 01:06:24 CET 2017-12-03 03:07:09 CET 2017-12-03 03:49:57 CET 2017-12-03 03:57:59 CET 2017-12-03 04:29:07 CET 2017-12-02 23:12:02 CET 2017-12-03 03:11:19 CET
Run set uautomizer.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.ReachSafety-BitVectors
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.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/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.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/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/uautomizer.2017-12-02_0106.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 85   880 880 false(unreach-call) 1 wit inspect 6.1  270 false(unreach-call) 1 wit inspect 28     520   unknown 0 wit inspect 5.0  210 true -32 wit inspect .82   19    - wit inspect - wit inspect
bitvector/sum02_false-unreach-call_true-no-overflow.i unknown 0 wit inspect 14   380 140 error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .97 49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i timeout 0 wit inspect 900   1400 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .021 4.9
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i timeout 0 wit inspect 900   1400 10000 - 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/gcd_1_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   630 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .020 4.8
bitvector/gcd_2_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   670 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .020 4.9
bitvector/gcd_3_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   2800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .020 4.9
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 56   520 590 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3  310 true 2 wit inspect 43     560  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 170   3800 2500 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4  320 true 2 wit inspect 160     630  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 4.7 290 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  290 true 2 wit inspect 7.0   250  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 4.9 290 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  280 true 2 wit inspect 26     330  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 4.9 290 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  280 true 2 wit inspect 6.1   260  
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   700 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .019 4.9
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 20   310 230 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  280 true 2 wit inspect 7.5   260  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 4.9 290 38 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    550 true 2 wit inspect 41     300  
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect 14   410 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 15    330 true 2 wit inspect 14     320  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 270   3300 3300 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  290 true 2 wit inspect 51     610  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   1300 8800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .028 4.8
bitvector/parity_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   1000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .022 4.9
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   560 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .020 4.8
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 24   710 180 true -32 wit inspect 6.3  270 false(unreach-call) 1 wit inspect 17     450   unknown 0 wit inspect 5.2  230 true -32 wit inspect .66   20    - wit inspect - wit inspect
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 27   650 210 true -32 wit inspect 6.0  280 false(unreach-call) 1 wit inspect 21     490   unknown 0 wit inspect 4.4  220 true -32 wit inspect .86   20    - wit inspect - wit inspect
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 23   580 170 true -32 wit inspect 7.9  280 false(unreach-call) 1 wit inspect 20     390   unknown 0 wit inspect 5.2  240 true -32 wit inspect .76   20    - wit inspect - wit inspect
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 41   1300 380 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 77    830 true 2 wit inspect 40     760  
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 43   1900 360 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 17    450 true 2 wit inspect 46     940  
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 25   1000 190 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 15    410 out of memory 0 wit inspect 120     7000  
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   2100 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .021 5.0
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 53   2200 490 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    4800 true 2 wit inspect 47     1100  
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c true 2 wit inspect 40   1800 350 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 true 2 wit inspect 33     1100  
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c true 2 wit inspect 41   1800 350 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 true 2 wit inspect 32     1100  
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 40   1500 390 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5300 true 2 wit inspect 36     990  
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 39   1500 330 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5400 true 2 wit inspect 29     950  
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c error (7) 0 wit inspect 110   850 1200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .021 4.8
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 26   750 210 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6300 true 2 wit inspect 62     700  
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c timeout 0 wit inspect 900   890 9600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .022 4.9
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c error (7) 0 wit inspect 490   910 6400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .019 5.0
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 22   680 210 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6300 true 2 wit inspect 24     610  
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.0 240 58 false(unreach-call) 1 wit inspect 4.0  270 false(unreach-call) 1 wit inspect 9.5   220   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.0 240 39 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 3.1   220   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .80   18    - wit inspect - wit inspect
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.0 240 64 false(unreach-call) 1 wit inspect 3.2  250 false(unreach-call) 1 wit inspect 9.1   220   unknown 0 wit inspect 3.7  190 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 210   1300 2900 false(unreach-call) 1 wit inspect 5.2  280 true -32 wit inspect 6.3   260   unknown 0 wit inspect 4.2  220 true -32 wit inspect .74   19    - wit inspect - wit inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.0 230 36 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 4.3   220   unknown 0 wit inspect 3.4  190 false(unreach-call) 1 wit inspect .69   18    - wit inspect - wit inspect
bitvector-regression/signextension_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.1 240 36 false(unreach-call) 1 wit inspect 3.7  250 false(unreach-call) 1 wit inspect 5.3   220   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .70   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c true 2 wit inspect 4.5 270 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 4.8   250  
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true 2 wit inspect 8.7 280 67 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 10     270  
bitvector-regression/signextension2_true-unreach-call_true-termination.c true 2 wit inspect 4.5 280 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.6   260  
bitvector-regression/signextension_true-unreach-call_true-termination.c true 2 wit inspect 4.8 290 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.5   260  
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect 7.2 340 63 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 5.8   260   unknown 0 wit inspect 3.2  210 true -32 wit inspect .61   19    - wit inspect - wit inspect
bitvector-loops/overflow_false-unreach-call1.i timeout 0 wit inspect 900   710 12000 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .99 50 error (invalid witness file) 0 wit inspect .0015 .28 - wit inspect - wit inspect
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 470   780 5400 false(unreach-call) 1 wit inspect 4.4  280 out of memory 0 wit inspect 40     7000   unknown 0 wit inspect 3.2  210 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 58 13000 48000 160000 14 -87 59 3300 14 -22 170   10000 14 0 48 2600 14 -219 8.4 230 36 30 7400 42000 36 44 850 20000
    correct results 35 58 1800 31000 20000 9 9 37 2400 10 10 120   3200 0 5 5 3.4 92 15 30 170 5100 22 44 730 13000
        correct true 23 46 940 25000 10000 0 0 0 0 15 30 170 5100 22 44 730 13000
        correct false 12 12 880 6500 10000 9 9 37 2400 10 10 120   3200 0 5 5 3.4 92 0 0
    incorrect results 0 3 -96 20 830 1 -32 6.3 260 0 7 -224 5.0 140 0 0
        incorrect true 0 3 -96 20 830 1 -32 6.3 260 0 7 -224 5.0 140 0 0
        incorrect false 0 0 0 0 0 0 0
score (50 tasks, max score: 86) 58 -87 -22 0 -219 30 44
Run set uautomizer.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.ReachSafety-BitVectors