Tool UltimateAutomizer r14553 CPAchecker 1.4-svn 17283M
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 3.13.0-57-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz with 32 cores, frequency: 2.6 GHz; RAM: 135 GB
Date of execution 2015-07-14 10:02:44 CEST 2015-07-14 13:21:15 CEST
Run set UltimateAutomizer Verification Predicate (LA) Validation
Options -disable-java-assertions -heap 13000M -predicateAnalysis-LA -setprop cfa.useMultiEdges=false -setprop cpa.predicate.solver=MATHSAT5 -setprop cpa.value.optimizeBooleanVariables=false -setprop cfa.simplifyCfa=false -setprop cfa.allowBranchSwapping=false -setprop cpa.predicate.ignoreIrrelevantVariables=false -setprop counterexample.export.assumptions.assumeLinearArithmetics=true -setprop coverage.enabled=false -setprop coverage.mode=TRANSFER -setprop coverage.export=true -setprop coverage.file=coverage.info -setprop analysis.traversal.byAutomatonVariable=__DISTANCE_TO_VIOLATION -setprop cpa.automaton.treatErrorsAsTargets=false -setprop WitnessAutomaton.cpa.automaton.treatErrorsAsTargets=true -setprop parser.transformTokensToLines=false -setprop spec.matchOriginLine=true -setprop spec.matchOffset=true -setprop spec.matchAssumeCase=true -setprop spec.matchSourcecodeData=false -setprop spec.strictMatching=false -setprop cpa.composite.inCPAEnabledAnalysis=true -skipRecursion -spec test/results/ultimateautomizer-no-mem.2015-07-14_1002.logfiles/UltimateAutomizer.${sourcefile_name}.files/workspace/UltimateAutomizer/witness.graphml
../../sv-benchmarks/c/ status cputime walltime host memUsage status cputime walltime host memUsage Line coverage Condition coverage
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-termination.cil.c false(reach) 79.236s 55.103s zeus04 1958678528 false(reach) 12.259s 6.898s zeus01 386097152 0.406 0.457
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c false(reach) 47.100s 28.290s zeus22 1295781888 timeout 907.178s 888.712s zeus23 3362947072 0.720 0.789
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c false(reach) 61.004s 38.035s zeus12 1315217408 timeout 906.919s 888.177s zeus05 3472801792 0.519 0.561
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c false(reach) 28.003s 16.059s zeus14 736378880 false(reach) 8.283s 4.908s zeus24 280391680 0.821 0.798
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(reach) 13.748s 7.847s zeus02 326664192 false(reach) 22.627s 12.370s zeus17 549187584 1.000 1.000
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(reach) 13.388s 7.747s zeus08 330883072 false(reach) 21.214s 11.617s zeus14 545976320 1.000 1.000
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c false(reach) 16.627s 9.766s zeus24 330264576 false(reach) 23.543s 12.742s zeus23 578297856 1.000 1.000
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(reach) 16.025s 9.424s zeus04 326508544 false(reach) 21.451s 11.777s zeus09 547868672 1.000 1.000
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(reach) 9.954s 5.976s zeus05 318812160 false(reach) 14.163s 8.316s zeus04 362319872 1.000 1.000
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c false(reach) 26.953s 15.937s zeus07 745771008 false(reach) 24.428s 13.363s zeus22 688320512 1.000 1.000
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c false(reach) 23.902s 13.660s zeus19 484642816 false(reach) 26.187s 14.110s zeus20 680747008 1.000 1.000
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c false(reach) 20.011s 11.403s zeus24 461692928 false(reach) 20.740s 11.295s zeus20 520216576 1.000 1.000
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c false(reach) 18.422s 10.308s zeus14 453361664 false(reach) 16.340s 9.053s zeus07 436158464 1.000 1.000
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(reach) 10.949s 6.260s zeus11 320356352 false(reach) 16.729s 9.307s zeus22 440193024 1.000 1.000
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(reach) 10.957s 6.309s zeus18 327094272 false(reach) 17.014s 9.472s zeus07 453746688 1.000 1.000
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(reach) 7.881s 4.662s zeus10 287744000 false(reach) 6.851s 4.093s zeus23 254062592 0.992 0.526
locks/test_locks_14_false-unreach-call.c false(reach) 7.817s 4.709s zeus01 282546176 false(reach) 6.022s 3.686s zeus09 226750464 0.985 0.395
locks/test_locks_15_false-unreach-call.c false(reach) 7.218s 4.229s zeus13 284385280 false(reach) 7.236s 4.613s zeus04 225800192 0.986 0.391
eca-rers2012/Problem01_label15_false-unreach-call.c false(reach) 39.609s 25.097s zeus03 760832000 timeout 902.177s 875.177s zeus23 5133684736 0.949 1.000
eca-rers2012/Problem01_label20_false-unreach-call.c false(reach) 39.734s 25.408s zeus23 848531456 timeout 901.318s 871.624s zeus19 5110726656 0.949 1.000
eca-rers2012/Problem01_label21_false-unreach-call.c false(reach) 41.637s 26.367s zeus09 945893376 timeout 901.881s 875.973s zeus11 5112467456 0.949 1.000
eca-rers2012/Problem01_label32_false-unreach-call.c false(reach) 46.598s 30.522s zeus19 1275506688 timeout 901.236s 871.896s zeus20 5111529472 0.949 1.000
eca-rers2012/Problem01_label33_false-unreach-call.c false(reach) 38.111s 23.937s zeus07 765435904 timeout 901.080s 873.432s zeus20 5085458432 0.949 1.000
eca-rers2012/Problem01_label35_false-unreach-call.c false(reach) 36.475s 22.829s zeus10 766943232 timeout 901.598s 874.935s zeus13 4942675968 0.963 1.000
eca-rers2012/Problem01_label37_false-unreach-call.c false(reach) 40.576s 25.290s zeus16 925679616 timeout 901.373s 874.092s zeus23 5091344384 0.949 1.000
eca-rers2012/Problem01_label38_false-unreach-call.c false(reach) 39.818s 25.271s zeus21 767938560 timeout 902.397s 875.198s zeus14 5125246976 0.949 1.000
eca-rers2012/Problem01_label44_false-unreach-call.c false(reach) 39.269s 24.423s zeus03 756781056 timeout 901.334s 873.524s zeus15 5129728000 1.000 1.000
eca-rers2012/Problem01_label47_false-unreach-call.c false(reach) 38.697s 24.894s zeus03 756387840 timeout 901.944s 871.129s zeus14 5171806208 0.949 1.000
eca-rers2012/Problem01_label50_false-unreach-call.c false(reach) 32.606s 20.089s zeus14 753741824 timeout 901.252s 874.864s zeus17 5118042112 0.949 1.000
eca-rers2012/Problem01_label56_false-unreach-call.c false(reach) 42.572s 27.007s zeus19 890949632 timeout 900.910s 872.888s zeus01 5106208768 0.949 1.000
eca-rers2012/Problem01_label57_false-unreach-call.c false(reach) 39.457s 25.380s zeus19 765935616 timeout 901.865s 874.666s zeus05 5031743488 0.949 1.000
eca-rers2012/Problem02_label13_false-unreach-call.c false(reach) 33.032s 20.622s zeus06 772460544 timeout 900.927s 872.926s zeus24 5207801856 0.816 0.998
eca-rers2012/Problem02_label16_false-unreach-call.c false(reach) 31.826s 19.500s zeus04 481366016 timeout 902.468s 874.428s zeus19 5316018176 0.983 1.000
eca-rers2012/Problem02_label43_false-unreach-call.c false(reach) 30.741s 19.575s zeus04 571953152 timeout 901.103s 873.342s zeus04 5202829312 1.000 1.000
eca-rers2012/Problem02_label44_false-unreach-call.c false(reach) 30.131s 17.331s zeus12 737792000 timeout 900.967s 873.635s zeus10 5338025984 0.983 1.000
eca-rers2012/Problem02_label45_false-unreach-call.c false(reach) 43.414s 27.565s zeus22 888119296 timeout 902.599s 877.134s zeus10 5140975616 0.825 0.998
eca-rers2012/Problem02_label50_false-unreach-call.c false(reach) 34.274s 21.231s zeus22 767381504 timeout 902.392s 875.656s zeus17 5188730880 0.965 1.000
eca-rers2012/Problem02_label59_false-unreach-call.c false(reach) 34.836s 21.888s zeus02 779153408 timeout 902.055s 875.333s zeus10 5220872192 0.816 0.998
eca-rers2012/Problem03_label13_false-unreach-call.c false(reach) 154.469s 113.215s zeus23 5455257600 timeout 901.294s 863.760s zeus03 5483966464 0.635 0.998
eca-rers2012/Problem03_label27_false-unreach-call.c false(reach) 191.846s 138.750s zeus21 5528915968 timeout 901.281s 865.069s zeus02 5503971328 0.839 0.999
eca-rers2012/Problem03_label31_false-unreach-call.c false(reach) 575.244s 384.052s zeus17 8570417152 timeout 902.205s 861.954s zeus04 5384134656 0.635 0.998
eca-rers2012/Problem03_label37_false-unreach-call.c false(reach) 151.529s 114.555s zeus18 5039132672 timeout 901.308s 862.860s zeus19 5917372416 0.985 1.000
eca-rers2012/Problem03_label50_false-unreach-call.c false(reach) 96.282s 68.482s zeus09 4293742592 timeout 901.467s 866.024s zeus21 5478367232 0.635 0.998
eca-rers2012/Problem04_label04_false-unreach-call.c false(reach) 763.190s 650.533s zeus15 5382213632 timeout 926.137s 780.674s zeus17 7151878144 0.988 1.000
eca-rers2012/Problem04_label06_false-unreach-call.c false(reach) 573.179s 490.421s zeus09 5364326400 timeout 921.231s 771.775s zeus11 6840475648 0.988 1.000
eca-rers2012/Problem04_label09_false-unreach-call.c false(reach) 741.152s 643.654s zeus15 5168873472 timeout 926.457s 782.722s zeus21 7451942912 0.988 1.000
eca-rers2012/Problem04_label11_false-unreach-call.c false(reach) 557.775s 467.210s zeus02 6006652928 timeout 922.137s 780.458s zeus07 7256809472 0.988 1.000
eca-rers2012/Problem04_label12_false-unreach-call.c false(reach) 552.952s 472.005s zeus21 5268471808 timeout 921.450s 767.451s zeus12 7276109824 0.988 1.000
eca-rers2012/Problem04_label13_false-unreach-call.c false(reach) 584.575s 505.199s zeus21 5141667840 timeout 924.569s 774.301s zeus22 7335444480 0.988 1.000
eca-rers2012/Problem04_label14_false-unreach-call.c false(reach) 666.561s 558.561s zeus09 5769797632 timeout 925.424s 782.003s zeus18 7385362432 0.988 1.000
eca-rers2012/Problem04_label15_false-unreach-call.c false(reach) 706.373s 604.589s zeus12 5190324224 timeout 925.559s 791.514s zeus22 7573745664 0.988 1.000
eca-rers2012/Problem04_label17_false-unreach-call.c false(reach) 623.902s 528.330s zeus14 5612916736 timeout 926.896s 778.337s zeus07 7301816320 0.988 1.000
eca-rers2012/Problem04_label18_false-unreach-call.c false(reach) 598.995s 503.113s zeus01 5582376960 timeout 911.215s 839.461s zeus15 6187081728 0.987 1.000
eca-rers2012/Problem04_label19_false-unreach-call.c false(reach) 623.624s 532.788s zeus06 5286109184 timeout 927.974s 789.748s zeus13 7557222400 0.988 1.000
eca-rers2012/Problem04_label26_false-unreach-call.c false(reach) 604.527s 509.428s zeus16 5533589504 timeout 919.612s 783.780s zeus09 6956032000 0.988 1.000
eca-rers2012/Problem04_label27_false-unreach-call.c false(reach) 595.617s 512.826s zeus23 5193854976 timeout 977.548s 866.896s zeus04 6722105344 0.988 1.000
eca-rers2012/Problem04_label31_false-unreach-call.c false(reach) 648.318s 540.642s zeus06 5690544128 timeout 927.029s 770.877s zeus21 7208382464 0.988 1.000
eca-rers2012/Problem04_label32_false-unreach-call.c false(reach) 525.474s 452.777s zeus24 5072572416 timeout 926.197s 778.318s zeus07 7303196672 0.988 1.000
eca-rers2012/Problem04_label35_false-unreach-call.c false(reach) 556.791s 478.200s zeus14 4949164032 timeout 993.987s 871.291s zeus04 6693167104 0.988 1.000
eca-rers2012/Problem04_label36_false-unreach-call.c false(reach) 673.142s 578.538s zeus12 5152739328 timeout 927.984s 774.533s zeus11 7070208000 0.988 1.000
eca-rers2012/Problem04_label38_false-unreach-call.c false(reach) 561.815s 480.985s zeus14 5131665408 timeout 927.131s 781.124s zeus12 7027724288 0.988 1.000
eca-rers2012/Problem04_label39_false-unreach-call.c false(reach) 613.231s 523.412s zeus12 5094731776 timeout 930.427s 782.710s zeus22 7094112256 0.988 1.000
eca-rers2012/Problem04_label40_false-unreach-call.c false(reach) 655.626s 559.688s zeus04 5166129152 timeout 925.717s 790.961s zeus18 7422394368 0.988 1.000
eca-rers2012/Problem04_label45_false-unreach-call.c false(reach) 583.892s 505.287s zeus01 5104824320 timeout 923.971s 783.022s zeus16 7032303616 0.988 1.000
eca-rers2012/Problem04_label52_false-unreach-call.c false(reach) 615.150s 520.433s zeus21 5410951168 timeout 926.437s 772.719s zeus20 7288619008 0.988 1.000
eca-rers2012/Problem04_label55_false-unreach-call.c false(reach) 624.695s 532.755s zeus13 5251268608 timeout 924.644s 778.435s zeus16 7121813504 0.988 1.000
eca-rers2012/Problem04_label58_false-unreach-call.c false(reach) 663.533s 565.429s zeus17 5157019648 timeout 930.320s 777.940s zeus02 7108055040 0.988 1.000
eca-rers2012/Problem10_label12_false-unreach-call.c false(reach) 146.515s 130.788s zeus22 1296908288 timeout 901.116s 878.608s zeus01 4633882624 0.745 0.578
eca-rers2012/Problem10_label15_false-unreach-call.c false(reach) 33.653s 20.025s zeus14 738967552 timeout 901.208s 875.864s zeus13 4761604096 1.000 1.000
eca-rers2012/Problem10_label29_false-unreach-call.c false(reach) 43.677s 29.753s zeus09 747122688 timeout 901.275s 878.266s zeus13 4645085184 1.000 1.000
eca-rers2012/Problem10_label41_false-unreach-call.c false(reach) 207.336s 186.688s zeus04 1303371776 timeout 901.076s 877.548s zeus06 4664180736 1.000 1.000
eca-rers2012/Problem10_label42_false-unreach-call.c false(reach) 29.370s 18.393s zeus21 610582528 timeout 902.468s 878.071s zeus22 5120180224 1.000 1.000
eca-rers2012/Problem10_label46_false-unreach-call.c false(reach) 12.618s 7.418s zeus07 325750784 timeout 901.360s 876.858s zeus22 5146771456 1.000 1.000
eca-rers2012/Problem10_label48_false-unreach-call.c false(reach) 106.894s 90.190s zeus15 1265774592 timeout 900.961s 878.705s zeus17 4631146496 0.844 0.688
eca-rers2012/Problem10_label55_false-unreach-call.c false(reach) 33.664s 20.076s zeus14 737759232 timeout 902.143s 876.554s zeus09 4881117184 1.000 1.000
eca-rers2012/Problem10_label57_false-unreach-call.c false(reach) 49.841s 34.659s zeus14 757747712 timeout 901.113s 878.030s zeus14 4785262592 0.984 1.000
eca-rers2012/Problem11_label08_false-unreach-call.c false(reach) 617.141s 592.317s zeus18 2435305472 timeout 901.514s 875.941s zeus09 5181607936 0.609 0.459
eca-rers2012/Problem11_label15_false-unreach-call.c false(reach) 792.981s 772.714s zeus17 1324036096 timeout 901.012s 872.733s zeus02 5210787840 1.000 1.000
eca-rers2012/Problem11_label42_false-unreach-call.c false(reach) 267.573s 246.109s zeus22 2414243840 timeout 901.224s 875.346s zeus12 5040545792 1.000 1.000
eca-rers2012/Problem11_label49_false-unreach-call.c false(reach) 873.521s 850.048s zeus20 2484174848 timeout 901.034s 875.690s zeus08 4847624192 1.000 1.000
eca-rers2012/Problem11_label58_false-unreach-call.c false(reach) 50.120s 33.698s zeus16 1295515648 timeout 901.176s 873.828s zeus02 5287161856 1.000 1.000
eca-rers2012/Problem12_label40_false-unreach-call.c false(reach) 313.497s 258.845s zeus10 5322661888 timeout 930.964s 843.912s zeus03 7846973440 1.000 1.000
eca-rers2012/Problem14_label10_false-unreach-call.c false(reach) 80.006s 60.093s zeus19 2258575360 timeout 901.329s 868.899s zeus11 5311451136 1.000 1.000
eca-rers2012/Problem14_label11_false-unreach-call.c false(reach) 87.315s 62.983s zeus08 2369634304 timeout 901.780s 867.055s zeus21 5343694848 1.000 1.000
eca-rers2012/Problem14_label12_false-unreach-call.c false(reach) 91.318s 69.194s zeus16 2365841408 timeout 901.049s 871.429s zeus24 5121085440 0.961 1.000
eca-rers2012/Problem14_label13_false-unreach-call.c false(reach) 97.799s 75.076s zeus14 2371047424 timeout 901.183s 865.814s zeus16 5371461632 1.000 1.000
eca-rers2012/Problem14_label27_false-unreach-call.c false(reach) 79.184s 60.913s zeus10 2263597056 timeout 902.430s 868.777s zeus06 5316993024 1.000 1.000
eca-rers2012/Problem14_label28_false-unreach-call.c false(reach) 98.122s 78.463s zeus20 2405339136 timeout 901.975s 873.242s zeus09 5197541376 0.961 1.000
eca-rers2012/Problem14_label31_false-unreach-call.c false(reach) 74.793s 54.732s zeus11 2443706368 timeout 902.693s 869.269s zeus18 5373726720 1.000 1.000
eca-rers2012/Problem14_label37_false-unreach-call.c false(reach) 82.175s 58.801s zeus16 2382032896 timeout 901.406s 867.632s zeus04 5268697088 1.000 1.000
eca-rers2012/Problem14_label39_false-unreach-call.c false(reach) 106.331s 81.451s zeus16 2395926528 timeout 901.093s 868.116s zeus23 5237276672 1.000 1.000
eca-rers2012/Problem14_label40_false-unreach-call.c false(reach) 98.127s 74.992s zeus18 2390265856 timeout 901.035s 866.736s zeus08 5371187200 1.000 1.000
eca-rers2012/Problem14_label44_false-unreach-call.c false(reach) 107.600s 84.057s zeus15 2403721216 timeout 901.211s 863.001s zeus14 5420658688 1.000 1.000
eca-rers2012/Problem14_label52_false-unreach-call.c false(reach) 215.658s 194.281s zeus07 2380341248 timeout 901.237s 868.435s zeus15 5200416768 1.000 1.000
eca-rers2012/Problem14_label54_false-unreach-call.c false(reach) 111.661s 84.202s zeus15 2407317504 timeout 901.185s 866.678s zeus10 5407252480 0.961 1.000
eca-rers2012/Problem14_label56_false-unreach-call.c false(reach) 97.177s 74.386s zeus20 2386677760 timeout 901.355s 866.307s zeus15 5332094976 1.000 1.000
heap-manipulation/merge_sort_false-unreach-call.i false(reach) 15.085s 9.762s zeus24 448163840 false(reach) 6.644s 4.054s zeus02 243957760 1.000 1.000
list-properties/alternating_list_false-unreach-call.i false(reach) 7.049s 4.097s zeus07 280969216 false(reach) 6.011s 3.661s zeus06 240254976 0.997 1.000
list-properties/list_false-unreach-call.i false(reach) 57.855s 48.150s zeus17 1265684480 false(reach) 5.845s 3.706s zeus15 226971648 0.997 1.000
list-properties/list_flag_false-unreach-call.i false(reach) 9.446s 5.650s zeus09 303349760 false(reach) 5.924s 3.599s zeus16 229961728 0.997 1.000
list-properties/list_search_false-unreach-call.i false(reach) 459.161s 448.491s zeus05 1998204928 false(reach) 6.699s 4.035s zeus19 242995200 1.000 1.000
list-properties/simple_false-unreach-call.i false(reach) 8.404s 5.060s zeus06 306159616 false(reach) 5.657s 3.529s zeus13 226316288 0.997 1.000
list-properties/splice_false-unreach-call.i false(reach) 8.122s 4.742s zeus10 288444416 false(reach) 6.840s 4.216s zeus19 244137984 0.997 1.000
ldv-regression/1_3.c_false-unreach-call.i false(reach) 6.718s 4.084s zeus09 283181056 false(reach) 4.295s 2.804s zeus04 205369344 0.950 1.000
ldv-regression/alt_test.c_false-unreach-call.i false(reach) 7.472s 4.580s zeus01 288161792 false(reach) 6.239s 3.747s zeus23 245121024 0.997 1.000
ldv-regression/callfpointer.c_false-unreach-call.i false(reach) 5.694s 3.414s zeus22 232902656 false(reach) 4.294s 2.800s zeus04 198623232 0.800 0.750
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(reach) 6.195s 3.623s zeus23 284196864 false(reach) 3.964s 2.607s zeus15 196493312 0.778 0.500
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(reach) 7.116s 4.266s zeus16 281751552 false(reach) 4.074s 2.584s zeus23 198668288 0.833 0.500
ldv-regression/recursive_list.c_false-unreach-call.i false(reach) 7.238s 4.363s zeus15 272474112 false(reach) 4.101s 2.643s zeus22 211013632 1.000 1.000
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(reach) 7.055s 4.299s zeus09 286527488 false(reach) 5.023s 3.110s zeus06 215515136 0.924 0.889
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(reach) 23.721s 17.205s zeus22 690167808 false(reach) 5.774s 3.523s zeus07 231657472 0.991 1.000
ldv-regression/stateful_check_false-unreach-call.i false(reach) 7.883s 4.722s zeus22 286937088 rejected 7.944s 4.950s zeus24 257470464 1.000 1.000
ldv-regression/test_while_int.c_false-unreach-call.i false(reach) 6.869s 4.138s zeus16 282918912 false(reach) 4.519s 2.964s zeus24 208617472 1.000 1.000
ldv-regression/test_while_int.c_false-unreach-call_1.i false(reach) 5.453s 3.128s zeus17 277155840 false(reach) 4.439s 2.933s zeus06 213348352 1.000 1.000
loops/array_false-unreach-call.i false(reach) 6.012s 3.548s zeus12 244441088 false(reach) 4.423s 2.812s zeus02 209678336 1.000 1.000
loops/count_up_down_false-unreach-call_true-termination.i false(reach) 5.124s 3.084s zeus10 238436352 false(reach) 4.153s 2.633s zeus03 202981376 0.909 1.000
loops/eureka_01_false-unreach-call.i false(reach) 178.367s 152.217s zeus24 3604676608 false(reach) 6.624s 4.095s zeus11 270733312 1.000 1.000
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(reach) 7.141s 4.354s zeus14 285745152 false(reach) 4.280s 2.737s zeus23 205938688 1.000 1.000
loops/invert_string_false-unreach-call.i false(reach) 14.196s 9.324s zeus22 441274368 false(reach) 5.875s 3.889s zeus24 229396480 1.000 1.000
loops/matrix_false-unreach-call_true-termination.i false(reach) 7.309s 4.401s zeus01 278622208 false(reach) 6.799s 4.552s zeus11 604307456 1.000 1.000
loops/nec11_false-unreach-call.i false(reach) 5.340s 3.317s zeus21 237064192 false(reach) 3.894s 2.526s zeus06 202158080 0.889 0.667
loops/nec20_false-unreach-call.i false(reach) 5.503s 3.293s zeus07 249761792 false(reach) 4.693s 3.044s zeus04 212660224 1.000 1.000
loops/sum01_bug02_false-unreach-call_true-termination.i false(reach) 13.864s 8.951s zeus14 441417728 rejected 6.220s 3.852s zeus09 233172992 1.000 1.000
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(reach) 9.241s 5.458s zeus13 314314752 rejected 5.104s 3.254s zeus15 207626240 1.000 1.000
loops/sum01_false-unreach-call_true-termination.i false(reach) 17.662s 12.004s zeus14 441782272 rejected 5.909s 3.697s zeus23 228085760 1.000 1.000
loops/sum03_false-unreach-call_true-termination.i false(reach) 17.621s 11.782s zeus08 452001792 false(reach) 8.361s 5.286s zeus08 265666560 1.000 1.000
loops/sum04_false-unreach-call_true-termination.i false(reach) 7.643s 4.609s zeus09 289267712 false(reach) 4.681s 2.949s zeus20 207577088 1.000 1.000
loops/sum_array_false-unreach-call.i false(reach) 6.357s 3.736s zeus08 283942912 false(reach) 5.585s 3.578s zeus11 250302464 1.000 1.000
loops/terminator_01_false-unreach-call_false-termination.i false(reach) 5.841s 3.545s zeus16 245731328 false(reach) 3.825s 2.490s zeus11 206106624 0.889 1.000
loops/terminator_02_false-unreach-call_true-termination.i false(reach) 5.517s 3.397s zeus04 237543424 false(reach) 4.152s 2.596s zeus22 202534912 0.950 0.500
loops/terminator_03_false-unreach-call_true-termination.i false(reach) 5.516s 3.417s zeus22 249704448 false(reach) 4.077s 2.577s zeus20 203300864 0.909 1.000
loops/trex01_false-unreach-call_true-termination.i false(reach) 6.034s 3.639s zeus16 240701440 false(reach) 4.378s 2.700s zeus22 208814080 0.391 0.500
loops/trex02_false-unreach-call_true-termination.i false(reach) 5.522s 3.412s zeus05 240316416 false(reach) 4.120s 2.602s zeus22 205131776 0.833 0.667
loops/trex03_false-unreach-call_true-termination.i false(reach) 5.126s 3.165s zeus14 241860608 false(reach) 4.232s 2.657s zeus09 203698176 0.875 0.556
loops/verisec_NetBSD-libc__loop_false-unreach-call.i false(reach) 7.798s 4.519s zeus17 302260224 false(reach) 4.645s 3.040s zeus04 209317888 0.941 1.000
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i false(reach) 11.093s 6.679s zeus23 314585088 rejected 26.388s 17.236s zeus24 675504128 1.000 1.000
loops/vogal_false-unreach-call.i false(reach) 183.435s 153.876s zeus05 4425863168 false(reach) 11.129s 7.004s zeus04 303345664 1.000 1.000
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(reach) 6.058s 3.583s zeus16 237572096 false(reach) 4.055s 2.584s zeus23 201793536 0.929 1.000
loop-acceleration/diamond_false-unreach-call1.i false(reach) 221.254s 185.724s zeus08 3646042112 false(reach) 9.959s 6.327s zeus04 262356992 1.000 1.000
loop-acceleration/multivar_false-unreach-call1.i false(reach) 5.736s 3.430s zeus12 236310528 rejected 3.982s 2.499s zeus22 195993600 1.000 1.000
loop-acceleration/phases_false-unreach-call2.i false(reach) 5.356s 3.240s zeus23 241033216 false(reach) 4.115s 2.572s zeus05 201797632 0.929 0.750
loop-acceleration/simple_false-unreach-call2.i false(reach) 4.882s 2.948s zeus23 235270144 false(reach) 3.822s 2.456s zeus17 202633216 0.875 1.000
loop-acceleration/simple_false-unreach-call3.i false(reach) 5.529s 3.359s zeus08 234250240 false(reach) 3.877s 2.478s zeus23 199634944 0.889 1.000
loop-acceleration/underapprox_false-unreach-call1.i false(reach) 7.350s 4.402s zeus02 284844032 false(reach) 4.206s 2.670s zeus03 208896000 1.000 1.000
loop-acceleration/underapprox_false-unreach-call2.i false(reach) 7.200s 4.404s zeus07 279674880 false(reach) 4.147s 2.676s zeus07 210792448 1.000 1.000
loop-acceleration/diamond_true-unreach-call1.i false(reach) 822.096s 719.041s zeus24 3625435136 false(reach) 14.068s 9.403s zeus17 368480256 1.000 1.000
loop-acceleration/diamond_true-unreach-call2.i false(reach) 6.640s 3.881s zeus08 282324992 rejected 8.608s 5.144s zeus24 286666752 1.000 1.000
loop-invgen/id_trans_false-unreach-call.i false(reach) 6.851s 4.077s zeus01 283226112 false(reach) 4.339s 2.748s zeus24 204726272 1.000 1.000
product-lines/email_spec3_product13_false-unreach-call.cil.c false(reach) 454.853s 316.247s zeus09 6900903936 false(reach) 12.170s 6.938s zeus22 406122496 0.394 0.266
product-lines/email_spec3_product17_false-unreach-call.cil.c false(reach) 359.412s 261.199s zeus23 6794301440 false(reach) 13.047s 7.455s zeus14 408346624 0.402 0.282
product-lines/email_spec3_product18_false-unreach-call.cil.c false(reach) 653.235s 456.742s zeus02 8251002880 false(reach) 12.185s 7.054s zeus12 403427328 0.392 0.265
product-lines/email_spec3_product19_false-unreach-call.cil.c false(reach) 558.502s 395.411s zeus01 7306358784 false(reach) 12.411s 7.079s zeus22 404602880 0.392 0.265
product-lines/email_spec3_product23_false-unreach-call.cil.c false(reach) 589.005s 420.867s zeus15 7235424256 false(reach) 12.866s 7.420s zeus11 425160704 0.400 0.280
product-lines/email_spec3_product24_false-unreach-call.cil.c false(reach) 677.360s 480.937s zeus22 7826202624 false(reach) 12.910s 7.322s zeus07 415014912 0.390 0.264
product-lines/email_spec3_product25_false-unreach-call.cil.c false(reach) 594.102s 421.808s zeus07 7450845184 false(reach) 13.371s 7.614s zeus19 422748160 0.400 0.280
product-lines/email_spec3_product27_false-unreach-call.cil.c false(reach) 569.524s 407.665s zeus20 7667105792 false(reach) 12.682s 7.277s zeus22 417521664 0.398 0.279
product-lines/minepump_spec1_product33_false-unreach-call.cil.c false(reach) 11.273s 6.613s zeus12 318722048 false(reach) 6.969s 4.192s zeus20 252018688 0.357 0.545
product-lines/minepump_spec1_product34_false-unreach-call.cil.c false(reach) 17.673s 10.196s zeus08 451334144 false(reach) 7.318s 4.327s zeus20 260575232 0.359 0.545
product-lines/minepump_spec1_product35_false-unreach-call.cil.c false(reach) 12.130s 7.053s zeus09 325545984 false(reach) 7.372s 4.468s zeus15 254820352 0.368 0.559
product-lines/minepump_spec1_product36_false-unreach-call.cil.c false(reach) 12.024s 6.936s zeus24 324005888 false(reach) 6.909s 4.141s zeus17 258211840 0.360 0.529
product-lines/minepump_spec1_product37_false-unreach-call.cil.c false(reach) 12.800s 7.546s zeus24 331792384 false(reach) 7.566s 4.500s zeus23 260718592 0.375 0.571
product-lines/minepump_spec1_product38_false-unreach-call.cil.c false(reach) 15.668s 9.159s zeus13 453636096 false(reach) 7.758s 4.638s zeus11 265400320 0.377 0.571
product-lines/minepump_spec1_product39_false-unreach-call.cil.c false(reach) 12.606s 7.221s zeus14 322088960 false(reach) 7.510s 4.460s zeus14 261173248 0.382 0.583
product-lines/minepump_spec1_product40_false-unreach-call.cil.c false(reach) 15.924s 9.144s zeus24 328019968 false(reach) 7.875s 4.659s zeus10 260853760 0.377 0.556
product-lines/minepump_spec1_product41_false-unreach-call.cil.c false(reach) 13.769s 8.331s zeus19 448364544 false(reach) 8.008s 4.783s zeus20 278011904 0.368 0.559
product-lines/minepump_spec1_product42_false-unreach-call.cil.c false(reach) 21.082s 12.559s zeus18 460103680 false(reach) 8.093s 4.854s zeus24 281780224 0.370 0.559
product-lines/minepump_spec1_product43_false-unreach-call.cil.c false(reach) 21.866s 12.467s zeus04 463286272 false(reach) 8.513s 5.004s zeus09 276594688 0.379 0.571
product-lines/minepump_spec1_product44_false-unreach-call.cil.c false(reach) 21.494s 12.174s zeus05 462725120 false(reach) 8.136s 4.828s zeus13 278265856 0.371 0.543
product-lines/minepump_spec1_product49_false-unreach-call.cil.c false(reach) 14.634s 8.564s zeus05 341811200 false(reach) 7.192s 4.338s zeus06 263737344 0.383 0.583
product-lines/minepump_spec1_product50_false-unreach-call.cil.c false(reach) 13.092s 7.494s zeus19 351727616 false(reach) 7.522s 4.475s zeus20 260702208 0.384 0.583
product-lines/minepump_spec1_product51_false-unreach-call.cil.c false(reach) 14.439s 8.207s zeus21 326795264 false(reach) 7.375s 4.398s zeus02 263897088 0.390 0.595
product-lines/minepump_spec1_product52_false-unreach-call.cil.c false(reach) 12.878s 7.357s zeus06 328298496 false(reach) 7.383s 4.406s zeus22 267280384 0.385 0.568
product-lines/minepump_spec1_product53_false-unreach-call.cil.c false(reach) 26.154s 15.845s zeus15 357220352 false(reach) 8.208s 4.809s zeus22 273047552 0.396 0.605
product-lines/minepump_spec1_product54_false-unreach-call.cil.c false(reach) 12.937s 7.578s zeus18 359829504 false(reach) 8.031s 4.717s zeus05 270532608 0.398 0.605
product-lines/minepump_spec1_product55_false-unreach-call.cil.c false(reach) 12.988s 7.438s zeus13 323162112 false(reach) 8.005s 4.751s zeus12 272490496 0.403 0.615
product-lines/minepump_spec1_product56_false-unreach-call.cil.c false(reach) 14.809s 8.457s zeus24 337346560 false(reach) 8.129s 4.811s zeus16 273424384 0.398 0.590
product-lines/minepump_spec1_productSimulator_false-unreach-call.cil.c false(reach) 18.391s 10.322s zeus20 460652544 false(reach) 10.015s 5.831s zeus06 325742592 0.451 0.609
product-lines/minepump_spec2_product33_false-unreach-call.cil.c false(reach) 15.754s 9.425s zeus16 452067328 false(reach) 7.924s 4.724s zeus02 273022976 0.366 0.559
product-lines/minepump_spec2_product34_false-unreach-call.cil.c false(reach) 16.131s 9.391s zeus02 418086912 false(reach) 8.349s 4.928s zeus18 278618112 0.368 0.559
product-lines/minepump_spec2_product35_false-unreach-call.cil.c false(reach) 14.077s 8.090s zeus16 323399680 false(reach) 8.039s 4.770s zeus18 277057536 0.377 0.571
product-lines/minepump_spec2_product36_false-unreach-call.cil.c false(reach) 15.406s 8.735s zeus08 454365184 false(reach) 7.954s 4.758s zeus14 278282240 0.369 0.543
product-lines/minepump_spec2_product41_false-unreach-call.cil.c false(reach) 22.402s 13.214s zeus05 472657920 false(reach) 8.485s 5.075s zeus06 296689664 0.377 0.571
product-lines/minepump_spec2_product42_false-unreach-call.cil.c false(reach) 29.148s 16.224s zeus16 530366464 false(reach) 9.277s 5.501s zeus10 296890368 0.379 0.571
product-lines/minepump_spec2_product43_false-unreach-call.cil.c false(reach) 28.488s 16.347s zeus19 519688192 false(reach) 9.391s 5.640s zeus22 296763392 0.388 0.583
product-lines/minepump_spec2_product44_false-unreach-call.cil.c false(reach) 29.745s 17.471s zeus21 612040704 false(reach) 8.886s 5.224s zeus11 298565632 0.379 0.556
product-lines/minepump_spec2_productSimulator_false-unreach-call.cil.c false(reach) 30.743s 17.356s zeus22 546504704 false(reach) 12.064s 6.964s zeus12 389812224 0.458 0.617
product-lines/minepump_spec3_product01_false-unreach-call.cil.c false(reach) 7.682s 4.552s zeus09 287657984 false(reach) 6.870s 4.095s zeus08 248233984 0.330 0.467
product-lines/minepump_spec3_product02_false-unreach-call.cil.c false(reach) 14.138s 8.716s zeus15 306798592 false(reach) 6.569s 3.980s zeus22 249860096 0.332 0.467
product-lines/minepump_spec3_product03_false-unreach-call.cil.c false(reach) 8.292s 5.047s zeus12 297881600 false(reach) 6.755s 4.049s zeus22 252555264 0.342 0.484
product-lines/minepump_spec3_product04_false-unreach-call.cil.c false(reach) 9.017s 5.425s zeus21 314318848 false(reach) 7.077s 4.284s zeus10 250777600 0.333 0.452
product-lines/minepump_spec3_product05_false-unreach-call.cil.c false(reach) 7.976s 4.692s zeus14 311066624 false(reach) 6.838s 4.122s zeus17 247017472 0.348 0.500
product-lines/minepump_spec3_product06_false-unreach-call.cil.c false(reach) 8.927s 5.309s zeus01 311705600 false(reach) 6.716s 4.080s zeus01 248299520 0.351 0.500
product-lines/minepump_spec3_product07_false-unreach-call.cil.c false(reach) 8.366s 5.016s zeus09 312328192 false(reach) 8.524s 5.287s zeus04 249184256 0.355 0.515
product-lines/minepump_spec3_product08_false-unreach-call.cil.c false(reach) 10.024s 6.043s zeus15 313581568 false(reach) 7.027s 4.159s zeus20 249110528 0.357 0.515
product-lines/minepump_spec3_product09_false-unreach-call.cil.c false(reach) 8.141s 5.136s zeus12 288542720 false(reach) 7.223s 4.408s zeus04 240910336 0.327 0.452
product-lines/minepump_spec3_product10_false-unreach-call.cil.c false(reach) 8.549s 4.990s zeus14 308580352 false(reach) 6.639s 3.971s zeus22 250466304 0.329 0.452
product-lines/minepump_spec3_product11_false-unreach-call.cil.c false(reach) 9.318s 5.489s zeus21 314347520 false(reach) 6.912s 4.145s zeus10 250241024 0.339 0.469
product-lines/minepump_spec3_product12_false-unreach-call.cil.c false(reach) 9.414s 5.725s zeus01 319262720 false(reach) 7.486s 4.554s zeus04 247476224 0.330 0.438
product-lines/minepump_spec3_product13_false-unreach-call.cil.c false(reach) 7.585s 4.564s zeus20 304812032 false(reach) 7.030s 4.186s zeus17 247857152 0.345 0.485
product-lines/minepump_spec3_product14_false-unreach-call.cil.c false(reach) 9.302s 5.545s zeus08 310534144 false(reach) 7.086s 4.198s zeus17 248045568 0.348 0.485
product-lines/minepump_spec3_product15_false-unreach-call.cil.c false(reach) 8.543s 5.072s zeus24 313573376 false(reach) 7.074s 4.222s zeus20 252780544 0.352 0.500
product-lines/minepump_spec3_product16_false-unreach-call.cil.c false(reach) 10.314s 6.110s zeus08 311533568 false(reach) 6.937s 4.131s zeus11 255225856 0.354 0.500
product-lines/minepump_spec3_product17_false-unreach-call.cil.c false(reach) 10.023s 6.189s zeus15 312127488 false(reach) 6.770s 4.021s zeus13 253448192 0.357 0.515
product-lines/minepump_spec3_product18_false-unreach-call.cil.c false(reach) 9.459s 5.702s zeus16 314585088 false(reach) 7.385s 4.476s zeus22 254664704 0.359 0.515
product-lines/minepump_spec3_product19_false-unreach-call.cil.c false(reach) 8.485s 5.073s zeus24 314851328 false(reach) 7.073s 4.352s zeus04 254205952 0.363 0.529
product-lines/minepump_spec3_product20_false-unreach-call.cil.c false(reach) 9.433s 5.671s zeus08 311332864 false(reach) 7.172s 4.307s zeus02 253894656 0.365 0.529
product-lines/minepump_spec3_product21_false-unreach-call.cil.c false(reach) 9.567s 5.757s zeus21 310411264 false(reach) 6.945s 4.215s zeus24 261570560 0.371 0.543
product-lines/minepump_spec3_product22_false-unreach-call.cil.c false(reach) 9.258s 5.508s zeus14 312418304 false(reach) 7.442s 4.426s zeus09 260878336 0.373 0.543
product-lines/minepump_spec3_product23_false-unreach-call.cil.c false(reach) 9.563s 5.611s zeus24 311992320 false(reach) 7.234s 4.340s zeus17 256290816 0.377 0.556
product-lines/minepump_spec3_product24_false-unreach-call.cil.c false(reach) 9.864s 5.841s zeus09 311341056 false(reach) 7.198s 4.261s zeus18 260833280 0.379 0.556
product-lines/minepump_spec3_product25_false-unreach-call.cil.c false(reach) 7.892s 4.711s zeus21 306970624 false(reach) 7.350s 4.399s zeus11 255488000 0.354 0.500
product-lines/minepump_spec3_product26_false-unreach-call.cil.c false(reach) 9.991s 5.980s zeus03 313565184 false(reach) 6.907s 4.094s zeus20 251834368 0.356 0.500
product-lines/minepump_spec3_product27_false-unreach-call.cil.c false(reach) 9.806s 5.836s zeus14 312999936 false(reach) 6.813s 4.067s zeus05 250974208 0.360 0.514
product-lines/minepump_spec3_product28_false-unreach-call.cil.c false(reach) 9.916s 6.001s zeus03 313688064 false(reach) 7.095s 4.240s zeus19 259891200 0.362 0.514
product-lines/minepump_spec3_product29_false-unreach-call.cil.c false(reach) 8.683s 5.236s zeus04 312745984 false(reach) 7.289s 4.344s zeus10 255188992 0.368 0.528
product-lines/minepump_spec3_product30_false-unreach-call.cil.c false(reach) 8.831s 5.170s zeus07 315645952 false(reach) 7.206s 4.263s zeus23 262533120 0.370 0.528
product-lines/minepump_spec3_product31_false-unreach-call.cil.c false(reach) 9.045s 5.388s zeus07 311578624 false(reach) 7.643s 4.678s zeus04 256081920 0.374 0.541
product-lines/minepump_spec3_product32_false-unreach-call.cil.c false(reach) 8.538s 5.086s zeus14 307974144 false(reach) 7.258s 4.353s zeus18 261074944 0.376 0.541
product-lines/minepump_spec3_product35_false-unreach-call.cil.c false(reach) 9.018s 5.410s zeus22 313204736 false(reach) 6.997s 4.162s zeus14 253739008 0.366 0.543
product-lines/minepump_spec3_product36_false-unreach-call.cil.c false(reach) 8.946s 5.229s zeus18 306421760 false(reach) 7.143s 4.301s zeus21 251658240 0.369 0.543
product-lines/minepump_spec3_product39_false-unreach-call.cil.c false(reach) 8.908s 5.358s zeus03 301973504 false(reach) 7.077s 4.149s zeus14 255221760 0.384 0.568
product-lines/minepump_spec3_product40_false-unreach-call.cil.c false(reach) 9.363s 5.538s zeus21 314773504 false(reach) 7.405s 4.444s zeus23 268132352 0.386 0.568
product-lines/minepump_spec3_product43_false-unreach-call.cil.c false(reach) 10.073s 5.954s zeus01 313135104 false(reach) 7.026s 4.167s zeus24 257392640 0.377 0.556
product-lines/minepump_spec3_product44_false-unreach-call.cil.c false(reach) 9.836s 5.853s zeus16 312938496 false(reach) 6.855s 4.118s zeus11 256245760 0.379 0.556
product-lines/minepump_spec3_product47_false-unreach-call.cil.c false(reach) 8.830s 5.277s zeus02 306864128 false(reach) 7.412s 4.435s zeus09 259829760 0.389 0.579
product-lines/minepump_spec3_product48_false-unreach-call.cil.c false(reach) 9.261s 5.503s zeus20 311050240 false(reach) 7.323s 4.315s zeus13 258203648 0.391 0.579
product-lines/minepump_spec3_product51_false-unreach-call.cil.c false(reach) 9.966s 5.996s zeus01 306970624 false(reach) 7.548s 4.507s zeus23 260317184 0.391 0.579
product-lines/minepump_spec3_product52_false-unreach-call.cil.c false(reach) 10.131s 6.052s zeus19 310181888 false(reach) 7.564s 4.524s zeus19 265183232 0.393 0.579
product-lines/minepump_spec3_product55_false-unreach-call.cil.c false(reach) 9.226s 5.256s zeus19 311099392 false(reach) 8.129s 4.768s zeus09 268636160 0.404 0.600
product-lines/minepump_spec3_product56_false-unreach-call.cil.c false(reach) 9.230s 5.402s zeus23 313909248 false(reach) 7.940s 4.647s zeus14 268722176 0.406 0.600
product-lines/minepump_spec3_product59_false-unreach-call.cil.c false(reach) 9.546s 5.597s zeus24 305295360 false(reach) 7.749s 4.567s zeus16 259796992 0.401 0.590
product-lines/minepump_spec3_product60_false-unreach-call.cil.c false(reach) 17.984s 10.844s zeus15 313597952 false(reach) 8.252s 4.882s zeus15 271101952 0.403 0.590
product-lines/minepump_spec3_product63_false-unreach-call.cil.c false(reach) 10.430s 6.099s zeus19 313073664 false(reach) 7.961s 4.760s zeus22 273014784 0.409 0.610
product-lines/minepump_spec3_product64_false-unreach-call.cil.c false(reach) 9.498s 5.710s zeus20 315305984 false(reach) 8.281s 5.005s zeus15 273772544 0.411 0.610
product-lines/minepump_spec3_productSimulator_false-unreach-call.cil.c false(reach) 11.296s 6.644s zeus10 328544256 false(reach) 10.202s 5.872s zeus11 319897600 0.458 0.638
product-lines/minepump_spec4_product33_false-unreach-call.cil.c false(reach) 21.003s 13.443s zeus04 451694592 false(reach) 8.285s 4.924s zeus02 280899584 0.352 0.515
product-lines/minepump_spec4_product34_false-unreach-call.cil.c false(reach) 19.082s 12.175s zeus07 465850368 false(reach) 8.483s 5.075s zeus19 285716480 0.354 0.515
product-lines/minepump_spec4_product35_false-unreach-call.cil.c false(reach) 17.728s 10.590s zeus02 451747840 false(reach) 8.047s 4.915s zeus03 287412224 0.363 0.529
product-lines/minepump_spec4_product36_false-unreach-call.cil.c false(reach) 16.615s 9.814s zeus05 452481024 false(reach) 8.518s 5.021s zeus11 284397568 0.355 0.500
product-lines/minepump_spec4_product37_false-unreach-call.cil.c false(reach) 27.897s 16.446s zeus08 557842432 false(reach) 9.475s 5.701s zeus04 301350912 0.375 0.543
product-lines/minepump_spec4_product38_false-unreach-call.cil.c false(reach) 16.824s 10.203s zeus20 466915328 false(reach) 9.466s 5.536s zeus19 311164928 0.377 0.543
product-lines/minepump_spec4_product39_false-unreach-call.cil.c false(reach) 27.521s 16.298s zeus20 654950400 false(reach) 9.617s 5.692s zeus06 312291328 0.382 0.556
product-lines/minepump_spec4_product40_false-unreach-call.cil.c false(reach) 25.098s 14.778s zeus17 579899392 false(reach) 9.701s 5.597s zeus24 313352192 0.377 0.528
product-lines/minepump_spec4_product41_false-unreach-call.cil.c false(reach) 14.150s 8.788s zeus14 453033984 false(reach) 8.313s 4.916s zeus08 290504704 0.368 0.529
product-lines/minepump_spec4_product42_false-unreach-call.cil.c false(reach) 15.894s 9.801s zeus08 454758400 false(reach) 8.812s 5.129s zeus14 289288192 0.370 0.529
product-lines/minepump_spec4_product43_false-unreach-call.cil.c false(reach) 22.538s 13.890s zeus13 477282304 false(reach) 8.540s 5.065s zeus23 290988032 0.379 0.543
product-lines/minepump_spec4_product44_false-unreach-call.cil.c false(reach) 22.395s 13.321s zeus11 472899584 false(reach) 9.122s 5.428s zeus19 292085760 0.371 0.514
product-lines/minepump_spec4_product45_false-unreach-call.cil.c false(reach) 27.382s 15.787s zeus12 475918336 false(reach) 9.691s 5.725s zeus06 319590400 0.380 0.556
product-lines/minepump_spec4_product46_false-unreach-call.cil.c false(reach) 20.145s 11.938s zeus05 469024768 false(reach) 11.693s 6.988s zeus04 317411328 0.382 0.556
product-lines/minepump_spec4_product47_false-unreach-call.cil.c false(reach) 28.836s 16.819s zeus07 721956864 false(reach) 9.737s 5.696s zeus11 314224640 0.388 0.568
product-lines/minepump_spec4_product48_false-unreach-call.cil.c false(reach) 20.304s 12.112s zeus14 467402752 false(reach) 9.927s 5.857s zeus02 317300736 0.383 0.541
product-lines/minepump_spec4_productSimulator_false-unreach-call.cil.c false(reach) 28.144s 16.649s zeus15 562151424 false(reach) 13.275s 7.740s zeus03 446496768 0.451 0.587
systemc/kundu1_false-unreach-call_false-termination.cil.c false(reach) 52.688s 32.007s zeus05 1372086272 false(reach) 11.105s 6.637s zeus01 360345600 0.951 0.971
systemc/kundu2_false-unreach-call_false-termination.cil.c false(reach) 683.821s 469.117s zeus20 8064929792 false(reach) 12.685s 7.608s zeus03 388653056 0.983 1.000
systemc/pc_sfifo_1_false-unreach-call_false-termination.cil.c false(reach) 7.430s 4.430s zeus08 283451392 false(reach) 5.572s 3.409s zeus24 221863936 0.487 0.280
systemc/pc_sfifo_2_false-unreach-call_false-termination.cil.c false(reach) 19.776s 11.294s zeus01 464068608 false(reach) 6.261s 3.803s zeus22 236859392 0.570 0.471
systemc/token_ring.01_false-unreach-call_false-termination.cil.c false(reach) 27.221s 15.350s zeus03 733339648 false(reach) 8.005s 4.928s zeus15 268017664 0.875 0.825
systemc/token_ring.02_false-unreach-call_false-termination.cil.c false(reach) 45.000s 25.566s zeus18 1289945088 false(reach) 9.180s 5.547s zeus22 305410048 0.878 0.836
systemc/token_ring.03_false-unreach-call_false-termination.cil.c false(reach) 59.830s 37.053s zeus24 2474786816 false(reach) 11.059s 6.478s zeus23 346497024 0.879 0.843
systemc/token_ring.04_false-unreach-call_false-termination.cil.c false(reach) 88.687s 64.828s zeus16 4462067712 false(reach) 12.242s 7.193s zeus03 399929344 0.880 0.847
systemc/token_ring.05_false-unreach-call_false-termination.cil.c false(reach) 421.669s 329.429s zeus15 5920772096 false(reach) 13.886s 8.167s zeus24 452177920 0.881 0.850
systemc/toy1_false-unreach-call_false-termination.cil.c false(reach) 64.060s 40.920s zeus21 2477305856 false(reach) 11.209s 6.555s zeus02 344170496 0.945 0.928
systemc/toy2_false-unreach-call_false-termination.cil.c false(reach) 50.241s 29.572s zeus09 1798279168 false(reach) 10.997s 6.516s zeus24 343175168 0.943 0.926
systemc/transmitter.01_false-unreach-call_false-termination.cil.c false(reach) 22.030s 12.560s zeus09 453910528 false(reach) 6.601s 3.950s zeus14 247316480 0.860 0.774
systemc/transmitter.02_false-unreach-call_false-termination.cil.c false(reach) 32.900s 18.246s zeus04 745496576 false(reach) 7.578s 4.633s zeus06 279302144 0.879 0.826
systemc/transmitter.03_false-unreach-call_false-termination.cil.c false(reach) 54.361s 33.810s zeus09 2596712448 false(reach) 9.973s 5.962s zeus09 314732544 0.880 0.836
systemc/transmitter.04_false-unreach-call_false-termination.cil.c false(reach) 100.626s 73.149s zeus01 4632133632 false(reach) 11.463s 6.742s zeus22 365584384 0.881 0.842
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 60.991s 40.636s zeus18 1298771968 false(reach) 9.335s 5.472s zeus23 305135616 0.925 0.856
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 64.032s 41.988s zeus21 1296465920 false(reach) 9.414s 5.466s zeus13 298000384 0.925 0.854
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c false(reach) 115.708s 86.720s zeus03 3684818944 false(reach) 12.139s 7.128s zeus18 366612480 0.926 0.912
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c false(reach) 145.778s 110.778s zeus24 3633729536 false(reach) 10.595s 6.281s zeus22 338206720 0.925 0.911
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_2.ufo.BOUNDED-10.pals.c false(reach) 176.031s 137.552s zeus24 3724009472 false(reach) 12.111s 7.172s zeus17 373481472 0.910 0.856
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_2.ufo.UNBOUNDED.pals.c false(reach) 228.974s 183.859s zeus16 4449275904 false(reach) 11.297s 6.535s zeus09 344358912 0.910 0.854
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 248.644s 197.840s zeus08 4640288768 false(reach) 99.075s 82.973s zeus24 1519046656 0.989 1.000
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 222.599s 177.979s zeus11 4498853888 false(reach) 106.828s 90.518s zeus20 2539843584 0.989 1.000
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) 620.201s 521.685s zeus03 4822740992 false(reach) 133.595s 115.063s zeus04 2518110208 0.989 1.000
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 484.673s 401.444s zeus11 4927582208 false(reach) 100.541s 84.201s zeus23 2516692992 0.989 1.000
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 814.063s 566.973s zeus18 8611205120 false(reach) 9.260s 5.619s zeus06 315228160 0.912 0.846
seq-mthreaded/pals_lcr.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 864.741s 730.515s zeus11 5929271296 false(reach) 9.638s 5.837s zeus09 305340416 0.988 1.000
seq-mthreaded/rekh_ctm_false-unreach-call.3.c false(reach) 147.245s 110.405s zeus02 3805892608 timeout 1002.003s 852.085s zeus22 10231185408 - -
seq-mthreaded/rekh_ctm_true-unreach-call.1.c false(reach) 384.038s 323.805s zeus01 4595744768 timeout 961.622s 914.063s zeus08 8366522368 0.998 1.000
seq-mthreaded/rekh_ctm_true-unreach-call.3.c false(reach) 155.503s 116.834s zeus12 3801718784 timeout 1001.990s 846.602s zeus18 10221551616 - -
seq-mthreaded/rekh_ctm_true-unreach-call.4.c false(reach) 443.796s 382.998s zeus08 4620677120 timeout 912.733s 888.499s zeus16 7844892672 0.994 1.000
seq-pthread/cs_lazy_false-unreach-call.i false(reach) 153.257s 125.113s zeus10 3053142016 timeout 1000.342s 897.132s zeus12 7690129408 - -
seq-pthread/cs_read_write_lock_false-unreach-call.i false(reach) 502.402s 468.821s zeus02 2445467648 timeout 907.614s 889.278s zeus06 1115938816 0.845 0.606
seq-pthread/cs_stateful_false-unreach-call.i false(reach) 61.666s 43.800s zeus14 1301450752 timeout 914.596s 891.121s zeus05 5688819712 0.934 0.847
seq-pthread/cs_dekker_true-unreach-call.i false(reach) 55.208s 38.545s zeus08 1034133504 timeout 905.911s 887.787s zeus01 1015988224 0.785 0.475
seq-pthread/cs_fib_true-unreach-call.i false(reach) 341.249s 314.741s zeus06 4971552768 timeout 903.841s 886.150s zeus07 888000512 0.893 0.799
seq-pthread/cs_lamport_true-unreach-call.i false(reach) 115.009s 101.346s zeus10 776912896 timeout 905.767s 885.707s zeus08 997203968 0.694 0.355
seq-pthread/cs_peterson_true-unreach-call.i false(reach) 128.805s 111.585s zeus04 772620288 timeout 908.470s 886.992s zeus03 1018626048 0.832 0.524
seq-pthread/cs_read_write_lock_true-unreach-call.i false(reach) 787.037s 756.545s zeus03 3762266112 timeout 905.524s 888.385s zeus06 1084829696 0.847 0.614
seq-pthread/cs_stateful_true-unreach-call.i false(reach) 73.137s 51.644s zeus18 1309130752 timeout 915.563s 891.456s zeus03 5542813696 0.934 0.847
seq-pthread/cs_sync_true-unreach-call.i false(reach) 96.375s 73.871s zeus07 2380075008 timeout 1002.022s 871.145s zeus19 9637388288 - -
seq-pthread/cs_szymanski_true-unreach-call.i false(reach) 139.316s 120.657s zeus11 1296969728 timeout 904.859s 885.063s zeus24 995065856 0.750 0.390
seq-pthread/cs_time_var_mutex_true-unreach-call.i false(reach) 58.500s 40.841s zeus03 859701248 timeout 906.046s 884.617s zeus05 1226170368 0.852 0.606
ntdrivers/diskperf_false-unreach-call.i.cil.c false(reach) 22.916s 13.283s zeus01 505360384 false(reach) 16.455s 9.741s zeus14 635924480 0.833 0.637
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c false(reach) 16.447s 9.822s zeus18 373784576 false(reach) 9.368s 5.494s zeus02 302657536 0.979 0.812
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c false(reach) 19.204s 11.573s zeus12 470155264 false(reach) 9.857s 5.712s zeus01 309600256 0.979 0.802
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c false(reach) 21.791s 13.078s zeus02 473460736 false(reach) 9.335s 5.424s zeus16 307638272 0.979 0.802
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c false(reach) 19.516s 11.418s zeus11 471293952 false(reach) 10.029s 5.748s zeus14 304033792 0.979 0.802
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c false(reach) 555.558s 492.957s zeus18 3845308416 false(reach) 11.989s 6.913s zeus24 354398208 0.982 0.880
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c false(reach) 33.528s 21.573s zeus03 757059584 false(reach) 11.808s 6.743s zeus22 342831104 0.982 0.868
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c false(reach) 32.382s 20.489s zeus03 764252160 false(reach) 12.915s 7.406s zeus15 342261760 0.982 0.868
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c false(reach) 24.293s 14.329s zeus09 471207936 false(reach) 11.063s 6.511s zeus04 335556608 0.979 0.811
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c false(reach) 570.924s 507.762s zeus03 4455387136 false(reach) 11.644s 6.607s zeus11 346329088 0.982 0.870
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c false(reach) 36.742s 24.153s zeus19 791302144 false(reach) 11.762s 6.701s zeus23 347222016 0.982 0.868
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c false(reach) 551.997s 491.457s zeus01 4491509760 false(reach) 11.893s 6.804s zeus05 344358912 0.982 0.874
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c false(reach) 548.436s 486.768s zeus10 4465278976 false(reach) 12.364s 7.048s zeus09 349396992 0.982 0.877
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c false(reach) 555.435s 506.636s zeus21 4531892224 timeout 909.345s 877.370s zeus01 5850628096 0.983 0.962
../../sv-benchmarks/c/ status cputime walltime host memUsage status cputime walltime host memUsage Line coverage Condition coverage
total tasks 309 42806.529 34779.444 - 524098117632 309 90972.668 84272.417 - 609689608192 227.402 237.376
    correct results 294 38644.384 31116.475 - 485476962304 204 2181.014 1402.126 - 68007903232 132.527 142.289
        correct true 0 - - - - 0 - - - - - -
        correct false 294 38644.384 31116.475 - 485476962304 204 2181.014 1402.126 - 68007903232 132.527 142.289
    incorrect results 15 4162.145 3662.969 - 38621155328 1 14.068 9.403 - 368480256 1.000 1.000
        incorrect true 0 - - - - 0 - - - - - -
        incorrect false 15 4162.145 3662.969 - 38621155328 1 14.068 9.403 - 368480256 1.000 1.000
score (309 tasks, max score: 324) 204 - - - - 198 - - - - - -
Run set UltimateAutomizer Verification Predicate (LA) Validation