Tool SMACK+Corral 1.5.2
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-07 09:05:16 CET [[ 2016-01-15 09:34:34 CET ]] [[ 2016-01-15 22:36:10 CET ]]
Run set sv-comp16.BitVectorsReach
Options -w error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/smack.2016-01-07_0905.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/smack.2016-01-07_0905.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 false(reach) 6.8 6.7 140 wit true 6.9 3.9 270 false(reach) 69 42   560
bitvector/byte_add_1_true-unreach-call.i true 23   22   160 wit - -
bitvector/byte_add_2_true-unreach-call.i true 24   24   160 wit - -
bitvector/gcd_1_true-unreach-call.i true 2.9 2.9 73 wit - -
bitvector/gcd_2_true-unreach-call.i true 2.9 2.9 71 wit - -
bitvector/gcd_3_true-unreach-call.i true 2.8 2.8 70 wit - -
bitvector/gcd_4_true-unreach-call.i true 3.4 3.4 75 wit - -
bitvector/interleave_bits_true-unreach-call.i true 2.2 2.3 73 wit - -
bitvector/jain_1_true-unreach-call.i true 880   880   110 wit - -
bitvector/jain_2_true-unreach-call.i true 880   880   100 wit - -
bitvector/jain_4_true-unreach-call.i timeout 880   930   140 wit - -
bitvector/jain_5_true-unreach-call.i timeout 900   900   700 wit - -
bitvector/jain_6_true-unreach-call.i timeout 880   930   110 wit - -
bitvector/jain_7_true-unreach-call.i timeout 880   930   94 wit - -
bitvector/modulus_true-unreach-call.i true 47   47   160 wit - -
bitvector/num_conversion_1_true-unreach-call.i true 2.6 2.6 64 wit - -
bitvector/num_conversion_2_true-unreach-call.i true 2.6 2.6 67 wit - -
bitvector/parity_true-unreach-call.i true 880   880   290 wit - -
bitvector/sum02_true-unreach-call.i true 880   880   390 wit - -
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c witness timeout 17   17   210 wit timeout 91   69   3700 true 14 7.8 350
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c witness timeout 40   39   240 wit timeout 91   68   2800 true 15 11   350
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c witness timeout 11   11   180 wit timeout 91   69   3000 true 15 12   340
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c true 210   210   320 wit - -
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c true 170   170   290 wit - -
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c true 180   180   300 wit - -
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c true 880   880   430 wit - -
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c true 880   880   530 wit - -
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c true 880   880   520 wit - -
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c true 880   880   560 wit - -
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c true 880   880   650 wit - -
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c true 880   880   610 wit - -
bitvector/soft_float_1_true-unreach-call.c.cil.c true 3.4 3.4 88 wit - -
bitvector/soft_float_2_true-unreach-call.c.cil.c true 3.2 3.2 87 wit - -
bitvector/soft_float_3_true-unreach-call.c.cil.c true 21   21   130 wit - -
bitvector/soft_float_4_true-unreach-call.c.cil.c true 12   12   88 wit - -
bitvector/soft_float_5_true-unreach-call.c.cil.c true 2.7 2.7 87 wit - -
bitvector-regression/implicitfloatconversion_false-unreach-call.i false(reach) 2.9 2.9 68 wit false(reach) 4.6 2.7 220 error 11 6.1 320
bitvector-regression/implicitunsignedconversion_false-unreach-call.i false(reach) 2.8 2.8 72 wit false(reach) 4.4 2.6 220 false(reach) 11 7.0 320
bitvector-regression/integerpromotion_false-unreach-call.i false(reach) 3.0 3.0 72 wit false(reach) 7.0 3.9 340 false(reach) 22 14   390
bitvector-regression/signextension2_false-unreach-call.i false(reach) 3.1 3.1 70 wit false(reach) 7.1 4.0 330 false(reach) 12 7.9 350
bitvector-regression/signextension_false-unreach-call.i false(reach) 3.0 2.9 74 wit false(reach) 7.3 4.1 330 false(reach) 11 6.5 330
bitvector-regression/implicitunsignedconversion_true-unreach-call.i true 2.5 2.5 61 wit - -
bitvector-regression/integerpromotion_true-unreach-call.i true 2.0 2.0 65 wit - -
bitvector-regression/signextension2_true-unreach-call.i true 2.7 2.8 67 wit - -
bitvector-regression/signextension_true-unreach-call.i true 2.8 2.8 67 wit - -
bitvector-loops/diamond_false-unreach-call2.i false(reach) 3.6 3.6 85 wit true 15   8.3 400 false(reach) 13 8.5 340
bitvector-loops/overflow_false-unreach-call1.i error (1) 890   890   830 wit - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i witness unconfirmed 7.0 6.9 93 wit true 5.4 3.1 230 true 20 12   410
../../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 14000 14000 10000 48 330   240   12000   48 210   130   4000  
    correct results 39 9600 9600 7400 7 53   30   2100   6 150   92   2600  
        correct true 32 9600 9500 6800 2 0   0   0   0 0   0   0  
        correct false 7 25 25 580 5 53   30   2100   6 150   92   2600  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 84) 71
Run set sv-comp16.BitVectorsReach