Tool CBMC
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-22-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-03 00:42:25 CET [[ 2016-01-15 08:22:02 CET ]] [[ 2016-01-15 21:54:19 CET ]]
Run set sv-comp16.BitVectorsOverflows
Options --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/signedintegeroverflow-regression/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime wit1_walltime wit1_memUsage (MB) wit2_status wit2_cputime wit2_walltime wit2_memUsage (MB)
AdditionIntMax_false-no-overflow.c.i false(reach) .16 .17 26 wit - -
Multiplication_false-no-overflow.c.i false(reach) .12 .13 26 wit - -
NoConversion_false-no-overflow.c.i false(reach) .10 .11 26 wit - -
PostfixDecrement_false-no-overflow.c.i false(reach) .12 .13 25 wit - -
PostfixIncrement_false-no-overflow.c.i false(reach) .16 .18 26 wit - -
PrefixDecrement_false-no-overflow.c.i false(reach) .13 .14 26 wit - -
PrefixIncrement_false-no-overflow.c.i false(reach) .12 .13 26 wit - -
UnaryMinus_false-no-overflow.c.i false(reach) .10 .11 26 wit - -
ConversionToSignedInt_true-no-overflow.c.i false(reach) .13 .14 26 wit - -
IntegerPromotion_true-no-overflow.c.i true 1.2  1.2  26 wit - -
Multiplication_true-no-overflow.c.i true 1.2  1.2  26 wit - -
UsualArithmeticConversions_true-no-overflow.c.i true 1.1  1.1  26 wit - -
../../sv-benchmarks/c/signedintegeroverflow-regression/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime wit1_walltime wit1_memUsage (MB) wit2_status wit2_cputime wit2_walltime wit2_memUsage (MB)
total tasks 12 4.6 4.7 310 12 0   12 0  
    correct results 3 3.4 3.5 77 0 0   0 0  
        correct true 3 3.4 3.5 77 0 0   0 0  
        correct false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (12 tasks, max score: 16) 6
Run set sv-comp16.BitVectorsOverflows