Tool 2LS 0.3.4 BLAST 2.7.3 CBMC CPAchecker 1.4-svcomp16c CPAchecker 1.4-svn 18373 CPAchecker 1.4-svcomp16c ESBMC ESBMC version 2.0.0 64-bit x86_64 linux DepthK ESBMC+DepthK version 2.1 impara 0.45 CPAchecker 1.4-svn 18356M SeaHorn-F16 0.1.0 skink SMACK+Corral 1.5.2 symbiotic 3.0.1 ULTIMATE Automizer cfb9fd9e ULTIMATE Kojak fd30d3d8 VVT prerelease
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 Linux 4.2.0-23-generic Linux 4.2.0-22-generic 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-02 22:42:27 CET [[ 2016-01-15 08:01:51 CET ]] [[ 2016-01-15 21:37:22 CET ]] 2016-01-03 17:36:26 CET [[ 2016-01-15 08:15:11 CET ]] [[ 2016-01-15 21:49:51 CET ]] 2016-01-03 00:42:25 CET [[ 2016-01-15 08:22:02 CET ]] [[ 2016-01-15 21:54:19 CET ]] 2016-01-04 06:25:51 CET [[ 2016-01-15 08:31:02 CET ]] [[ 2016-01-15 21:59:57 CET ]] 2016-01-04 01:42:53 CET [[ 2016-01-15 08:36:34 CET ]] [[ 2016-01-15 22:02:40 CET ]] 2016-01-04 20:04:07 CET [[ 2016-01-15 08:41:31 CET ]] [[ 2016-01-15 22:05:37 CET ]] 2016-01-04 13:17:38 CET [[ 2016-01-15 08:48:20 CET ]] [[ 2016-01-15 22:10:37 CET ]] 2016-01-16 17:45:19 CET [[ 2016-01-17 00:36:28 CET ]] [[ 2016-01-17 00:39:38 CET ]] 2016-01-05 14:06:34 CET [[ 2016-01-15 09:00:06 CET ]] [[ 2016-01-15 22:17:52 CET ]] 2016-01-13 07:41:14 CET [[ 2016-01-15 09:11:00 CET ]] [[ 2016-01-15 22:23:23 CET ]] 2016-01-10 22:01:17 CET [[ 2016-01-15 09:16:15 CET ]] [[ 2016-01-15 22:26:01 CET ]] 2016-01-11 21:35:00 [[ 2016-01-15 18:20:27 CET ]] [[ 2016-01-15 22:30:28 CET ]] 2016-01-15 22:52:00 CET [[ 2016-01-16 00:34:30 CET ]] [[ 2016-01-16 00:56:26 CET ]] 2016-01-07 09:05:16 CET [[ 2016-01-15 09:34:34 CET ]] [[ 2016-01-15 22:36:10 CET ]] 2016-01-07 09:04:54 CET [[ 2016-01-15 09:39:10 CET ]] [[ 2016-01-15 22:39:28 CET ]] 2016-01-14 23:51:13 CET [[ 2016-01-15 09:43:48 CET ]] [[ 2016-01-15 22:41:15 CET ]] 2016-01-08 15:10:30 CET [[ 2016-01-15 09:49:48 CET ]] [[ 2016-01-15 22:43:29 CET ]] 2016-01-17 23:14:00 CET [[ 2016-01-18 06:54:01 CET ]] [[ 2016-01-18 07:05:55 CET ]]
Run set 2ls.sv-comp16.Simple blast.sv-comp16.Simple cbmc.sv-comp16.Simple cpa-bam.sv-comp16.Simple cpa-kind.sv-comp16.Simple cpa-refsel.sv-comp16.Simple cpa-seq.sv-comp16.Simple esbmc.sv-comp16.Simple esbmcdepthk.sv-comp16.Simple impara.sv-comp16.Simple lpi.sv-comp16.Simple seahorn.sv-comp16.Simple skink.sv-comp16.Simple smack.sv-comp16.Simple symbiotic3.sv-comp16.Simple uautomizer.sv-comp16.Simple ukojak.sv-comp16.Simple vvt.sv-comp16.Simple
Options --k-induction --competition-mode --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr -svcomp-witness error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/blast.2016-01-03_1736.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/blast.2016-01-03_1736.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --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-comp16-bam -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16--k-induction -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16--refsel -disable-java-assertions -heap 12500m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16 -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -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 ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --eager --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/impara.2016-01-13_0741.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/impara.2016-01-13_0741.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -lpi-svcomp16 -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/lpi.2016-01-10_2201.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/lpi.2016-01-10_2201.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --cex=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/skink.2016-01-15_2252.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/skink.2016-01-15_2252.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -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 ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -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 ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/vvt.2016-01-17_2314.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/vvt.2016-01-17_2314.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/ status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB)
ntdrivers/cdaudio_false-unreach-call.i.cil.c timeout 900    2800 timeout 740    250 true 210   4800 timeout 900   4800 timeout 900 5400 timeout 900 3200 timeout 900 5000 unknown 8.4 2200 unknown 440 460 error (8) 670    70 timeout 900 7000 timeout 900   320 unknown 34 2300 timeout 890   1900 error .23 16 timeout 900 2500 error 460 9500 unknown .71 19
ntdrivers/diskperf_false-unreach-call.i.cil.c witness timeout 3.3  780 witness timeout 14    180 witness timeout 1.5 100 timeout 900   4400 witness timeout 63 1400 false(reach) 170 1200 false(reach) 120 3900 unknown 4.2 210 unknown 900 48 error (8) .70 45 witness timeout 31 580 witness timeout 1.8 120 unknown 25 1300 witness timeout 7.8 170 witness timeout 54    21 unknown 29 580 unknown 140 3000 unknown .64 15
ntdrivers/floppy_false-unreach-call.i.cil.c witness unconfirmed 12    2100 false(reach) 9.7  130 witness invalid (assertion) 3.2 140 witness timeout 52   1400 witness unconfirmed 130 3100 timeout 900 930 false(reach) 25 860 unknown 890   280 unknown 900 74 true .52 59 witness unconfirmed 58 1000 witness timeout 2.3 140 unknown 34 2100 witness unconfirmed 14   230 unknown .64 32 error 98 2900 error 55 6700 unknown 1.2  44
ntdrivers/kbfiltr_false-unreach-call.i.cil.c true 110    630 false(reach) 42    58 error 850   2200 false(reach) 23   790 timeout 900 4100 false(reach) 51 860 false(reach) 15 540 witness timeout 810   5600 unknown 900 1900 error (8) .39 37 timeout 900 4000 false(reach) 1.1 66 unknown 19 870 witness unconfirmed 6.0 130 unknown .36 15 timeout 900 2500 unknown 32 500 unknown .20 16
ntdrivers/parport_false-unreach-call.i.cil.c error (6) .84 66 witness timeout 7.6  100 witness timeout 14   670 timeout 900   6100 witness timeout 140 2100 false(reach) 520 1900 false(reach) 130 4600 unknown 900   8600 unknown 900 2600 witness timeout .94 68 witness timeout 100 1200 witness timeout 7.6 700 unknown 33 2200 witness timeout 15   340 unknown 19    67 unknown 170 1100 unknown 500 2700 unknown 1.4  28
ntdrivers/cdaudio_true-unreach-call.i.cil.c true 63    1400 true 290    270 true 330   3600 timeout 900   5000 true 270 4400 true 450 1200 true 14 490 unknown 6.3 2100 unknown 81 910 error (8) .85 65 true 87 1400 true 1.2 75 unknown 32 2400 true 23   250 error .39 16 unknown 68 1200 error 450 7800 unknown .64 18
ntdrivers/diskperf_true-unreach-call.i.cil.c true 3.4  780 true 190    410 true 250   8300 timeout 900   4400 true 46 1400 true 360 950 true 110 3600 unknown 4.3 210 unknown 900 48 error (8) .51 46 true 65 1500 true 2.1 140 unknown 27 1400 true 21   220 unknown 53    21 unknown 36 610 unknown 120 4800 unknown .51 17
ntdrivers/floppy2_true-unreach-call.i.cil.c error (6) 4.7  470 true .56 44 true 850   4200 timeout 900   4400 timeout 900 8100 true 200 2500 true 440 5800 unknown 890   510 out of memory 76 15000 true 1.8  170 true 530 7500 true 5.7 300 unknown 96 8400 true 31   320 unknown 21    980 error 370 6400 error 230 5900 unknown 14    49
ntdrivers/floppy_true-unreach-call.i.cil.c error (8) 7.7  1900 exception (gremlins) 96    170 true 850   1700 timeout 910   6000 timeout 900 7100 timeout 900 940 true 460 5500 unknown 890   280 unknown 900 74 error (8) .73 59 true 170 3700 true 3.1 150 unknown 30 2200 true 240   420 unknown 1.0  32 error 180 5400 error 55 7400 unknown 1.2  44
ntdrivers/parport_true-unreach-call.i.cil.c error (6) .84 66 timeout 670    310 true 850   4900 timeout 900   6000 timeout 900 7800 timeout 900 1900 true 820 5600 unknown 900   8500 unknown 92 2200 error (8) .96 67 error (recursion) 52 910 true 110   1200 unknown 34 2400 true 29   370 unknown 20    67 unknown 150 1200 unknown 640 3300 unknown 1.4  26
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c witness unconfirmed 590    1200 witness unconfirmed 19    53 witness invalid (assertion) 13   410 false(reach) 26   840 out of memory 110 15000 timeout 900 1300 out of memory 200 15000 witness timeout 800   4600 unknown 890 3400 error (8) 8.7  33 out of memory 93 15000 false(reach) 2.3 67 unknown 13 470 witness unconfirmed 17   210 unknown 19    20 unknown 290 960 timeout 41 620 unknown .17 15
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c witness unconfirmed 410    910 witness unconfirmed 13    48 witness invalid (assertion) 4.6 180 false(reach) 15   650 out of memory 100 15000 timeout 900 1300 out of memory 200 15000 witness unconfirmed 680   6900 unknown 890 3400 error (8) 8.8  33 exception 28 570 false(reach) 2.3 75 unknown 11 470 witness timeout 10   190 unknown .93 20 unknown 260 700 timeout 36 580 unknown .14 13
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c witness unconfirmed 320    910 witness unconfirmed 14    46 witness invalid (assertion) 4.3 180 false(reach) 17   650 out of memory 100 15000 timeout 900 1300 out of memory 210 15000 witness unconfirmed 710   7000 unknown 900 3500 error (8) 8.9  33 out of memory 82 15000 false(reach) 2.3 79 unknown 11 470 witness timeout 9.9 190 unknown 1.0  20 unknown 260 690 timeout 36 600 unknown .12 13
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c witness unconfirmed 420    910 witness unconfirmed 15    53 witness invalid (assertion) 4.4 180 false(reach) 15   650 out of memory 100 15000 timeout 900 1300 out of memory 200 15000 witness unconfirmed 680   6900 unknown 900 3200 error (8) 8.7  33 out of memory 83 15000 false(reach) 2.6 79 unknown 11 480 witness timeout 10   200 unknown 36    20 unknown 260 610 timeout 36 720 unknown .11 15
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c witness unconfirmed 540    1100 witness unconfirmed 8.3  46 witness invalid (assertion) 5.5 240 false(reach) 10   500 out of memory 89 15000 false(reach) 270 870 out of memory 190 15000 witness timeout 830   7700 unknown 890 3700 error (8) 8.8  33 out of memory 72 15000 false(reach) 1.3 72 unknown 12 490 witness unconfirmed 10   200 unknown 180    23 unknown 53 520 unknown 36 670 unknown .10 13
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c witness unconfirmed 450    1000 witness unconfirmed 5.3  45 witness invalid (assertion) 5.5 230 false(reach) 12   490 out of memory 87 15000 false(reach) 150 830 out of memory 190 15000 witness timeout 800   11000 unknown 890 3600 error (8) 8.9  33 out of memory 73 15000 false(reach) 1.3 78 unknown 11 480 witness unconfirmed 9.9 190 unknown 190    22 unknown 44 390 unknown 57 980 unknown .12 15
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c witness unconfirmed 450    1000 witness unconfirmed 5.1  47 witness invalid (assertion) 5.7 230 false(reach) 12   480 out of memory 89 15000 false(reach) 150 870 out of memory 190 15000 witness timeout 820   13000 unknown 890 3600 error (8) 7.9  34 out of memory 72 15000 false(reach) 1.2 77 unknown 11 480 witness unconfirmed 9.9 200 unknown 180    22 unknown 50 530 unknown 71 1100 unknown .16 13
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c witness unconfirmed 450    1000 witness unconfirmed 5.4  47 witness invalid (assertion) 5.5 230 false(reach) 9.6 490 out of memory 88 15000 false(reach) 190 860 out of memory 190 15000 witness timeout 820   13000 unknown 890 3600 error (8) 9.1  33 out of memory 75 15000 false(reach) 1.3 76 unknown 12 500 witness unconfirmed 10   190 unknown 180    23 unknown 48 520 unknown 57 1000 unknown .16 15
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c timeout 900    1300 witness unconfirmed 330    250 witness invalid (assertion) 5.7 230 false(reach) 21   760 out of memory 110 15000 false(reach) 100 820 out of memory 100 15000 witness timeout 830   13000 unknown 890 3600 error (8) 8.0  34 out of memory 86 15000 false(reach) 3.1 83 unknown 12 500 witness unconfirmed 20   240 unknown 180    25 error 690 3400 timeout 31 620 unknown .14 19
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c timeout 900    1300 witness unconfirmed 180    150 witness invalid (assertion) 5.8 230 false(reach) 20   760 out of memory 100 15000 timeout 900 1300 out of memory 210 15000 witness timeout 840   13000 unknown 890 3700 error (8) 8.1  34 out of memory 86 15000 false(reach) 2.9 85 unknown 12 490 witness unconfirmed 19   230 unknown 180    23 error 56 880 timeout 93 1200 unknown .19 13
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c timeout 900    1300 timeout 690    320 witness invalid (assertion) 16   460 false(reach) 29   890 out of memory 140 15000 timeout 900 1500 out of memory 130 15000 witness timeout 800   13000 unknown 890 3600 error (8) 7.9  35 out of memory 110 15000 false(reach) 13   100 unknown 12 490 witness unconfirmed 250   330 unknown 190    23 timeout 900 3900 timeout 100 1200 unknown .15 17
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c timeout 900    1300 witness unconfirmed 180    150 witness invalid (assertion) 5.9 230 false(reach) 19   740 out of memory 100 15000 timeout 900 1100 out of memory 210 15000 witness timeout 800   13000 unknown 890 3700 error (8) 8.9  33 out of memory 88 15000 false(reach) 2.6 84 unknown 12 480 witness unconfirmed 19   230 unknown 180    23 timeout 900 4600 timeout 73 1600 unknown .13 10
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c timeout 900    1300 timeout 690    320 witness invalid (assertion) 15   460 false(reach) 33   870 out of memory 140 15000 timeout 900 1300 out of memory 140 15000 witness timeout 800   13000 unknown 890 3600 error (8) 8.8  33 out of memory 120 15000 false(reach) 8.4 82 unknown 11 490 witness unconfirmed 300   350 unknown 180    23 timeout 900 3200 timeout 93 1500 unknown .16 15
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c witness unconfirmed 810    1300 witness unconfirmed 74    63 witness invalid (assertion) 6.0 230 false(reach) 12   550 out of memory 99 15000 timeout 900 1200 out of memory 190 15000 witness timeout 840   13000 unknown 890 3700 error (8) 8.4  33 out of memory 81 15000 false(reach) 2.1 79 unknown 11 500 witness unconfirmed 14   230 unknown 180    23 unknown 65 560 timeout 74 1400 unknown .22 13
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c timeout 900    1300 witness unconfirmed 270    170 witness invalid (assertion) 5.6 230 false(reach) 25   760 out of memory 100 15000 false(reach) 94 850 out of memory 110 15000 witness timeout 840   13000 unknown 890 3600 error (8) 8.7  33 out of memory 88 15000 false(reach) 2.7 71 unknown 11 490 witness unconfirmed 19   230 unknown 180    24 timeout 900 3200 unknown 71 1300 unknown .18 15
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c timeout 900    1400 witness unconfirmed 190    150 witness invalid (assertion) 5.7 230 false(reach) 25   810 out of memory 100 15000 timeout 900 1500 out of memory 200 15000 witness timeout 850   11000 unknown 890 3700 error (8) 8.6  33 out of memory 87 15000 false(reach) 3.0 84 unknown 11 500 witness unconfirmed 19   230 unknown 190    23 error 58 880 timeout 81 1400 unknown .14 13
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c timeout 900    1300 witness unconfirmed 270    170 witness invalid (assertion) 5.3 230 false(reach) 23   750 out of memory 100 15000 false(reach) 110 850 out of memory 100 15000 witness timeout 800   11000 unknown 890 3600 error (8) 8.7  34 exception 31 700 false(reach) 3.4 86 unknown 12 490 witness unconfirmed 20   240 unknown 160    24 error 290 2400 timeout 62 1200 unknown .16 13
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c timeout 900    1300 timeout 690    450 witness invalid (assertion) 17   460 false(reach) 29   910 out of memory 140 15000 timeout 900 1300 out of memory 130 15000 witness timeout 800   11000 unknown 890 3700 error (8) 8.7  35 out of memory 120 15000 false(reach) 14   110 unknown 12 500 witness unconfirmed 250   350 unknown 140    24 timeout 900 3800 timeout 28 600 unknown .17 12
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c timeout 900    1400 witness unconfirmed 330    250 witness invalid (assertion) 5.4 230 false(reach) 24   780 out of memory 100 15000 false(reach) 100 860 out of memory 100 15000 witness timeout 850   13000 unknown 890 3600 error (8) 8.3  34 out of memory 86 15000 false(reach) 2.8 79 unknown 12 500 witness unconfirmed 20   240 unknown 180    25 error 270 3000 unknown 66 1100 unknown .15 13
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 880    1400 timeout 660    280 true 850   1300 true 210   1100 true 48 1200 timeout 900 1100 true 150 1300 true 230   4500 unknown 890 3500 error (8) 8.6  35 true 47 880 true 9.3 70 unknown 10 480 true 880   390 unknown .67 20 error 120 1500 timeout 36 550 unknown .20 13
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 740    1300 true 310    160 true 850   1300 true 160   990 true 52 1300 timeout 900 920 true 150 970 true 240   6800 unknown 900 3400 error (8) 9.1  33 true 39 840 true 91   140 unknown 11 470 true 880   330 unknown .92 20 error 180 2500 timeout 39 650 unknown .14 11
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c true 700    1300 timeout 670    290 true 850   1300 true 89   1100 true 51 1200 timeout 900 1100 true 150 990 true 230   6800 unknown 890 3400 error (8) 8.8  35 true 39 810 true 58   100 unknown 11 480 true 880   390 unknown 71    20 error 200 1800 timeout 38 660 unknown .23 13
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 700    1300 true 310    160 true 850   1300 true 90   970 true 48 1200 timeout 900 1400 true 150 1200 true 260   6900 unknown 890 3500 error (8) 9.0  36 segmentation fault 36 810 true 15   81 unknown 12 470 true 880   350 unknown 36    20 error 130 2100 timeout 52 770 unknown .15 13
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c timeout 900    1400 timeout 670    380 true 850   1600 true 38   880 true 68 1200 timeout 900 1200 true 160 970 true 310   8100 unknown 890 3700 error (8) 8.7  33 timeout 900 4100 true 12   67 unknown 12 500 true 880   400 unknown 140    23 timeout 900 4800 timeout 58 1000 unknown .13 15
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c timeout 900    1300 timeout 660    440 true 850   1500 true 64   1100 true 41 950 timeout 900 1000 true 140 780 true 430   12000 unknown 890 3600 error (8) 8.7  33 timeout 900 5000 true 64   81 unknown 11 500 true 880   420 unknown 160    23 error 400 2400 timeout 66 1000 unknown .14 13
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c timeout 900    1200 timeout 700    300 true 850   1600 true 140   1400 true 160 3800 timeout 900 1300 true 400 4800 true 450   14000 unknown 890 3600 error (8) 8.5  33 timeout 900 4400 timeout 900   220 unknown 13 510 true 880   450 unknown 180    26 timeout 900 6100 timeout 27 690 unknown .18 11
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c timeout 900    1400 timeout 670    300 true 850   1600 true 150   1200 true 150 3800 timeout 900 880 true 250 2900 true 460   14000 unknown 890 3700 error (8) 8.9  33 timeout 900 5500 true 93   92 unknown 12 490 true 880   410 unknown 180    23 timeout 900 5700 timeout 78 1200 unknown .14 13
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c timeout 900    1300 timeout 670    300 true 850   1600 true 120   1300 true 57 1200 timeout 900 1400 true 160 1200 true 440   14000 unknown 890 3600 error (8) 9.1  33 timeout 900 5400 true 11   78 unknown 12 500 true 880   430 unknown 180    24 timeout 900 5200 timeout 72 1500 unknown .16 13
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c timeout 900    1300 timeout 670    310 true 850   1600 true 120   1200 true 150 3400 timeout 900 1200 true 250 2300 out of memory 500   15000 unknown 890 3700 error (8) 9.1  33 timeout 900 5100 true 77   87 unknown 11 490 true 880   410 unknown 180    23 error 490 4700 timeout 69 960 unknown .24 13
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c timeout 900    1400 timeout 670    430 true 850   1500 true 70   1000 true 57 1200 timeout 900 1200 true 160 1500 true 450   13000 unknown 890 3700 error (8) 8.7  33 timeout 900 5100 true 6.8 73 unknown 12 480 true 880   410 unknown 200    23 error 620 5600 timeout 67 950 unknown .16 11
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c timeout 900    1300 timeout 660    410 true 850   1600 true 100   1500 true 140 3400 timeout 900 1000 true 240 2800 true 460   14000 unknown 890 3700 error (8) 8.9  33 timeout 900 5200 true 43   78 unknown 12 490 true 880   390 unknown 180    23 error 670 5100 timeout 72 920 unknown .16 13
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c timeout 900    1300 timeout 690    310 true 850   1600 true 120   1700 true 130 3100 timeout 900 1400 true 390 4700 true 460   14000 unknown 890 3600 error (8) 9.0  33 timeout 900 5200 true 240   120 unknown 14 540 true 880   410 unknown 190    24 error 690 5500 timeout 82 1500 unknown .20 13
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c timeout 900    1300 timeout 670    300 true 850   1600 true 110   1200 true 64 1500 timeout 900 1300 true 170 1700 true 470   14000 unknown 890 3700 error (8) 9.0  33 timeout 900 5000 true 35   77 unknown 11 500 true 880   390 unknown 180    23 timeout 900 5200 timeout 73 1300 unknown .11 13
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c timeout 900    1300 timeout 670    300 true 850   1600 true 95   1100 true 140 3600 timeout 900 1300 true 250 4300 true 460   14000 unknown 900 3700 error (8) 8.5  33 timeout 900 4800 timeout 900   200 unknown 12 520 true 880   430 unknown 180    24 timeout 900 7900 timeout 85 1200 unknown .23 11
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c timeout 900    1300 timeout 670    420 true 850   1600 true 200   1500 true 100 2200 timeout 900 1200 true 200 2000 true 450   13000 unknown 890 3600 error (8) 8.9  33 timeout 900 5100 true 10   80 unknown 11 500 true 880   420 unknown 90    24 timeout 900 5800 timeout 27 710 unknown .15 11
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c timeout 900    1200 timeout 690    310 true 850   1600 true 190   1900 true 150 3800 timeout 900 1400 true 250 4400 true 440   13000 unknown 890 3600 error (8) 7.9  34 timeout 900 4400 timeout 900   180 unknown 12 500 true 880   400 unknown 190    25 timeout 900 5900 timeout 79 1300 unknown .18 11
../../sv-benchmarks/c/ status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB)
total tasks 46 29000 56000 46 17000 10000 46 19000 61000 46 9700 78000 46 8800 370000 46 32000 57000 46 9900 360000 46 27000 430000 46 38000 150000 46 990    1900 46 16000 350000 46 4600 6600 46 780 43000 46 17000 16000 46 5200 2100 46 21000 140000 46 4800 88000 46 28 740
    correct results 6 3100 7600 7 1200 1200 22 18000 48000 37 2500 35000 19 1900 44000 14 2900 15000 26 5800 70000 16 6200 180000 0 1 1.8  170 7 970 17000 39 970 4700 0 22 15000 8400 0 0 0 0
        correct true 6 3100 7600 5 1100 1000 22 18000 48000 17 2100 21000 19 1900 44000 3 1000 4700 22 5500 60000 16 6200 180000 0 1 1.8  170 7 970 17000 19 890 3100 0 22 15000 8400 0 0 0 0
        correct false 0 2 52 190 0 20 400 14000 0 11 1900 11000 4 300 9900 0 0 0 0 20 73 1600 0 0 0 0 0 0
    incorrect results 1 110 630 0 1 210 4800 0 0 0 0 0 0 1 .52 59 0 0 0 0 0 0 0 0
        incorrect true 1 110 630 0 1 210 4800 0 0 0 0 0 0 1 .52 59 0 0 0 0 0 0 0 0
        incorrect false 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
score (46 tasks, max score: 68) -20 12 12 54 38 17 48 32 0 -30 14 58 0 44 0 0 0 0
Run set 2ls.sv-comp16.Simple blast.sv-comp16.Simple cbmc.sv-comp16.Simple cpa-bam.sv-comp16.Simple cpa-kind.sv-comp16.Simple cpa-refsel.sv-comp16.Simple cpa-seq.sv-comp16.Simple esbmc.sv-comp16.Simple esbmcdepthk.sv-comp16.Simple impara.sv-comp16.Simple lpi.sv-comp16.Simple seahorn.sv-comp16.Simple skink.sv-comp16.Simple smack.sv-comp16.Simple symbiotic3.sv-comp16.Simple uautomizer.sv-comp16.Simple ukojak.sv-comp16.Simple vvt.sv-comp16.Simple