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.Simple MathSAT5-oldarray.Simple MathSAT5-uf.Simple PRINCESS-heaparray-quantifiers.Simple PRINCESS-heaparray.Simple PRINCESS-oldarray.Simple PRINCESS-uf.Simple SMTInterpol-heaparray.Simple SMTInterpol-oldarray.Simple SMTInterpol-uf.Simple Z3-heaparray-quantifiers.Simple Z3-heaparray.Simple Z3-oldarray.Simple Z3-uf.Simple
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) 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) 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) memUsage host status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage status cputime (s) walltime (s) host memUsage
ntdrivers/cdaudio_false-unreach-call.i.cil.c 927    877    zeus06 4650668032 12.0  6.42 zeus24 366149632 937   880    zeus16 3114557440 912   853   1590210560 zeus03 911   851   zeus19 1623306240 15.1  8.12 zeus09 466092032 901   844   4511166464 zeus23 902   822    4824887296 zeus23 11.3  6.08 zeus24 361091072 902   824   zeus09 4872732672 902   862    1850347520 zeus08 902   858    zeus04 1807327232 12.7  6.75 zeus03 358313984 911   868    zeus07 1204867072
ntdrivers/diskperf_false-unreach-call.i.cil.c 16.2  8.78 zeus20 532897792 8.50 4.75 zeus10 285859840 16.2 8.82 zeus04 530923520 130   82.8 2904793088 zeus16 118   75.8 zeus10 3609976832 39.4  20.4  zeus16 845996032 170   124   4471230464 zeus15 43.9 22.6  919351296 zeus05 12.7  6.90 zeus09 491208704 37.2 19.2 zeus13 685916160 17.6 9.50 534007808 zeus14 15.6 8.45 zeus12 508788736 8.81 4.94 zeus02 284065792 16.9 9.15 zeus05 529539072
ntdrivers/floppy_false-unreach-call.i.cil.c 904    896    zeus19 3023147008 9.11 4.87 zeus16 315047936 903   891    zeus23 1335054336 80.2 48.5 1573941248 zeus01 901   726   zeus16 10834735104 10.6  5.83 zeus10 410337280 902   798   5349421056 zeus19 59.6 30.5  955875328 zeus17 10.1  5.46 zeus01 328847360 61.4 31.8 zeus24 1237200896 905   897    1719517184 zeus13 913   902    zeus21 1648103424 9.34 4.98 zeus05 303087616 41.6 23.2  zeus05 937512960
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 12.0  6.63 zeus02 455294976 5.65 3.23 zeus14 247640064 12.6 6.94 zeus09 463941632 76.4 40.2 1507913728 zeus08 72.5 38.4 zeus18 1530195968 7.48 4.18 zeus05 349396992 57.3 29.6 1052700672 zeus06 21.2 11.3  517636096 zeus12 6.61 3.75 zeus07 250785792 21.4 11.3 zeus17 558948352 12.2 6.65 444088320 zeus12 12.4 6.72 zeus02 452542464 5.58 3.15 zeus24 238743552 12.4 6.73 zeus21 450347008
ntdrivers/parport_false-unreach-call.i.cil.c 18.6  9.69 zeus23 451448832 11.3  6.03 zeus11 353894400 17.7 9.23 zeus11 457150464 32.4 16.7 557740032 zeus15 30.2 15.8 zeus14 597528576 12.7  6.86 zeus13 453115904 32.1 16.6 605712384 zeus05 20.9 10.8  547151872 zeus04 13.1  6.89 zeus01 362557440 23.3 12.1 zeus04 525795328 18.9 9.86 455331840 zeus23 18.9 9.87 zeus03 449425408 11.3  6.01 zeus02 342630400 19.2 9.98 zeus19 468230144
ntdrivers/cdaudio_true-unreach-call.i.cil.c 19.4  10.4  zeus13 445423616 10.9  5.91 zeus13 340770816 19.4 10.5  zeus09 444833792 901   835   4531884032 zeus12 902   830   zeus07 4533059584 13.1  7.07 zeus12 457281536 902   848   4526182400 zeus07 45.6 23.3  914952192 zeus14 12.3  6.49 zeus01 354488320 43.2 22.2 zeus18 791773184 18.7 10.1  448872448 zeus14 18.9 10.1  zeus04 441192448 10.8  5.82 zeus24 338546688 19.4 10.5  zeus13 442826752
ntdrivers/diskperf_true-unreach-call.i.cil.c 12.8  6.98 zeus19 341377024 8.68 4.84 zeus24 280637440 12.2 6.77 zeus06 334536704 901   835   4567605248 zeus22 901   836   zeus19 4551561216 39.3  20.4  zeus04 853094400 902   836   4533456896 zeus15 45.6 23.3  928202752 zeus05 13.3  7.28 zeus04 487407616 38.9 20.1 zeus17 708489216 11.8 6.61 338784256 zeus20 12.1 6.76 zeus12 343482368 8.82 4.91 zeus07 282923008 11.8 6.59 zeus08 337256448
ntdrivers/floppy2_true-unreach-call.i.cil.c 68.5  46.0  zeus04 1149526016 23.3  12.0  zeus09 523227136 56.1 33.3  zeus03 1019990016 68.3 34.6 954748928 zeus12 902   846   zeus03 4638429184 27.2  14.0  zeus23 688332800 902   797   5022015488 zeus11 210   149    4551532544 zeus16 23.6  12.2  zeus20 554823680 149   98.4 zeus01 3910119424 495   467    1255424000 zeus12 149   121    zeus06 1626214400 21.8  11.2  zeus14 563818496 54.1 31.6  zeus22 1116434432
ntdrivers/floppy_true-unreach-call.i.cil.c 904    895    zeus21 3028602880 9.34 5.02 zeus15 322908160 903   890    zeus12 1212796928 82.4 50.0 1606381568 zeus10 901   728   zeus23 10768592896 10.4  5.67 zeus12 406175744 902   801   5562408960 zeus13 85.0 46.4  1587380224 zeus07 9.17 4.96 zeus14 310759424 108   63.5 zeus14 2190118912 913   904    1530695680 zeus02 913   902    zeus04 1685524480 9.39 5.04 zeus17 323674112 37.1 23.1  zeus02 861753344
ntdrivers/parport_true-unreach-call.i.cil.c 19.1  9.94 zeus09 473669632 13.1  6.86 zeus19 368988160 18.5 9.70 zeus24 442937344 33.6 17.3 576270336 zeus03 31.2 16.1 zeus10 596791296 14.4  7.63 zeus12 473178112 31.8 16.4 619069440 zeus22 21.8 11.4  562855936 zeus03 11.6  6.20 zeus12 351670272 20.5 10.6 zeus05 538468352 19.4 10.0  465747968 zeus13 18.9 9.85 zeus23 463376384 11.5  6.00 zeus19 344174592 18.8 9.78 zeus01 455299072
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 18.0  10.2  zeus17 459145216 16.9  9.16 zeus13 548270080 20.0 11.2  zeus16 586248192 901   807   5404594176 zeus11 902   807   zeus04 5346369536 110    64.5  zeus20 2395029504 902   817   4902457344 zeus03 23.8 12.4  778539008 zeus24 31.7  16.5  zeus24 666669056 44.7 23.0 zeus17 865136640 19.3 11.0  549400576 zeus10 17.9 10.1  zeus19 529592320 16.7  9.26 zeus02 520978432 22.4 12.9  zeus23 582352896
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 11.7  7.14 zeus19 324816896 14.1  7.49 zeus21 483086336 17.6 9.84 zeus02 561201152 902   820   5122707456 zeus23 901   823   zeus06 5051809792 72.8  38.3  zeus09 1313595392 246   188   4534870016 zeus15 18.6 9.89 770875392 zeus13 26.0  13.5  zeus22 580608000 26.8 14.0 zeus14 596496384 34.2 24.9  620298240 zeus05 30.2 22.2  zeus08 617660416 16.7  9.13 zeus09 519860224 16.1 8.84 zeus23 519053312
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 12.0  7.62 zeus20 326721536 14.4  7.79 zeus16 488001536 16.5 9.31 zeus03 552665088 902   822   4935450624 zeus11 902   820   zeus16 4875452416 74.8  39.7  zeus23 1419157504 233   177   4156002304 zeus02 16.1 8.56 556445696 zeus19 26.6  14.0  zeus01 605446144 29.1 15.0 zeus06 681463808 19.6 11.0  541392896 zeus10 20.1 11.4  zeus06 545710080 14.9  8.07 zeus20 490024960 16.2 8.87 zeus02 531947520
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 12.0  7.53 zeus06 341991424 14.2  7.65 zeus23 488357888 16.2 9.10 zeus04 554737664 901   815   5041983488 zeus23 902   819   zeus16 5011316736 75.3  39.7  zeus02 1431441408 225   170   4593528832 zeus02 16.5 8.77 689102848 zeus10 25.6  13.4  zeus02 645382144 30.7 15.9 zeus24 646610944 17.3 9.78 532508672 zeus14 17.5 9.86 zeus12 540266496 17.0  9.25 zeus12 509427712 17.0 9.29 zeus09 557260800
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 18.4  14.9  zeus04 301752320 12.0  6.56 zeus09 465113088 14.6 8.03 zeus12 488009728 80.9 43.3 1464672256 zeus11 84.7 45.6 zeus17 1484824576 54.9  28.4  zeus05 860594176 148   101   3361275904 zeus08 23.0 12.0  745230336 zeus22 17.9  9.52 zeus14 472870912 21.2 11.2 zeus03 489787392 13.4 7.40 455352320 zeus15 12.7 7.02 zeus11 454549504 11.4  6.28 zeus16 443740160 12.6 6.82 zeus20 469417984
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 8.67 5.04 zeus08 289533952 11.9  6.53 zeus15 455663616 13.8 7.67 zeus06 499765248 82.4 44.1 1492873216 zeus02 84.1 44.9 zeus22 1484468224 48.1  24.9  zeus02 888127488 109   66.8 2251460608 zeus24 20.5 10.7  655069184 zeus21 16.7  8.98 zeus19 484536320 20.1 10.8 zeus17 493395968 12.0 6.56 461479936 zeus09 12.1 6.62 zeus02 461492224 12.4  6.76 zeus10 452382720 12.7 7.00 zeus07 473505792
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 45.5  41.6  zeus11 305602560 12.3  6.68 zeus08 456556544 13.7 7.50 zeus22 488718336 79.9 42.5 1494659072 zeus20 78.1 41.5 zeus24 1515171840 46.2  23.8  zeus04 890556416 116   70.3 2528403456 zeus06 24.0 12.6  715296768 zeus20 16.4  8.75 zeus22 485240832 19.7 10.5 zeus11 454508544 13.6 7.33 472915968 zeus09 12.2 6.78 zeus19 460345344 12.9  6.99 zeus19 437776384 12.5 6.86 zeus05 461336576
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 45.8  39.6  zeus09 482365440 12.0  6.49 zeus09 471777280 13.8 7.60 zeus13 488292352 81.5 43.2 1486934016 zeus07 89.0 47.3 zeus01 1506549760 53.1  27.2  zeus15 903708672 120   74.9 2893512704 zeus05 21.7 11.4  692502528 zeus18 18.0  9.51 zeus05 476692480 19.8 10.4 zeus08 434814976 12.4 6.82 453140480 zeus01 12.6 6.93 zeus16 466251776 11.5  6.35 zeus16 445407232 13.0 7.11 zeus22 471101440
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 125    116    zeus15 469581824 18.2  10.0  zeus02 557178880 24.6 13.6  zeus05 647069696 901   824   4737617920 zeus19 902   829   zeus16 4735594496 120    72.8  zeus14 2959011840 902   826   5021782016 zeus16 15.2 8.18 477356032 zeus14 27.6  14.4  zeus14 661942272 38.0 19.6 zeus05 858599424 26.3 16.4  647290880 zeus01 26.0 15.8  zeus09 642220032 17.9  9.85 zeus06 546795520 23.1 12.5  zeus04 643018752
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 117    111    zeus22 386240512 16.4  8.76 zeus09 524308480 16.8 9.32 zeus22 558882816 901   802   5455802368 zeus03 901   805   zeus21 5460242432 80.4  44.0  zeus21 1720750080 901   822   4686999552 zeus20 28.0 14.7  899452928 zeus16 26.9  14.1  zeus01 644931584 38.2 19.7 zeus13 815931392 18.6 10.5  553836544 zeus03 20.8 12.3  zeus16 571412480 904    894    zeus10 900984832 24.3 13.4  zeus22 666681344
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 340    329    zeus11 797462528 22.4  12.1  zeus19 651673600 29.1 16.5  zeus12 753799168 901   812   4891107328 zeus19 901   821   zeus13 4975390720 385    319    zeus06 4629430272 902   816   5012320256 zeus01 16.0 8.54 490754048 zeus06 57.4  30.8  zeus14 1255514112 66.5 35.3 zeus06 1277624320 53.7 39.8  875999232 zeus14 54.8 40.9  zeus14 874610688 29.0  17.6  zeus17 682708992 32.5 20.0  zeus05 768229376
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 13.0  7.63 zeus23 376782848 14.5  7.71 zeus21 501284864 19.7 11.0  zeus09 618319872 901   808   5348171776 zeus13 901   788   zeus09 5312770048 84.0  45.8  zeus10 1682804736 901   824   4693053440 zeus10 27.0 14.1  869040128 zeus06 27.4  14.4  zeus01 593199104 39.8 20.5 zeus17 847618048 28.3 16.9  647376896 zeus05 26.1 15.5  zeus04 635629568 16.2  8.87 zeus05 512892928 22.5 12.5  zeus15 638873600
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 106    95.9  zeus06 806322176 20.7  11.3  zeus17 611266560 31.0 18.4  zeus21 767328256 902   819   4882362368 zeus20 902   821   zeus12 4880883712 373    304    zeus01 4637057024 901   825   4831358976 zeus21 14.9 7.92 445550592 zeus05 45.9  23.5  zeus12 835223552 60.5 31.9 zeus14 1147420672 73.7 60.7  864919552 zeus10 70.3 55.7  zeus07 901476352 22.4  12.4  zeus19 623210496 35.0 22.0  zeus23 781713408
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 72.3  67.7  zeus12 340058112 15.1  8.18 zeus20 519811072 17.8 9.79 zeus03 554319872 161   108   3157078016 zeus14 158   106   zeus10 3639840768 81.8  44.5  zeus22 1663463424 901   818   4759244800 zeus18 32.2 16.6  815742976 zeus11 35.4  18.3  zeus18 792526848 29.8 15.6 zeus03 716521472 18.0 9.92 539041792 zeus06 19.0 10.4  zeus21 534568960 25.9  17.4  zeus07 597364736 17.2 9.34 zeus08 552153088
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 127    120    zeus19 437846016 17.9  10.0  zeus16 543010816 16.9 9.45 zeus10 558522368 901   826   4843175936 zeus24 902   828   zeus15 4847943680 91.3  52.3  zeus23 2151649280 901   823   4952956928 zeus06 15.4 8.24 483315712 zeus18 24.7  12.9  zeus08 542502912 31.9 16.5 zeus13 724627456 21.0 13.1  571695104 zeus06 22.2 13.9  zeus17 570884096 15.7  8.66 zeus15 495333376 18.8 10.2  zeus17 565043200
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 191    185    zeus17 393621504 15.9  8.59 zeus11 536846336 18.4 10.1  zeus15 571363328 901   803   5558435840 zeus16 901   808   zeus04 5514067968 103    57.8  zeus03 1934770176 581   505   4691066880 zeus07 26.0 13.5  867549184 zeus07 37.7  19.4  zeus05 833347584 42.6 21.9 zeus02 874635264 20.9 12.1  571166720 zeus09 20.4 11.9  zeus24 564072448 17.0  9.14 zeus16 518938624 21.6 11.9  zeus06 604708864
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 147    138    zeus06 496246784 16.2  8.90 zeus01 532410368 21.0 11.7  zeus08 604258304 902   825   4841373696 zeus09 902   825   zeus02 4872097792 137    84.6  zeus08 2569793536 901   822   4989640704 zeus22 21.1 11.1  768630784 zeus24 28.8  14.9  zeus16 718053376 36.2 18.8 zeus16 817209344 19.6 11.4  573394944 zeus01 18.2 10.7  zeus13 547299328 18.9  11.0  zeus15 545021952 18.1 9.95 zeus23 552624128
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 48.6  41.3  zeus04 475688960 20.1  10.9  zeus01 592715776 27.7 15.6  zeus18 763138048 901   817   4884844544 zeus14 901   822   zeus17 4957011968 412    341    zeus10 4631703552 902   822   5044084736 zeus22 15.0 8.14 466636800 zeus02 43.3  22.2  zeus08 870367232 58.8 30.1 zeus05 1194196992 51.8 37.4  901349376 zeus10 54.7 40.4  zeus01 887320576 25.5  14.4  zeus10 607248384 38.3 24.3  zeus18 835477504
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 69.2  61.4  zeus03 469319680 17.6  9.45 zeus09 527536128 20.1 11.3  zeus17 592908288 901   823   4658802688 zeus07 901   831   zeus03 4656128000 122    74.4  zeus20 2312728576 901   822   4996509696 zeus09 15.5 8.30 458444800 zeus20 33.2  17.2  zeus09 774348800 34.1 17.6 zeus05 791388160 19.4 11.2  519667712 zeus13 18.8 10.5  zeus02 535171072 18.6  10.5  zeus02 527253504 22.3 12.2  zeus08 620195840
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 33.5  24.5  zeus11 504139776 25.4  15.2  zeus17 686067712 44.0 32.8  zeus22 888094720 901   811   5282521088 zeus21 902   810   zeus10 5270847488 744    663    zeus10 4953235456 902   819   4849238016 zeus23 51.2 27.1  1594884096 zeus08 30.7  15.9  zeus08 841977856 93.8 58.2 zeus19 2447761408 455   442    878354432 zeus11 595   581    zeus12 914817024 21.4  13.1  zeus03 504094720 349   337    zeus06 998154240
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 111    101    zeus06 795529216 124    113    zeus24 2370252800 36.6 25.3  zeus09 840929280 901   812   5105049600 zeus20 901   812   zeus06 5098020864 265    204    zeus17 4589625344 902   820   4799385600 zeus06 18.4 9.70 770564096 zeus18 70.3  43.3  zeus09 1574363136 43.5 22.2 zeus20 919633920 93.3 79.8  839077888 zeus24 80.8 69.3  zeus20 741343232 33.0  22.5  zeus14 692391936 903   887    zeus16 1386434560
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 177    164    zeus03 864899072 28.7  19.1  zeus10 712728576 113   100    zeus17 917463040 902   812   4988989440 zeus20 902   814   zeus21 4964605952 229    165    zeus14 4606259200 902   824   4786495488 zeus16 26.2 14.0  1039626240 zeus04 144    116    zeus16 3419414528 72.1 40.3 zeus15 1459003392 47.0 34.6  746356736 zeus12 43.2 32.7  zeus10 733659136 21.5  13.3  zeus02 479633408 903   889    zeus13 2358165504
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 342    329    zeus20 835203072 31.7  22.0  zeus05 768942080 37.1 26.4  zeus08 837529600 901   808   4998721536 zeus10 902   814   zeus16 5045981184 218    157    zeus15 4543483904 902   824   4804771840 zeus19 43.6 23.2  1323663360 zeus06 45.2  23.4  zeus03 950165504 73.5 41.6 zeus16 1614647296 224   212    821022720 zeus22 227   216    zeus07 821817344 21.8  12.9  zeus19 495464448 902   886    zeus05 1575874560
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 142    131    zeus18 802185216 25.0  14.0  zeus09 708706304 46.1 28.9  zeus19 829390848 901   836   4883382272 zeus17 901   835   zeus23 4882784256 902    833    zeus11 4777336832 901   830   4847804416 zeus01 35.3 18.9  1217622016 zeus06 47.5  24.7  zeus17 1115283456 87.7 48.9 zeus10 1630408704 901   887    1060884480 zeus22 902   886    zeus06 1023045632 46.7  34.1  zeus11 770187264 133   116    zeus13 926572544
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 14.6  8.83 zeus11 386936832 22.5  12.6  zeus20 675270656 60.8 44.8  zeus12 839147520 901   815   4856549376 zeus02 902   820   zeus07 4909428736 902    827    zeus12 4819214336 901   825   4841684992 zeus10 31.3 16.5  986714112 zeus03 60.8  32.0  zeus05 1263566848 69.8 38.7 zeus09 1353113600 902   887    994508800 zeus14 902   887    zeus24 1018638336 69.4  57.3  zeus02 802099200 526   507    zeus02 1298894848
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 224    210    zeus02 1129201664 31.7  18.9  zeus09 774201344 90.7 75.5  zeus20 863756288 902   827   4885520384 zeus17 902   823   zeus17 4886253568 902    834    zeus17 4558684160 902   825   4593135616 zeus07 297   254    4701966336 zeus04 51.7  27.1  zeus24 1114963968 478   421   zeus24 4706127872 902   887    972836864 zeus07 902   889    zeus02 1006825472 39.7  24.5  zeus08 813498368 910   896    zeus22 5822046208
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 82.1  72.5  zeus02 738873344 37.9  23.7  zeus22 761090048 330   312    zeus05 857227264 902   833   4867026944 zeus09 901   832   zeus02 4879826944 903    824    zeus02 5219389440 902   825   4721795072 zeus03 39.4 20.5  1182461952 zeus09 106    72.4  zeus13 2193305600 88.9 53.1 zeus22 1658974208 902   883    1000443904 zeus20 902   885    zeus15 1043337216 98.4  84.2  zeus01 824008704 34.4 24.4  zeus24 664326144
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 27.5  17.0  zeus22 537468928 237    222    zeus14 4507557888 202   185    zeus06 901177344 902   841   4643782656 zeus24 901   838   zeus06 4649410560 902    831    zeus10 4779941888 901   824   4856119296 zeus15 42.8 24.8  2384502784 zeus13 52.0  26.8  zeus12 1091727360 99.2 56.8 zeus19 2091237376 901   886    1095671808 zeus21 901   887    zeus21 1239605248 35.0  20.5  zeus21 757219328 370   353    zeus12 923783168
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 43.6  33.6  zeus10 520605696 63.4  49.1  zeus08 1296519168 104   86.4  zeus15 972476416 902   834   4818366464 zeus22 901   836   zeus23 4832272384 902    816    zeus06 4878495744 901   821   4685758464 zeus12 27.3 14.1  882532352 zeus21 54.5  27.9  zeus12 986304512 90.4 54.4 zeus12 1593724928 818   798    930623488 zeus11 827   804    zeus07 983302144 763    745    zeus13 948269056 74.0 55.1  zeus01 914325504
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 23.5  13.5  zeus16 496259072 111    97.5  zeus20 1388314624 121   103    zeus02 1022214144 902   834   4769570816 zeus09 902   836   zeus02 4774600704 902    830    zeus09 4802260992 902   828   4857294848 zeus15 24.9 13.0  792645632 zeus11 48.6  25.0  zeus16 944369664 59.7 30.9 zeus24 1179209728 608   586    976814080 zeus05 777   756    zeus15 972734464 28.5  17.4  zeus17 714203136 108   96.2  zeus11 850931712
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 103    93.8  zeus12 720805888 58.2  43.3  zeus14 879468544 97.7 79.5  zeus06 941498368 902   833   4859654144 zeus03 902   833   zeus02 4854427648 902    826    zeus08 4748800000 901   821   4728836096 zeus24 31.9 16.5  1105682432 zeus16 170    126    zeus18 3094315008 165   126   zeus05 2718666752 907   893    2494066688 zeus17 441   423    zeus20 979873792 394    378    zeus06 843730944 902   887    zeus10 973430784
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 31.5  20.0  zeus21 542232576 119    105    zeus13 2431791104 62.6 51.2  zeus07 836173824 902   837   4652150784 zeus05 901   837   zeus01 4629151744 901    831    zeus15 4723437568 902   827   4610457600 zeus07 22.4 11.7  780251136 zeus24 68.4  38.2  zeus07 1305247744 149   106   zeus03 3272679424 906   894    1576390656 zeus11 910   897    zeus12 1890308096 34.0  20.5  zeus09 782262272 901   887    zeus14 1011425280
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 34.3  24.8  zeus08 481001472 44.3  30.2  zeus16 818262016 153   135    zeus05 929140736 902   832   4832940032 zeus16 902   835   zeus08 4846366720 902    824    zeus07 4748963840 902   822   4861038592 zeus22 26.3 13.7  884428800 zeus17 97.5  60.5  zeus08 2152640512 113   75.6 zeus22 1843367936 902   889    872992768 zeus10 902   883    zeus12 967741440 87.1  73.8  zeus20 786030592 46.6 30.7  zeus10 791289856
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 39.9  28.9  zeus12 689766400 641    625    zeus21 2954956800 91.1 74.4  zeus03 859017216 902   830   4705550336 zeus24 902   831   zeus05 4718997504 902    826    zeus22 4654555136 902   825   4621742080 zeus13 106   75.0  4560662528 zeus14 169    126    zeus20 4446781440 205   158   zeus01 4619730944 903   888    1959292928 zeus08 902   890    zeus10 1420435456 38.2  24.4  zeus13 730836992 901   887    zeus22 1281474560
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 38.5  26.1  zeus10 655724544 146    131    zeus09 1417101312 59.2 44.1  zeus07 920854528 902   829   4587806720 zeus24 902   825   zeus10 4592447488 447    388    zeus07 4571111424 902   824   4802269184 zeus02 62.3 40.2  3840966656 zeus10 76.8  41.2  zeus07 1663795200 201   156   zeus18 4569841664 913   900    5424869376 zeus13 903   888    zeus18 1223081984 902    889    zeus18 910798848 903   887    zeus13 1917026304
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 56.2  45.2  zeus18 889503744 474    455    zeus01 1205260288 299   280    zeus22 1118068736 902   824   4902088704 zeus10 902   825   zeus05 4916973568 902    835    zeus22 4577857536 902   830   4595253248 zeus21 144   111    4572553216 zeus04 63.1  32.5  zeus23 1001648128 356   304   zeus13 4731232256 913   900    2084941824 zeus21 903   890    zeus20 1996029952 608    592    zeus09 900788224 904   891    zeus23 2439290880
test/programs/benchmarks/ 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) 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) 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 46 5950   5520   34423492608 46 2640 2220 37716484096 46 5210 4640 35940429824 46 31700 28600 182713806848 46 34100 30800 206164508672 46 15400 13300 126951026688 46 32700 29500 200016973824 46 2880 2060 61577089024 46 2050 1220 45952913408 46 4540 3260 73156911104 46 16000 15500 45124194304 46 15500 14900 39743107072 46 4580 4160 26512846848 46 11300 10700 44232208384
    correct results 6 175   118   3406884864 36 2520 2160 34311360512 41 2430 1960 29377933312 6 562 321 10604130304 6 566 324 11161051136 24 4430 3300 64259088384 9 1840 1380 30062821376 12 633 370 13998772224 36 1920 1160 42099273728 43 3590 2420 67219914752 30 3290 2980 19565654016 31 3690 3350 20860301312 34 2660 2320 21321084928 34 2230 1860 23338643456
        correct true 3 101   63.4 1936326656 17 2220 2000 24356491264 20 2040 1740 17173520384 0 0 5 1900 1580 23263715328 0 4 387 242 7982067712 17 1360 860 29159870464 21 2790 2000 50009862144 9 2770 2640 7235330048 10 3170 3020 8558436352 16 2340 2130 11844718592 12 1760 1590 10126548992
        correct false 3 74.0 55.1 1470558208 19 303 164 9954869248 21 398 223 12204412928 6 562 321 10604130304 6 566 324 11161051136 19 2530 1730 40995373056 9 1840 1380 30062821376 8 246 128 6016704512 19 567 296 12939403264 22 809 421 17210052608 21 523 340 12330323968 21 515 334 12301864960 18 321 182 9476366336 22 467 265 13212094464
    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 (46 tasks, max score: 68) 9 53 61 6 6 29 9 16 53 64 39 41 50 46
Run set MathSAT5-heaparray.Simple MathSAT5-oldarray.Simple MathSAT5-uf.Simple PRINCESS-heaparray-quantifiers.Simple PRINCESS-heaparray.Simple PRINCESS-oldarray.Simple PRINCESS-uf.Simple SMTInterpol-heaparray.Simple SMTInterpol-oldarray.Simple SMTInterpol-uf.Simple Z3-heaparray-quantifiers.Simple Z3-heaparray.Simple Z3-oldarray.Simple Z3-uf.Simple