Tool CPAchecker 1.6.1-svn 26758M 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-11-30 11:20:26 CET 2017-12-01 07:36:48 CET 2017-12-01 08:27:40 CET 2017-12-01 08:32:13 CET 2017-12-01 08:39:14 CET 2017-12-01 04:24:39 CET 2017-12-01 07:43:13 CET
Run set cpa-bam-slicing.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-BitVectors
Options -ldv-bam-svcomp -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.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/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.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/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-slicing.2017-11-30_1120.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 0 12   500 89 0 .58 44 0 .019 5.0 0 .86 49 0 .0014 .26 - -
bitvector/sum02_false-unreach-call_true-no-overflow.i 0 3.3 290 30 0 .57 45 0 .019 4.9 0 .87 47 0 .0015 .26 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i 0 12   530 88 - - - - 0 .56 42 0 .019 5.0
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i 0 12   500 95 - - - - 0 .72 46 0 .019 4.9
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 0 5.3 310 56 - - - - 0 .58 44 0 .019 4.9
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 2 3.7 280 37 - - - - 2 180    470 0 960     720  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 0 3.5 300 35 - - - - 0 .56 43 0 .019 4.8
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i 2 3.2 270 27 - - - - 2 6.5  300 2 40     580  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 0 3.5 290 34 - - - - 0 .40 44 0 .022 4.9
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i 2 2.9 270 24 - - - - 0 910    5400 2 5.9   260  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i 2 3.1 270 28 - - - - 0 890    7000 2 5.2   260  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i 2 3.1 270 29 - - - - 0 700    7000 2 6.8   260  
bitvector/jain_5_true-unreach-call_true-no-overflow.i 0 900   3900 11000 - - - - 0 .55 44 0 .023 4.8
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i 2 3.2 270 29 - - - - 0 620    7000 2 21     280  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i 2 3.1 270 27 - - - - 0 870    7000 2 6.0   260  
bitvector/modulus_true-unreach-call_true-no-overflow.i 0 3.9 300 34 - - - - 0 .51 42 0 .023 4.9
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 2 3.1 270 29 - - - - 2 5.3  270 2 57     610  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 0 3.4 290 35 - - - - 0 .53 43 0 .020 4.8
bitvector/parity_true-unreach-call_true-no-overflow.i 0 3.0 280 27 - - - - 0 .67 42 0 .021 4.9
bitvector/sum02_true-unreach-call_true-no-overflow.i 0 3.2 290 29 - - - - 0 .63 43 0 .021 4.8
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c 1 21   750 160 -32 5.3  260 1 16     440   0 3.8  230 -32 .67   20    - -
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c 1 23   1000 160 -32 5.2  270 1 19     520   0 4.2  230 -32 .65   20    - -
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c 1 7.8 460 72 -32 5.0  270 1 19     430   0 3.8  220 -32 .67   19    - -
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c 0 21   720 130 - - - - 0 .69 43 0 .025 4.8
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c 2 36   1700 270 - - - - 2 15    560 2 50     940  
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c 2 23   890 150 - - - - 2 16    400 2 37     820  
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900   5200 10000 - - - - 0 .57 43 0 .021 5.0
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c 2 41   1800 330 - - - - 0 900    4700 2 58     1000  
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c 2 20   790 150 - - - - 0 900    4200 2 43     880  
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c 2 20   790 160 - - - - 0 900    4100 2 32     1100  
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 2 43   1700 310 - - - - 0 910    5300 2 37     990  
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c 2 42   2000 280 - - - - 0 910    5300 2 42     910  
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c 0 3.7 290 37 - - - - 0 .54 44 0 .024 4.8
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c 0 7.4 400 59 - - - - 0 .55 41 0 .018 4.8
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c 0 7.0 490 56 - - - - 0 .52 41 0 .022 4.9
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c 0 3.4 290 31 - - - - 0 .40 43 0 .023 4.9
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c 0 6.6 360 52 - - - - 0 .56 41 0 .023 4.8
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c 1 3.0 280 24 -32 3.8  270 1 8.7   220   0 2.7  180 1 .68   18    - -
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c -32 2.8 270 25 1 3.7  260 1 4.2   210   0 .94 51 0 .069  9.1  - -
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c 1 2.9 270 27 -32 3.0  250 1 9.1   230   0 2.8  180 1 .59   18    - -
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c 0 3.2 280 31 -32 3.2  260 -32 4.4   220   0 2.7  180 -32 .61   18    - -
bitvector-regression/signextension2_false-unreach-call_true-termination.c -32 2.7 270 25 1 3.6  250 1 4.4   220   0 1.1  52 0 .068  9.1  - -
bitvector-regression/signextension_false-unreach-call_true-termination.c -32 2.9 270 25 1 3.5  250 1 4.8   220   0 .95 51 0 .069  9.0  - -
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c 2 2.6 260 25 - - - - 2 2.9  250 2 4.7   240  
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c 2 2.8 270 25 - - - - 2 2.8  240 2 12     240  
bitvector-regression/signextension2_true-unreach-call_true-termination.c 2 2.7 270 23 - - - - 2 3.4  250 2 5.1   260  
bitvector-regression/signextension_true-unreach-call_true-termination.c 2 2.8 270 29 - - - - 2 3.5  260 2 5.9   260  
bitvector-loops/diamond_false-unreach-call2.i -32 14   600 100 0 4.9  280 1 9.3   330   0 .92 51 0 .068  9.0  - -
bitvector-loops/overflow_false-unreach-call1.i -32 3.3 270 33 0 92    1600 0 96     560   0 .92 51 0 .078  9.0  - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i -32 3.2 270 28 0 13    480 0 97     550   0 .93 51 0 .065  9.0  - -
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 -149 2300   33000 24000 14 -189 150 4800 14 -23 290   4200 14 0 27 1600 14 -126 4.3 170 36 18 8800 61000 36 36 1400 11000
    correct results 24 43 320   16000 2400 3 3 11 760 9 9 94   2800 0 2 2 1.3 37 9 18 240 3000 18 36 470 10000
        correct true 19 38 260   13000 2000 0 0 0 0 9 18 240 3000 18 36 470 10000
        correct false 5 5 58   2800 440 3 3 11 760 9 9 94   2800 0 2 2 1.3 37 0 0
    correct-unconfimed results 1 0 3.2 280 31 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 1 0 3.2 280 31 0 0 0 0 0 0
    incorrect results 6 -192 29   2000 240 6 -192 25 1600 1 -32 4.4 220 0 4 -128 2.6 78 0 0
        incorrect true 6 -192 29   2000 240 6 -192 25 1600 1 -32 4.4 220 0 4 -128 2.6 78 0 0
        incorrect false 0 0 0 0 0 0 0
score (50 tasks, max score: 86) -149 -189 -23 0 -126 18 36
Run set cpa-bam-slicing.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-BitVectors