Tool | ESBMC ESBMC version 2.0.0 64-bit x86_64 linux | ||||||||||||
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-16 17:45:19 CET [[ 2016-01-17 00:36:28 CET ]] [[ 2016-01-17 00:39:38 CET ]] | ||||||||||||
Run set | sv-comp16.BitVectorsOverflows | ||||||||||||
Options | [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmc.2016-01-16_1745.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 (s) | wit1_walltime (s) | wit1_memUsage (MB) | wit2_status | wit2_cputime (s) | wit2_walltime (s) | wit2_memUsage (MB) |
AdditionIntMax_false-no-overflow.c.i | false(no-overflow) | .10 | .12 | 17 | wit | false(no-overflow) | 6.1 | 3.6 | 220 | true | 10 | 5.9 | 320 |
Multiplication_false-no-overflow.c.i | false(no-overflow) | .095 | .11 | 17 | wit | false(no-overflow) | 6.3 | 3.7 | 220 | true | 9.4 | 5.3 | 330 |
NoConversion_false-no-overflow.c.i | false(no-overflow) | .10 | .12 | 17 | wit | false(no-overflow) | 6.4 | 3.6 | 220 | true | 11 | 7.9 | 310 |
PostfixDecrement_false-no-overflow.c.i | false(no-overflow) | .15 | .16 | 17 | wit | false(no-overflow) | 6.2 | 3.6 | 230 | true | 10 | 7.1 | 320 |
PostfixIncrement_false-no-overflow.c.i | false(no-overflow) | .46 | .60 | 17 | wit | false(no-overflow) | 6.3 | 3.5 | 220 | true | 11 | 7.9 | 350 |
PrefixDecrement_false-no-overflow.c.i | false(no-overflow) | .093 | .10 | 17 | wit | false(no-overflow) | 6.0 | 3.4 | 230 | true | 11 | 6.4 | 320 |
PrefixIncrement_false-no-overflow.c.i | false(no-overflow) | .66 | .88 | 17 | wit | false(no-overflow) | 6.1 | 3.7 | 220 | true | 10 | 6.2 | 320 |
UnaryMinus_false-no-overflow.c.i | false(no-overflow) | .44 | .59 | 17 | wit | false(no-overflow) | 6.3 | 3.6 | 230 | true | 10 | 5.5 | 330 |
ConversionToSignedInt_true-no-overflow.c.i | true | .12 | .13 | 17 | wit | - | - | ||||||
IntegerPromotion_true-no-overflow.c.i | true | .080 | .090 | 17 | wit | - | - | ||||||
Multiplication_true-no-overflow.c.i | true | .088 | .098 | 17 | wit | - | - | ||||||
UsualArithmeticConversions_true-no-overflow.c.i | true | .13 | .14 | 17 | wit | - | - | ||||||
../../sv-benchmarks/c/signedintegeroverflow-regression/ | 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 | 12 | 2.5 | 3.1 | 210 | 12 | 50 | 29 | 1800 | 12 | 83 | 52 | 2600 | |
correct results | 12 | 2.5 | 3.1 | 210 | 8 | 50 | 29 | 1800 | 8 | 83 | 52 | 2600 | |
correct true | 4 | .41 | .46 | 68 | 0 | 0 | 0 | 0 | 8 | 0 | 0 | 0 | |
correct false | 8 | 2.1 | 2.7 | 140 | 8 | 50 | 29 | 1800 | 0 | 83 | 52 | 2600 | |
incorrect results | 0 | ||||||||||||
incorrect true | 0 | ||||||||||||
incorrect false | 0 | ||||||||||||
score (12 tasks, max score: 16) | 16 | ||||||||||||
Run set | sv-comp16.BitVectorsOverflows |