| 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.BitVectorsOverflows | ||||||||||||
| 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/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 | timeout | 130 | 930 | 1200 | wit | - | - | ||||||
| Multiplication_false-no-overflow.c.i | false(no-overflow) | 8.4 | 2.6 | 320 | wit | true | 5.2 | 3.0 | 210 | false(no-overflow) | 10 | 6.3 | 320 |
| NoConversion_false-no-overflow.c.i | timeout | 130 | 930 | 1100 | wit | - | - | ||||||
| PostfixDecrement_false-no-overflow.c.i | timeout | 130 | 930 | 1100 | wit | - | - | ||||||
| PostfixIncrement_false-no-overflow.c.i | timeout | 130 | 930 | 1300 | wit | - | - | ||||||
| PrefixDecrement_false-no-overflow.c.i | timeout | 130 | 930 | 960 | wit | - | - | ||||||
| PrefixIncrement_false-no-overflow.c.i | timeout | 130 | 930 | 1300 | wit | - | - | ||||||
| UnaryMinus_false-no-overflow.c.i | timeout | 140 | 930 | 1200 | wit | - | - | ||||||
| ConversionToSignedInt_true-no-overflow.c.i | true | 8.2 | 2.7 | 310 | wit | - | - | ||||||
| IntegerPromotion_true-no-overflow.c.i | timeout | 140 | 930 | 1500 | wit | - | - | ||||||
| Multiplication_true-no-overflow.c.i | timeout | 130 | 930 | 1200 | wit | - | - | ||||||
| UsualArithmeticConversions_true-no-overflow.c.i | timeout | 130 | 930 | 1300 | 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 | 1300 | 9300 | 13000 | 12 | 5.2 | 3.0 | 210 | 12 | 10 | 6.3 | 320 | |
| correct results | 2 | 17 | 5.2 | 640 | 1 | 5.2 | 3.0 | 210 | 1 | 10 | 6.3 | 320 | |
| correct true | 1 | 8.2 | 2.7 | 310 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | |
| correct false | 1 | 8.4 | 2.6 | 320 | 0 | 5.2 | 3.0 | 210 | 1 | 10 | 6.3 | 320 | |
| incorrect results | 0 | ||||||||||||
| incorrect true | 0 | ||||||||||||
| incorrect false | 0 | ||||||||||||
| score (12 tasks, max score: 16) | 3 | ||||||||||||
| Run set | sv-comp16.BitVectorsOverflows | ||||||||||||