Tool CPAchecker 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-05 07:52:24 CET 2017-12-05 13:10:09 CET 2017-12-05 13:34:02 CET 2017-12-05 13:37:41 CET 2017-12-05 13:41:35 CET 2017-12-05 12:37:13 CET 2017-12-05 13:13:01 CET
Run set interpchecker.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-BitVectors
Options -sv-comp18-interpcpachecker -heap 10000M -disable-java-assertions -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.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/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.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/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/interpchecker.2017-12-05_0752.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) 0 wit inspect 7.1 400 47 true -32 wit inspect 3.6 260 timeout 0 wit inspect 96   760 unknown 0 wit inspect 3.2  210 true -32 wit inspect .66  19   - wit inspect - wit inspect
bitvector/sum02_false-unreach-call_true-no-overflow.i false(unreach-call) 0 wit inspect 3.5 270 34 timeout 0 wit inspect 92   2000 unknown 0 wit inspect 13   390 unknown 0 wit inspect 2.7  210 true -32 wit inspect .58  18   - wit inspect - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i false(unreach-call) -16 wit inspect 9.4 460 78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 timeout 0 wit inspect 960     1200  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i false(unreach-call) -16 wit inspect 9.1 460 84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  280 timeout 0 wit inspect 960     1300  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   2400 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .018 4.9
bitvector/gcd_2_true-unreach-call_true-no-overflow.i false(unreach-call) -16 wit inspect 4.5 290 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.2  290 true 2 wit inspect 4.9   260  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i false(unreach-call) -16 wit inspect 3.4 260 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 220    310 true 2 wit inspect 4.7   260  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i false(unreach-call) -16 wit inspect 8.6 460 69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  270 true 2 wit inspect 30     590  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i false(unreach-call) -16 wit inspect 7.8 440 64 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  260 out of memory 0 wit inspect 54     7000  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 2.9 280 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    7000 true 2 wit inspect 7.5   280  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 3.1 280 31 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    7000 true 2 wit inspect 5.0   260  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900   5500 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .021 4.8
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   4300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .047 4.8
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900   5500 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .021 4.8
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900   5700 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .019 5.0
bitvector/modulus_true-unreach-call_true-no-overflow.i false(unreach-call) -16 wit inspect 3.0 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  260 true 2 wit inspect 10     330  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i false(unreach-call) -16 wit inspect 5.6 310 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  260 true 2 wit inspect 21     490  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i false(unreach-call) -16 wit inspect 5.8 310 51 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 timeout 0 wit inspect 960     1300  
bitvector/parity_true-unreach-call_true-no-overflow.i false(unreach-call) -16 wit inspect 2.9 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 true 2 wit inspect 13     310  
bitvector/sum02_true-unreach-call_true-no-overflow.i false(unreach-call) -16 wit inspect 3.8 280 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  260 timeout 0 wit inspect 960     530  
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 86   3900 850 false(unreach-call) 1 wit inspect 15   450 false(unreach-call) 1 wit inspect 25   540 unknown 0 wit inspect 3.8  220 error (1) 0 wit inspect .61  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 63   3700 660 timeout 0 wit inspect 92   2100 false(unreach-call) 1 wit inspect 25   540 unknown 0 wit inspect 4.1  220 error (1) 0 wit inspect .57  20   - wit inspect - wit inspect
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 0 wit inspect 7.4 450 54 true -32 wit inspect 3.6 260 true -32 wit inspect 17   360 unknown 0 wit inspect 4.0  220 true -32 wit inspect .65  19   - wit inspect - wit inspect
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) -16 wit inspect 86   3900 810 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    680 true 2 wit inspect 26     570  
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) -16 wit inspect 65   3100 620 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 true 2 wit inspect 31     550  
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 88   3800 1000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 15    400 true 2 wit inspect 19     800  
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   4400 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.8
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 40   2400 350 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 true 2 wit inspect 47     1000  
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c true 2 wit inspect 120   3500 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 true 2 wit inspect 32     920  
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c true 2 wit inspect 120   3300 1600 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 true 2 wit inspect 33     1000  
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 110   3200 1300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5200 true 2 wit inspect 40     940  
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 66   3000 650 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 true 2 wit inspect 37     950  
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c false(unreach-call) -16 wit inspect 13   630 100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 9.5   310  
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c false(unreach-call) -16 wit inspect 8.1 450 62 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 9.3   330  
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c false(unreach-call) -16 wit inspect 10   450 71 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 true 2 wit inspect 12     340  
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c timeout 0 wit inspect 900   3100 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 46 error (2) 0 wit inspect .050 5.0
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c false(unreach-call) -16 wit inspect 13   590 100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 8.6   310  
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.9 280 25 false(unreach-call) 1 wit inspect 2.9 250 false(unreach-call) 1 wit inspect 8.3 230 unknown 0 wit inspect 2.6  210 false(unreach-call) 1 wit inspect .57  18   - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c true -32 wit inspect 2.7 270 27 false(unreach-call) 1 wit inspect 3.2 250 false(unreach-call) 1 wit inspect 4.6 220 unknown 0 wit inspect .86 50 error (1) 0 wit inspect .070 9.0 - wit inspect - wit inspect
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.0 280 24 false(unreach-call) 1 wit inspect 2.9 250 false(unreach-call) 1 wit inspect 8.3 230 unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .56  18   - wit inspect - wit inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 3.0 280 26 true -32 wit inspect 3.3 260 true -32 wit inspect 17   420 unknown 0 wit inspect 2.6  180 true -32 wit inspect .57  18   - wit inspect - wit inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c true -32 wit inspect 2.9 280 26 false(unreach-call) 1 wit inspect 3.3 250 false(unreach-call) 1 wit inspect 4.3 220 unknown 0 wit inspect .90 53 error (1) 0 wit inspect .098 9.0 - wit inspect - wit inspect
bitvector-regression/signextension_false-unreach-call_true-termination.c true -32 wit inspect 2.8 280 23 false(unreach-call) 1 wit inspect 3.4 250 false(unreach-call) 1 wit inspect 4.5 220 unknown 0 wit inspect .88 50 error (1) 0 wit inspect .097 8.9 - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.9 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 4.5   250  
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.1 270 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 8.9   230  
bitvector-regression/signextension2_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.0 280 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 4.1   210  
bitvector-regression/signextension_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.8 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  260 true 2 wit inspect 4.4   220  
bitvector-loops/diamond_false-unreach-call2.i true -32 wit inspect 31   2100 230 unknown 0 wit inspect 4.8 280 false(unreach-call) 1 wit inspect 9.0 330 unknown 0 wit inspect .89 53 error (1) 0 wit inspect .075 9.1 - wit inspect - wit inspect
bitvector-loops/overflow_false-unreach-call1.i true -32 wit inspect 2.8 280 25 timeout 0 wit inspect 92   1500 timeout 0 wit inspect 96   540 unknown 0 wit inspect .88 50 error (1) 0 wit inspect .065 9.0 - wit inspect - wit inspect
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i true -32 wit inspect 7.7 450 60 unknown 0 wit inspect 12   370 timeout 0 wit inspect 97   590 unknown 0 wit inspect .88 51 error (1) 0 wit inspect .097 8.9 - 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 -508 7400 78000 90000 14 -90 330 8800 14 -56 430 5600 14 0 31 2000 14 -126 5.3 200 36 40 7400 47000 36 48 4300 23000
    correct results 12 20 710 28000 7800 6 6 31 1700 8 8 89 2500 0 2 2 1.1 37 20 40 310 5400 24 48 420 12000
        correct true 8 16 550 20000 6200 0 0 0 0 20 40 310 5400 24 48 420 12000
        correct false 4 4 160 8200 1600 6 6 31 1700 8 8 89 2500 0 2 2 1.1 37 0 0
    correct-unconfimed results 4 0 21 1400 160 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 4 0 21 1400 160 0 0 0 0 0 0
    incorrect results 27 -528 320 18000 2800 3 -96 10 780 2 -64 33 780 0 4 -128 2.5 74 0 0
        incorrect true 6 -192 50 3700 390 3 -96 10 780 2 -64 33 780 0 4 -128 2.5 74 0 0
        incorrect false 21 -336 270 14000 2400 0 0 0 0 0 0
score (50 tasks, max score: 86) -508 -90 -56 0 -126 40 48
Run set interpchecker.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-BitVectors