Tool CPAchecker 1.5-svn 20187M CPAchecker 1.5-svn 20312M CPAchecker 1.5-svn 20187M CPAchecker 1.5-svn 20312M CPAchecker 1.5-svn 20187M
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 2
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-30-generic [Linux 4.2.0-34-generic; Linux 4.2.0-30-generic] Linux 4.2.0-30-generic [Linux 4.2.0-34-generic; Linux 4.2.0-30-generic] Linux 4.2.0-30-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-03-11 14:33:18 CET 2016-03-15 20:04:06 CET 2016-03-11 14:33:18 CET 2016-03-15 20:04:06 CET 2016-03-11 14:33:18 CET
Run set MathSAT5-heaparray.ControlFlow MathSAT5-oldarray.ControlFlow MathSAT5-uf.ControlFlow PRINCESS-heaparray-quantifiers.ControlFlow PRINCESS-heaparray.ControlFlow PRINCESS-oldarray.ControlFlow PRINCESS-uf.ControlFlow SMTInterpol-heaparray.ControlFlow SMTInterpol-oldarray.ControlFlow SMTInterpol-uf.ControlFlow Z3-heaparray-quantifiers.ControlFlow Z3-heaparray.ControlFlow Z3-oldarray.ControlFlow Z3-uf.ControlFlow
Options -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis-heaparray -setprop solver.solver=MATHSAT5 -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis -setprop solver.solver=MATHSAT5 -setprop cpa.predicate.handleArrays=true -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis -setprop solver.solver=MATHSAT5 -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis-heaparray -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeFloatAs=INTEGER -setprop cpa.predicate.useQuantifiersOnArrays=true -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis-heaparray -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeFloatAs=INTEGER -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeFloatAs=INTEGER -setprop cpa.predicate.handleArrays=true -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeFloatAs=INTEGER -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis-heaparray -setprop solver.solver=SMTINTERPOL -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis -setprop solver.solver=SMTINTERPOL -setprop cpa.predicate.handleArrays=true -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis -setprop solver.solver=SMTINTERPOL -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis-heaparray -setprop cpa.predicate.useQuantifiersOnArrays=true -setprop solver.solver=Z3 -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis-heaparray -setprop solver.solver=Z3 -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis -setprop solver.solver=Z3 -setprop cpa.predicate.handleArrays=true -heap 12000M -stack 10M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis -setprop solver.solver=Z3
test/programs/benchmarks/ status cputime (s) walltime (s) memUsage host status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) memUsage host status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) memUsage host status cputime (s) walltime (s) memUsage host status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-termination.cil.c 15.9  8.66 530530304 zeus22 14.9  8.10 zeus10 493944832 14.7  8.09 zeus12 506802176 215    168    4558512128 zeus23 209    165    zeus20 4546113536 208    163    zeus14 4538732544 217    171    zeus19 4535226368 31.2  16.2  zeus09 626069504 32.5  16.9  zeus01 621809664 30.5  15.8  626376704 zeus04 14.1  7.71 491876352 zeus07 15.9  8.54 zeus20 496791552 13.8  7.51 zeus22 482865152 15.3  8.23 zeus04 516366336
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c 10.6  5.94 433053696 zeus02 10.3  5.69 zeus20 426188800 9.70 5.54 zeus04 414326784 59.7  30.7  1043214336 zeus14 57.9  29.7  zeus03 1057816576 56.9  29.1  zeus13 1037799424 59.1  30.4  zeus09 1046794240 21.3  11.3  zeus24 582418432 21.7  11.5  zeus16 564846592 22.3  11.7  560185344 zeus22 11.3  6.24 428351488 zeus16 10.3  5.80 zeus22 414502912 9.79 5.52 zeus18 403693568 10.9  6.07 zeus08 425844736
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c 11.8  6.55 458174464 zeus19 11.5  6.33 zeus04 447823872 11.7  6.52 zeus07 443899904 84.1  47.3  1875533824 zeus20 85.6  47.9  zeus05 2087239680 81.4  45.7  zeus14 1909780480 82.4  46.4  zeus04 2079485952 27.1  14.2  zeus03 568197120 25.2  13.1  zeus17 608571392 24.5  12.8  578592768 zeus21 12.0  6.64 432001024 zeus11 11.4  6.38 zeus01 435961856 11.5  6.38 zeus08 440451072 12.0  6.62 zeus04 448761856
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c 9.21 5.12 394915840 zeus14 8.23 4.68 zeus03 384036864 9.61 5.28 zeus18 397418496 45.2  23.2  864780288 zeus21 39.4  20.3  zeus11 861057024 42.7  22.0  zeus19 881582080 42.3  21.7  zeus08 856817664 14.9  8.03 zeus12 486404096 14.0  7.51 zeus08 478343168 15.4  8.27 468680704 zeus12 8.84 4.90 383844352 zeus23 9.61 5.36 zeus18 373055488 8.43 4.75 zeus17 380088320 9.30 5.17 zeus15 378687488
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c 10.1  5.57 299401216 zeus21 10.3  5.71 zeus18 305217536 10.4  5.78 zeus08 295997440 138    105    4382576640 zeus12 126    94.7  zeus19 4217868288 126    95.6  zeus06 3862814720 126    94.5  zeus11 4459786240 25.3  13.2  zeus22 644112384 28.8  15.0  zeus18 624340992 26.0  13.6  597528576 zeus15 11.3  6.18 331632640 zeus09 11.1  6.21 zeus08 328982528 10.3  5.80 zeus04 310378496 10.3  5.81 zeus24 322678784
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c 7.85 4.55 271298560 zeus14 7.86 4.58 zeus04 266063872 7.83 4.56 zeus01 260812800 902    849    4513898496 zeus02 902    850    zeus08 4502654976 902    852    zeus03 4493979648 902    851    zeus19 4513841152 20.5  10.8  zeus22 631308288 22.0  11.5  zeus17 637239296 23.4  12.3  606081024 zeus24 8.10 4.71 269692928 zeus18 7.68 4.46 zeus04 267751424 7.35 4.28 zeus07 267407360 8.06 4.65 zeus22 269455360
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c 7.04 4.05 255889408 zeus19 7.14 4.08 zeus07 257544192 7.27 4.18 zeus12 264253440 45.6  23.5  866762752 zeus07 47.2  24.2  zeus17 883961856 41.1  21.2  zeus10 862687232 43.3  22.5  zeus13 875552768 16.6  9.00 zeus12 538148864 16.2  8.71 zeus24 522076160 16.7  8.92 527572992 zeus22 7.43 4.24 265367552 zeus12 7.46 4.25 zeus17 258211840 6.76 3.89 zeus01 252743680 7.16 4.11 zeus13 259866624
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c 7.88 4.44 273469440 zeus13 7.79 4.41 zeus01 267300864 7.86 4.46 zeus13 274513920 57.9  30.7  1308696576 zeus12 55.7  29.8  zeus01 1294049280 59.6  31.7  zeus21 1293881344 55.8  29.7  zeus20 1322373120 20.4  10.7  zeus17 579850240 20.2  10.7  zeus02 604413952 19.9  10.5  570671104 zeus24 8.94 5.04 269094912 zeus03 7.95 4.51 zeus20 266862592 8.01 4.52 zeus15 266383360 8.44 4.73 zeus14 274329600
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c 4.96 2.90 220348416 zeus08 4.82 2.75 zeus21 222072832 5.16 2.96 zeus12 229863424 11.7  6.44 381022208 zeus09 14.0  7.51 zeus11 425385984 12.5  6.80 zeus07 390963200 13.1  7.09 zeus01 401915904 6.11 3.55 zeus13 251383808 5.39 3.07 zeus21 241086464 6.29 3.62 247386112 zeus02 4.88 2.85 222539776 zeus14 5.24 3.07 zeus13 225599488 4.67 2.69 zeus04 218382336 5.22 3.01 zeus16 224792576
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c 5.59 3.18 231354368 zeus04 5.71 3.23 zeus22 238186496 5.84 3.34 zeus02 232796160 18.6  9.79 428945408 zeus02 17.8  9.38 zeus04 464941056 15.3  8.28 zeus10 404475904 17.5  9.31 zeus17 458293248 7.74 4.34 zeus19 284016640 7.15 4.08 zeus22 280801280 7.80 4.36 286638080 zeus23 5.60 3.26 232951808 zeus10 5.88 3.36 zeus03 235843584 5.83 3.34 zeus16 226897920 5.57 3.20 zeus04 231936000
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c 11.3  6.18 452509696 zeus19 11.5  6.30 zeus24 438018048 12.0  6.48 zeus16 449019904 60.7  31.4  1107628032 zeus17 59.3  30.7  zeus19 1159970816 61.0  31.5  zeus04 1119789056 60.4  31.3  zeus02 1106788352 24.4  12.8  zeus01 563101696 23.4  12.4  zeus19 657043456 21.7  11.5  569040896 zeus03 13.0  7.20 459862016 zeus08 13.0  7.20 zeus05 471093248 12.7  7.07 zeus11 451620864 12.9  7.20 zeus18 462098432
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 11.9  6.61 453824512 zeus10 11.9  6.47 zeus23 453763072 11.0  6.14 zeus09 452243456 60.2  31.1  1031794688 zeus04 53.2  27.6  zeus08 921354240 56.6  29.1  zeus01 991637504 51.8  26.8  zeus15 1002672128 24.6  12.9  zeus01 541544448 23.4  12.2  zeus12 646000640 22.7  11.9  520347648 zeus16 12.2  6.78 451641344 zeus02 11.2  6.29 zeus14 436473856 11.3  6.43 zeus08 444219392 11.9  6.53 zeus21 452268032
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c 11.4  6.30 455368704 zeus08 11.4  6.29 zeus13 458571776 12.1  6.61 zeus06 469008384 54.7  28.1  917413888 zeus21 50.3  26.1  zeus23 934051840 53.4  27.4  zeus04 1002807296 57.3  29.6  zeus12 1006387200 25.7  13.5  zeus07 647745536 25.8  13.5  zeus15 611319808 28.0  14.6  699396096 zeus15 15.9  8.83 526123008 zeus14 14.8  8.27 zeus12 482578432 14.6  8.10 zeus19 508321792 15.3  8.45 zeus13 506568704
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c 12.3  6.70 456851456 zeus19 11.0  6.15 zeus11 456585216 11.8  6.43 zeus15 452198400 55.2  28.4  950784000 zeus18 54.0  28.1  zeus14 1018175488 56.8  29.2  zeus11 991531008 53.1  27.5  zeus19 949043200 27.6  14.3  zeus22 786862080 26.5  13.8  zeus07 700502016 25.1  13.1  741224448 zeus17 11.7  6.45 452190208 zeus13 12.1  6.67 zeus04 457990144 13.0  7.13 zeus09 450654208 12.4  6.83 zeus01 451710976
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c 7.32 4.21 368271360 zeus17 7.28 4.08 zeus17 371159040 8.11 4.51 zeus24 385945600 23.1  12.3  521392128 zeus11 23.1  12.1  zeus16 541167616 20.3  10.8  zeus18 475414528 21.7  11.5  zeus15 503070720 8.66 4.88 zeus08 394244096 8.03 4.59 zeus22 386932736 8.27 4.64 388784128 zeus22 7.68 4.26 373719040 zeus11 7.40 4.14 zeus06 368435200 7.68 4.22 zeus13 357072896 7.47 4.23 zeus17 363298816
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c 57.3  42.1  932663296 zeus14 55.2  41.0  zeus17 928149504 57.1  42.1  zeus02 913113088 902    819    4669353984 zeus20 902    822    zeus15 4637061120 902    822    zeus20 4659593216 902    818    zeus15 4642062336 164    124    zeus16 3627114496 139    94.7  zeus05 2724532224 156    116    2929012736 zeus19 85.0  70.2  880111616 zeus12 90.0  74.3  zeus02 880590848 83.3  67.7  zeus08 862175232 83.5  69.3  zeus07 872218624
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c 387    363    2132910080 zeus21 386    363    zeus06 1809416192 405    380    zeus23 2062749696 830    755    4562677760 zeus02 802    729    zeus23 4587692032 803    733    zeus17 4569571328 801    731    zeus24 4586524672 901    840    zeus14 4960595968 135    85.8  zeus10 2711101440 138    90.9  2576908288 zeus07 84.1  64.2  1050685440 zeus24 75.0  58.5  zeus11 996196352 75.8  58.7  zeus20 972730368 74.4  58.3  zeus23 979472384
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c 17.7  9.99 510980096 zeus16 16.9  10.0  zeus22 498589696 18.5  10.3  zeus16 520507392 77.0  41.3  1407459328 zeus15 75.4  40.2  zeus11 1448083456 76.6  41.0  zeus23 1601884160 79.1  42.1  zeus18 1635278848 47.5  24.3  zeus11 867282944 40.9  21.3  zeus02 870985728 84.8  46.8  1599057920 zeus18 16.0  8.70 505892864 zeus20 71.0  49.5  zeus04 925229056 15.1  8.31 zeus15 493748224 16.0  8.65 zeus20 506314752
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c 11.4  6.36 448405504 zeus09 11.3  6.15 zeus17 442044416 10.5  5.83 zeus12 427663360 45.2  23.4  838119424 zeus18 41.6  21.6  zeus15 845484032 44.6  22.9  zeus12 830345216 44.3  22.7  zeus02 846323712 20.7  11.0  zeus14 526905344 19.6  10.4  zeus22 597483520 21.2  11.2  538353664 zeus02 10.8  5.91 426237952 zeus08 9.94 5.46 zeus21 427692032 10.5  5.82 zeus02 418283520 10.1  5.56 zeus23 415477760
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c 10.4  5.79 435400704 zeus05 11.0  6.21 zeus22 448061440 10.4  5.79 zeus12 445493248 39.6  20.5  854843392 zeus19 42.1  21.7  zeus07 837533696 40.1  20.9  zeus06 838729728 41.9  21.7  zeus09 852299776 16.5  8.83 zeus03 498511872 16.3  8.66 zeus03 515227648 17.3  9.17 477827072 zeus01 9.74 5.36 411635712 zeus02 10.7  5.90 zeus13 418406400 9.53 5.32 zeus11 405491712 10.5  5.80 zeus17 419893248
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c 11.5  6.31 439607296 zeus18 9.89 5.52 zeus24 436809728 10.5  5.93 zeus11 438689792 39.2  20.2  852705280 zeus12 39.3  20.3  zeus09 843489280 39.2  20.2  zeus15 842510336 44.0  22.6  zeus18 889978880 14.8  7.97 zeus19 477765632 14.3  7.70 zeus04 483926016 16.2  8.62 511520768 zeus23 9.02 5.10 407674880 zeus17 9.44 5.17 zeus22 415526912 10.7  5.97 zeus05 406413312 9.44 5.26 zeus22 415133696
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c 6.12 3.53 272007168 zeus05 6.03 3.43 zeus24 260448256 5.93 3.43 zeus04 270082048 13.0  7.12 447500288 zeus22 12.0  6.65 zeus01 442441728 12.1  6.66 zeus08 436645888 12.0  6.51 zeus24 436867072 7.02 3.99 zeus16 340680704 6.45 3.64 zeus21 346628096 6.79 3.93 367149056 zeus22 5.67 3.31 257060864 zeus22 6.58 3.80 zeus14 353243136 5.67 3.23 zeus21 262492160 6.91 3.93 zeus22 349052928
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c 21.8  13.5  701431808 zeus21 21.8  13.3  zeus22 738889728 22.0  13.5  zeus17 684109824 121    76.8  3313426432 zeus17 113    72.0  zeus15 2866806784 117    74.3  zeus20 2624180224 114    72.2  zeus14 2769006592 56.7  31.9  zeus10 1218707456 59.3  32.9  zeus23 1182994432 58.0  31.7  1281482752 zeus01 14.0  8.24 380555264 zeus10 12.6  7.46 zeus04 376000512 12.9  7.47 zeus04 372371456 14.5  8.23 zeus13 397201408
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 33.9  22.5  787378176 zeus01 29.3  20.7  zeus05 760418304 30.0  20.8  zeus05 768823296 104    64.1  2671800320 zeus09 107    65.8  zeus08 2525937664 108    66.4  zeus22 2974797824 105    64.5  zeus21 2649264128 85.3  59.7  zeus07 1665814528 70.9  48.7  zeus20 1585233920 84.6  56.6  1603629056 zeus05 15.4  8.74 415735808 zeus01 14.8  8.51 zeus20 421310464 14.7  8.52 zeus10 454848512 15.1  8.80 zeus08 422850560
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c 52.9  43.8  809893888 zeus10 63.8  53.4  zeus03 828272640 55.0  46.0  zeus22 820875264 112    68.6  2794139648 zeus05 116    71.3  zeus15 2768007168 105    65.1  zeus24 2732335104 108    66.7  zeus10 2415783936 33.2  17.1  zeus21 831074304 36.4  18.9  zeus09 820367360 34.8  17.9  792137728 zeus12 69.5  59.6  574443520 zeus01 68.0  58.3  zeus12 607289344 65.2  56.8  zeus14 583720960 66.9  57.7  zeus22 588443648
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c 22.5  13.0  578519040 zeus12 20.8  12.1  zeus11 596594688 22.9  13.4  zeus11 608403456 110    68.1  2518339584 zeus06 107    66.4  zeus15 2914447360 108    66.8  zeus22 2211258368 107    66.0  zeus19 2772123648 53.0  27.3  zeus09 975245312 51.2  26.5  zeus05 1025437696 55.2  28.6  983515136 zeus04 68.1  58.0  655314944 zeus24 66.9  57.0  zeus03 668983296 74.2  63.5  zeus01 673435648 66.0  56.5  zeus24 617029632
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c 30.2  17.4  757907456 zeus17 26.5  16.0  zeus19 705220608 30.2  17.7  zeus07 813559808 901    842    4687917056 zeus16 901    844    zeus19 4669337600 901    841    zeus09 4695494656 902    841    zeus17 4689014784 60.1  30.7  zeus04 1099587584 50.7  26.1  zeus03 997003264 53.2  27.4  1039462400 zeus12 41.0  27.9  817491968 zeus01 40.3  27.6  zeus14 816615424 38.5  26.4  zeus09 780963840 40.2  27.5  zeus09 806760448
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c 10.0  5.47 325967872 zeus18 10.5  5.82 zeus19 338255872 9.98 5.46 zeus12 307884032 54.1  28.0  1053114368 zeus04 53.3  27.7  zeus05 1031700480 64.0  33.0  zeus04 1048199168 58.6  30.2  zeus24 1061056512 22.0  11.6  zeus24 643309568 23.1  12.1  zeus18 655032320 21.3  11.2  642727936 zeus23 27.9  16.5  549912576 zeus14 26.8  15.6  zeus21 593424384 21.7  13.5  zeus23 520581120 28.1  16.4  zeus20 634888192
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 4.81 2.83 221786112 zeus05 4.74 2.85 zeus11 228540416 4.98 2.90 zeus05 226373632 23.2  12.3  536031232 zeus09 21.4  11.3  zeus11 522358784 24.4  13.1  zeus01 516333568 22.8  12.0  zeus07 509407232 5.92 3.41 zeus24 254529536 6.23 3.61 zeus15 259317760 6.10 3.53 249143296 zeus02 5.27 3.09 231514112 zeus04 5.29 3.14 zeus03 222031872 5.03 2.98 zeus19 225386496 4.85 2.87 zeus07 227143680
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c 30.7  16.6  667746304 zeus07 24.1  13.8  zeus20 549638144 31.7  17.5  zeus20 728489984 902    830    4682248192 zeus18 902    831    zeus12 4763127808 902    831    zeus12 4695957504 902    831    zeus17 4742885376 57.7  29.5  zeus09 1058549760 51.3  26.6  zeus15 935383040 57.2  29.4  1020346368 zeus19 38.8  23.4  798285824 zeus20 34.5  20.8  zeus06 858910720 29.9  18.4  zeus13 709861376 29.8  18.7  zeus13 771223552
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c 46.0  32.9  802627584 zeus05 41.4  30.7  zeus20 781987840 45.5  32.3  zeus23 837558272 901    838    4914073600 zeus19 902    837    zeus06 4892528640 902    839    zeus08 4885659648 902    835    zeus15 4938215424 62.8  32.5  zeus01 1233403904 59.5  31.1  zeus05 1199030272 60.2  32.2  1247522816 zeus10 33.6  21.7  801161216 zeus17 30.7  20.5  zeus15 717529088 32.8  21.2  zeus08 737140736 35.0  22.7  zeus14 778641408
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c 182    166    1094512640 zeus07 160    147    zeus10 1064189952 148    134    zeus07 1577385984 902    837    4865363968 zeus14 902    837    zeus14 4844535808 902    839    zeus03 4853002240 902    836    zeus14 4850102272 59.0  31.4  zeus24 1136504832 56.9  30.2  zeus12 1197170688 60.8  32.3  1111986176 zeus17 29.4  17.3  728506368 zeus16 28.0  16.8  zeus05 719257600 25.4  15.4  zeus10 667721728 33.0  19.1  zeus02 874582016
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c 89.4  74.1  955813888 zeus04 81.8  68.9  zeus03 911077376 81.7  69.4  zeus02 920588288 902    835    4651921408 zeus10 901    834    zeus15 4686426112 902    829    zeus16 4627767296 902    834    zeus18 4651110400 63.0  36.2  zeus07 1326739456 59.2  34.4  zeus19 1252220928 67.5  38.5  1382535168 zeus17 49.5  36.5  876916736 zeus22 50.1  36.9  zeus20 819359744 47.9  35.5  zeus23 846823424 52.3  38.0  zeus08 840749056
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c 51.3  36.5  862113792 zeus08 51.1  37.8  zeus13 826241024 47.6  35.5  zeus17 811163648 901    845    4738068480 zeus12 901    843    zeus06 4740894720 902    846    zeus04 4750503936 901    843    zeus22 4715155456 120    83.4  zeus13 2012246016 116    80.9  zeus13 2308653056 88.8  54.6  1706782720 zeus16 44.8  32.1  768798720 zeus09 49.0  33.9  zeus19 804429824 42.1  30.5  zeus19 738213888 47.4  34.1  zeus18 776138752
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c 31.9  17.0  797425664 zeus02 26.1  14.4  zeus19 660910080 27.5  15.0  zeus23 745947136 901    849    4643536896 zeus21 901    850    zeus07 4647395328 902    850    zeus08 4655603712 901    851    zeus03 4661362688 67.7  35.3  zeus15 1255673856 56.9  30.4  zeus02 1275658240 66.8  35.0  1273147392 zeus10 34.7  19.8  841773056 zeus13 27.8  16.3  zeus19 712744960 27.6  15.9  zeus14 715657216 27.8  16.5  zeus19 764936192
locks/test_locks_14_false-unreach-call.c 5.75 3.35 266260480 zeus02 5.97 3.45 zeus12 265252864 5.66 3.29 zeus23 264261632 20.7  11.0  525492224 zeus10 21.9  11.5  zeus05 512446464 20.3  10.8  zeus07 480591872 19.6  10.6  zeus22 527245312 6.57 3.76 zeus07 351109120 6.67 3.86 zeus20 341749760 6.47 3.76 350011392 zeus16 5.51 3.21 260472832 zeus22 6.13 3.49 zeus05 256274432 5.68 3.21 zeus16 252297216 6.21 3.58 zeus18 255205376
locks/test_locks_15_false-unreach-call.c 6.39 3.67 271085568 zeus20 5.64 3.27 zeus24 263208960 6.33 3.66 zeus24 265867264 20.7  11.1  544583680 zeus18 19.5  10.4  zeus02 502427648 20.2  10.6  zeus03 486375424 19.8  10.6  zeus11 505978880 6.79 3.94 zeus12 355954688 7.32 4.15 zeus18 356536320 6.92 3.92 351096832 zeus22 5.30 3.11 257212416 zeus19 5.91 3.39 zeus22 255356928 5.60 3.23 zeus16 255967232 5.56 3.24 zeus03 259497984
locks/test_locks_10_true-unreach-call.c 4.17 2.51 214601728 zeus04 4.07 2.40 zeus13 217161728 4.05 2.41 zeus19 210407424 14.0  7.48 427388928 zeus21 13.7  7.41 zeus23 413585408 10.6  6.01 zeus04 409206784 10.4  5.89 zeus10 414314496 4.88 2.89 zeus06 225394688 4.43 2.60 zeus07 220770304 4.66 2.73 220868608 zeus12 4.31 2.56 219639808 zeus23 4.15 2.45 zeus09 216272896 4.12 2.38 zeus07 214343680 4.09 2.69 zeus13 213975040
locks/test_locks_11_true-unreach-call_false-termination.c 4.05 2.40 214200320 zeus14 4.03 2.37 zeus07 212189184 4.30 2.52 zeus12 215224320 12.6  6.91 437809152 zeus08 14.5  7.91 zeus16 429264896 14.1  7.59 zeus21 437911552 16.4  8.80 zeus09 501751808 4.49 2.65 zeus12 223313920 4.47 2.68 zeus05 216760320 4.32 2.61 218910720 zeus24 3.98 2.36 211435520 zeus17 4.12 2.44 zeus19 210661376 3.97 2.40 zeus20 212803584 4.40 2.56 zeus05 215166976
locks/test_locks_12_true-unreach-call_false-termination.c 4.27 2.50 214872064 zeus18 4.05 2.43 zeus18 214364160 3.94 2.32 zeus21 212160512 8.75 4.98 367308800 zeus04 11.3  6.23 zeus11 410763264 11.0  6.04 zeus05 411893760 9.48 5.30 zeus22 376528896 4.46 2.63 zeus05 217669632 4.64 2.71 zeus07 221933568 4.36 2.58 221896704 zeus02 3.82 2.30 213401600 zeus11 4.36 2.61 zeus24 210345984 4.01 2.38 zeus16 213458944 4.21 2.45 zeus05 210403328
locks/test_locks_13_true-unreach-call.c 4.25 2.55 214913024 zeus04 4.05 2.39 zeus19 217427968 4.09 2.45 zeus09 213708800 23.8  12.5  780390400 zeus03 24.9  13.0  zeus15 796286976 24.4  12.9  zeus19 810532864 24.5  13.0  zeus20 804868096 4.64 2.74 zeus09 222789632 4.46 2.60 zeus08 216408064 4.71 2.77 221659136 zeus23 4.24 2.49 215089152 zeus02 3.99 2.36 zeus13 212078592 4.17 2.47 zeus17 213540864 4.41 2.57 zeus23 210501632
locks/test_locks_14_true-unreach-call.c 4.28 2.53 219758592 zeus12 3.99 2.39 zeus04 213229568 4.14 2.43 zeus08 211161088 23.5  12.5  797601792 zeus08 24.9  13.2  zeus12 798007296 25.1  13.3  zeus06 805613568 26.6  14.0  zeus14 817328128 4.66 2.69 zeus02 220033024 4.53 2.68 zeus06 224296960 4.75 2.79 229019648 zeus07 4.34 2.59 212979712 zeus10 4.28 2.53 zeus08 210530304 3.79 2.20 zeus21 212033536 4.44 2.60 zeus05 215056384
locks/test_locks_15_true-unreach-call_false-termination.c 4.41 2.56 218419200 zeus19 4.21 2.44 zeus24 213635072 4.09 2.43 zeus19 211107840 11.0  6.12 391467008 zeus11 13.2  7.16 zeus13 426823680 11.0  6.12 zeus24 410152960 13.7  7.42 zeus09 452923392 4.89 2.94 zeus11 227332096 5.03 2.93 zeus08 222400512 5.04 2.98 222097408 zeus19 4.26 2.50 211189760 zeus05 4.65 2.74 zeus09 215531520 4.09 2.40 zeus22 207257600 4.23 2.47 zeus12 215826432
locks/test_locks_5_true-unreach-call_false-termination.c 3.97 2.38 210137088 zeus23 3.67 2.21 zeus08 203137024 3.86 2.32 zeus16 218144768 8.47 4.74 398630912 zeus08 7.02 4.01 zeus23 343285760 7.45 4.40 zeus04 346132480 7.72 4.35 zeus14 363827200 4.01 2.40 zeus24 211038208 3.90 2.33 zeus16 215511040 3.97 2.42 219156480 zeus14 4.16 2.43 213045248 zeus14 3.92 2.32 zeus12 214286336 3.93 2.31 zeus04 207769600 3.80 2.29 zeus09 211959808
locks/test_locks_6_true-unreach-call_false-termination.c 4.20 2.45 211849216 zeus03 4.15 2.44 zeus05 209313792 4.31 2.50 zeus08 208158720 7.60 4.31 341843968 zeus20 8.41 4.72 zeus09 366505984 7.39 4.18 zeus15 340938752 9.39 5.18 zeus24 396382208 4.17 2.47 zeus10 216850432 4.17 2.49 zeus18 215416832 4.46 2.59 219402240 zeus04 3.93 2.35 213327872 zeus04 3.92 2.32 zeus19 212434944 3.89 2.33 zeus13 207659008 3.88 2.30 zeus12 215986176
locks/test_locks_7_true-unreach-call_false-termination.c 4.11 2.49 212402176 zeus22 3.75 2.25 zeus01 207568896 3.99 2.36 zeus21 215093248 7.85 4.46 343642112 zeus10 7.81 4.44 zeus15 332820480 8.13 4.61 zeus22 348672000 8.47 4.81 zeus01 342843392 4.33 2.53 zeus20 219529216 4.27 2.54 zeus08 217145344 4.20 2.48 213585920 zeus03 4.37 2.62 212480000 zeus12 3.82 2.29 zeus18 208883712 3.91 2.31 zeus18 208580608 4.08 2.41 zeus17 208965632
locks/test_locks_8_true-unreach-call_false-termination.c 4.26 2.52 210698240 zeus10 3.86 2.30 zeus20 210722816 4.40 2.62 zeus23 211636224 7.92 4.50 357031936 zeus10 8.51 4.80 zeus07 339726336 7.81 4.44 zeus17 333746176 7.64 4.33 zeus20 347238400 4.45 2.60 zeus01 215846912 4.07 2.43 zeus18 218943488 4.16 2.45 215158784 zeus24 4.04 2.35 214102016 zeus03 3.97 2.34 zeus06 219086848 4.02 2.41 zeus07 208715776 4.44 2.59 zeus03 209358848
locks/test_locks_9_true-unreach-call.c 4.08 2.43 212975616 zeus13 3.97 2.37 zeus04 213254144 4.10 2.44 zeus12 214536192 12.5  6.83 425037824 zeus17 10.2  5.73 zeus08 414273536 11.6  6.36 zeus17 412766208 10.4  5.82 zeus16 414343168 4.24 2.52 zeus22 220790784 4.24 2.48 zeus19 214671360 4.33 2.57 220573696 zeus07 4.46 2.63 218533888 zeus22 3.98 2.33 zeus10 208130048 3.85 2.27 zeus21 210014208 4.17 2.51 zeus09 209387520
test/programs/benchmarks/ status cputime (s) walltime (s) memUsage host status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) memUsage host status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) memUsage host status cputime (s) walltime (s) memUsage host status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage
total tasks 48 1310 1010 22982533120 48 1250 983 22160699392 48 1280 992 23330029568 48 10800 9400 90593824768 48 10700 9360 90517315584 48 10700 9360 89342783488 48 10700 9360 90697445376 48 2280 1650 37263302656 48 1430 829 34231259136 48 1520 879 34446192640 48 902 614 20843507712 48 936 644 21124780032 48 849 585 20133683200 48 882 603 20898107392
    correct results 48 1310 1010 22982533120 48 1250 983 22160699392 48 1280 992 23330029568 39 2680 1860 48227442688 39 2610 1810 48133353472 39 2610 1810 47025221632 39 2620 1820 48293695488 47 1380 806 32302706688 48 1430 829 34231259136 48 1520 879 34446192640 48 902 614 20843507712 48 936 644 21124780032 48 849 585 20133683200 48 882 603 20898107392
        correct true 30 697 514 13269712896 30 649 487 12878626816 30 647 476 13750738944 22 933 568 25323008000 22 923 559 24986808320 22 919 558 23989493760 22 917 554 24926912512 30 892 511 20060794880 30 846 484 20007718912 30 864 481 19592626176 30 564 386 12386914304 30 545 375 12259381248 30 525 367 11885096960 30 552 380 12420235264
        correct false 18 615 500 9712820224 18 605 496 9282072576 18 631 516 9579290624 17 1740 1290 22904434688 17 1690 1250 23146545152 17 1690 1250 23035727872 17 1710 1260 23366782976 17 489 296 12241911808 18 586 346 14223540224 18 653 398 14853566464 18 338 228 8456593408 18 390 268 8865398784 18 325 219 8248586240 18 330 223 8477872128
    incorrect results 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        incorrect true 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        incorrect false 0 0 0 0 0 0 0 0 0 0 0 0 0 0
score (48 tasks, max score: 78) 78 78 78 61 61 61 61 77 78 78 78 78 78 78
Run set MathSAT5-heaparray.ControlFlow MathSAT5-oldarray.ControlFlow MathSAT5-uf.ControlFlow PRINCESS-heaparray-quantifiers.ControlFlow PRINCESS-heaparray.ControlFlow PRINCESS-oldarray.ControlFlow PRINCESS-uf.ControlFlow SMTInterpol-heaparray.ControlFlow SMTInterpol-oldarray.ControlFlow SMTInterpol-uf.ControlFlow Z3-heaparray-quantifiers.ControlFlow Z3-heaparray.ControlFlow Z3-oldarray.ControlFlow Z3-uf.ControlFlow