Tool ULTIMATE Kojak fd30d3d8
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-23-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-08 15:10:30 CET [[ 2016-01-15 09:49:48 CET ]] [[ 2016-01-15 22:43:29 CET ]]
Run set sv-comp16.BitVectorsReach
Options [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
bitvector/byte_add_false-unreach-call.i timeout 46   930   720 wit - -
bitvector/byte_add_1_true-unreach-call.i timeout 34   930   540 wit - -
bitvector/byte_add_2_true-unreach-call.i timeout 31   930   430 wit - -
bitvector/gcd_1_true-unreach-call.i error 8.4 2.7 320 wit - -
bitvector/gcd_2_true-unreach-call.i error 10   2.9 350 wit - -
bitvector/gcd_3_true-unreach-call.i error 8.6 2.6 320 wit - -
bitvector/gcd_4_true-unreach-call.i error 9.5 2.9 330 wit - -
bitvector/interleave_bits_true-unreach-call.i true 38   17   520 wit - -
bitvector/jain_1_true-unreach-call.i true 8.2 2.7 320 wit - -
bitvector/jain_2_true-unreach-call.i true 9.4 3.0 320 wit - -
bitvector/jain_4_true-unreach-call.i true 10   3.4 320 wit - -
bitvector/jain_5_true-unreach-call.i timeout 62   930   1200 wit - -
bitvector/jain_6_true-unreach-call.i true 9.1 2.9 320 wit - -
bitvector/jain_7_true-unreach-call.i true 9.4 3.0 340 wit - -
bitvector/modulus_true-unreach-call.i error 67   54   380 wit - -
bitvector/num_conversion_1_true-unreach-call.i true 55   39   390 wit - -
bitvector/num_conversion_2_true-unreach-call.i timeout 270   930   870 wit - -
bitvector/parity_true-unreach-call.i timeout 43   930   360 wit - -
bitvector/sum02_true-unreach-call.i error 33   27   320 wit - -
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c timeout 30   930   490 wit - -
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c timeout 30   930   500 wit - -
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c timeout 45   930   560 wit - -
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c timeout 28   930   500 wit - -
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c timeout 28   930   480 wit - -
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c timeout 31   930   500 wit - -
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c timeout 580   930   940 wit - -
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c timeout 60   930   1000 wit - -
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c timeout 53   930   1000 wit - -
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c timeout 56   930   860 wit - -
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c timeout 53   930   520 wit - -
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c timeout 53   930   540 wit - -
bitvector/soft_float_1_true-unreach-call.c.cil.c timeout 38   930   590 wit - -
bitvector/soft_float_2_true-unreach-call.c.cil.c timeout 41   930   660 wit - -
bitvector/soft_float_3_true-unreach-call.c.cil.c timeout 42   930   660 wit - -
bitvector/soft_float_4_true-unreach-call.c.cil.c timeout 36   930   640 wit - -
bitvector/soft_float_5_true-unreach-call.c.cil.c timeout 42   930   610 wit - -
bitvector-regression/implicitfloatconversion_false-unreach-call.i error 7.9 2.4 310 wit - -
bitvector-regression/implicitunsignedconversion_false-unreach-call.i false(reach) 8.5 2.7 320 wit false(reach) 4.3 2.6 220 false(reach) 11 6.4 330
bitvector-regression/integerpromotion_false-unreach-call.i false(reach) 15   4.8 350 wit false(reach) 7.1 4.2 330 false(reach) 19 11   390
bitvector-regression/signextension2_false-unreach-call.i false(reach) 8.7 2.7 320 wit false(reach) 7.3 4.1 330 false(reach) 11 6.3 320
bitvector-regression/signextension_false-unreach-call.i false(reach) 11   2.9 360 wit false(reach) 7.4 4.2 330 false(reach) 12 6.7 340
bitvector-regression/implicitunsignedconversion_true-unreach-call.i timeout 130   930   1100 wit - -
bitvector-regression/integerpromotion_true-unreach-call.i timeout 150   930   1100 wit - -
bitvector-regression/signextension2_true-unreach-call.i timeout 130   930   1300 wit - -
bitvector-regression/signextension_true-unreach-call.i timeout 140   930   1100 wit - -
bitvector-loops/diamond_false-unreach-call2.i false(reach) 9.5 3.0 320 wit false(reach) 5.7 3.3 250 false(reach) 12 8.0 340
bitvector-loops/overflow_false-unreach-call1.i timeout 42   930   630 wit - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i timeout 900   870   520 wit - -
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
total tasks 48 3600 27000 27000 48 32   18   1500   48 64   39   1700  
    correct results 12 190 87 4200 5 32   18   1500   5 64   39   1700  
        correct true 7 140 71 2500 0 0   0   0   0 0   0   0  
        correct false 5 53 16 1700 5 32   18   1500   5 64   39   1700  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 84) 19
Run set sv-comp16.BitVectorsReach