Tool CPAchecker 1.3.4-svn 13949
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 2
Host [cs-sel-05; cs-sel-06; db1; db2; db3; db4; db5; db6; db7; db8]
OS [Linux 3.13.0-36-generic; Linux 3.13.0-37-generic]
System CPU: [Intel Core i7-2600K @ 3.40 GHz; Intel Core i7-2600 @ 3.40 GHz] with 8 cores, frequency: 3.4 GHz; RAM: [16 GB; 33 GB]
Date of execution 14-10-16 18:16
Run set va_default__pred_sbe.DeviceDrivers64 va_domain__pred_sbe.DeviceDrivers64
Options -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -heap 12000M -skipRecursion -ldv -setprop analysis.checkCounterexamples=true -setprop counterexample.checker=CPACHECKER -setprop counterexample.checker.config=config/predicateAnalysis-as-bitprecise-cex-check.properties -setprop cpa.value.refiner.prefixPreference=DEFAULT -setprop cpa.predicate.blk.threshold=1 -setprop cpa.predicate.abstraction.computation=CARTESIAN -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -heap 12000M -skipRecursion -ldv -setprop analysis.checkCounterexamples=true -setprop counterexample.checker=CPACHECKER -setprop counterexample.checker.config=config/predicateAnalysis-as-bitprecise-cex-check.properties -setprop cpa.value.refiner.prefixPreference=DOMAIN_BEST_DEEP -setprop cpa.predicate.blk.threshold=1 -setprop cpa.predicate.abstraction.computation=CARTESIAN
Propertyfile ./benchmarks/slicedItp/svcomp14/ldv-consumption/ALL.prp
../benchmarks/slicedItp/svcomp14/ status cputime walltime host memUsage status cputime walltime host memUsage
ldv-linux-3.4-simple/32_1_cilled_true_ok_nondet_linux-3.4-32_1-drivers--auxdisplay--cfag12864b.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 891.415s 875.851s db5 4556447744 true 6.205s 3.633s db7 210894848
ldv-linux-3.4-simple/32_1_cilled_true_ok_nondet_linux-3.4-32_1-drivers--input--misc--apanel.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 911.131s 536.830s db7 12989919232 true 5.988s 3.517s cs-sel-05 169803776
ldv-linux-3.4-simple/43_1a_cilled_true_ok_nondet_linux-43_1a-drivers--staging--comedi--drivers--8255.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 929.970s 505.086s db8 13083598848 true 4.870s 2.991s db4 206315520
ldv-commit-tester/m0_false_drivers-scsi-gdth-ko--111_1a--5934df9-1.c out of memory 129.711s 98.882s db8 15000002560 timeout 930.027s 632.435s db8 13404254208
ldv-commit-tester/m0_true_drivers-media-video-cx88-cx88-blackbird-ko--32_7a--d47b389-1.c timeout 930.609s 492.939s cs-sel-05 13094174720 true 30.943s 20.852s db4 2554740736
ldv-commit-tester/m0_true_drivers-media-video-cx88-cx88-blackbird-ko--32_7a--d47b389.c timeout 929.757s 493.481s db2 13197357056 true 32.075s 21.322s db3 2879660032
ldv-commit-tester/main1_true_sound-oss-sound-ko--32_7a--c4cb1dd-1.c timeout 930.207s 536.011s cs-sel-06 12951064576 true 30.226s 16.620s db8 657035264
ldv-commit-tester/main1_true_sound-oss-sound-ko--32_7a--c4cb1dd.c timeout 930.148s 537.380s cs-sel-05 12903145472 true 29.089s 16.382s db4 752799744
ldv-consumption/32_7a_cilled_false_linux-3.8-rc1-drivers--hwmon--abituguru3.ko-main.cil.out.c timeout 930.066s 509.759s db6 13105332224 false(reach) 46.187s 34.011s db4 2003095552
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--block--paride--pf.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 929.722s 742.657s db2 10574766080 true 28.321s 17.054s db3 812621824
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--block--paride--pg.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 930.097s 690.658s db7 14471004160 true 12.704s 7.167s db6 243974144
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--block--paride--pt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 929.994s 524.276s db4 13176233984 true 26.808s 15.309s db3 740388864
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--hwmon--applesmc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 919.135s 509.083s db8 13096357888 true 23.651s 13.509s db4 722542592
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--infiniband--hw--cxgb3--iw_cxgb3.ko-ldv_main6_sequence_infinite_withcheck_stateful.cil.out.c timeout 930.101s 567.551s db8 12949733376 true 23.805s 12.979s db2 460226560
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--infiniband--hw--mlx4--mlx4_ib.ko-ldv_main4_sequence_infinite_withcheck_stateful.cil.out.c timeout 930.337s 555.627s db5 13049389056 true 29.909s 17.150s db8 797667328
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--isdn--hisax--hisax.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 902.140s 804.251s cs-sel-06 7074738176 true 56.376s 34.752s db7 1564626944
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--isdn--i4l--isdn.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c timeout 901.600s 852.580s db8 6712635392 true 74.509s 54.528s db3 4399042560
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--message--fusion--mptsas.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 912.378s 594.042s db1 12912680960 true 110.102s 95.704s db4 4485574656
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--misc--sgi-xp--xpc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 929.883s 504.272s db3 13408583680 true 18.779s 10.421s db3 427638784
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--mtd--ubi--ubi.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c timeout 907.395s 671.684s db3 9437597696 true 49.549s 33.049s cs-sel-05 1684582400
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--net--arcnet--com90xx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 903.751s 531.682s db4 12913033216 true 9.627s 5.394s db7 246231040
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--net--ethernet--i825xx--znet.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 929.814s 560.383s db3 13041795072 true 12.228s 6.811s db3 282836992
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--net--ethernet--qlogic--qlge--qlge.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 930.060s 575.903s db4 12537708544 true 132.082s 98.922s db2 4935958528
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 930.084s 559.061s db4 12944859136 true 82.324s 59.578s db7 4097384448
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c timeout 930.017s 522.200s db6 13105192960 true 58.806s 39.160s db7 2547978240
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c timeout 904.334s 744.865s db6 11825356800 true 73.957s 54.066s db3 3757481984
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--net--usb--hso.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 901.492s 829.495s db5 8205422592 true 15.519s 8.566s db4 398065664
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--parport--parport_pc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 930.005s 543.534s db3 13003100160 true 47.758s 36.217s db3 4332679168
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--platform--x86--samsung-laptop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 930.048s 544.414s db6 13019983872 true 23.173s 14.200s db3 1721458688
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--staging--speakup--speakup.ko-ldv_main4_sequence_infinite_withcheck_stateful.cil.out.c timeout 930.078s 496.503s db7 12879441920 true 34.765s 19.998s db8 818458624
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--tty--mxser.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 901.178s 810.739s db6 6308376576 true 19.621s 10.741s db7 428183552
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--video--aty--radeonfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 930.072s 548.174s db7 13086674944 true 37.698s 23.314s db3 1761837056
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--video--smscufx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c out of memory 797.530s 595.238s db3 15000002560 timeout 904.606s 788.449s db4 8718168064
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-drivers--video--via--viafb.ko-ldv_main12_sequence_infinite_withcheck_stateful.cil.out.c timeout 911.491s 544.453s db4 13067980800 true 29.083s 16.352s db4 716996608
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c timeout 930.019s 498.837s db3 13291290624 true 26.264s 14.798s db6 1233747968
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-kernel--rcutorture.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 930.093s 541.255s db7 13155876864 true 20.339s 11.601s db3 705363968
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-lib--rbtree_test.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 930.020s 588.780s db7 13173997568 true 7.874s 4.497s db7 221609984
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c timeout 930.182s 541.251s db3 12931375104 true 31.917s 17.024s db7 716193792
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-drivers--block--paride--pg.ko-main.cil.out.c timeout 930.228s 714.779s db4 14469165056 true 12.460s 6.975s db1 255897600
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-drivers--gpu--drm--gma500--gma500_gfx.ko-main.cil.out.c timeout 930.300s 576.264s db1 13113839616 true 107.589s 75.380s db7 4001247232
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-drivers--hwmon--w83781d.ko-main.cil.out.c timeout 907.215s 704.379s db8 10102693888 true 580.054s 477.216s db3 7628476416
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-drivers--infiniband--hw-cxgb3--iw_cxgb3.ko-main.cil.out.c timeout 922.919s 559.865s db2 12990128128 true 20.681s 11.112s db8 455905280
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-drivers--isdn--mISDN--l1oip.ko-main.cil.out.c timeout 901.026s 866.925s db5 5636698112 true 10.772s 6.105s db2 248635392
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-drivers--mfd--sm501.ko-main.cil.out.c timeout 929.968s 790.449s db8 8580157440 true 13.935s 7.750s db4 245755904
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-drivers--misc--sgi-xp--xpc.ko-main.cil.out.c timeout 930.233s 503.764s db1 13348417536 true 22.790s 12.877s cs-sel-05 634052608
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-drivers--net--ethernet--chelsio--cxgb4--cxgb4.ko-main.cil.out.c timeout 930.030s 537.772s db8 13054713856 true 78.793s 53.090s db6 3203063808
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-drivers--net--ethernet--qlogic--qlge--qlge.ko-main.cil.out.c timeout 930.010s 566.638s db7 13162442752 true 155.355s 114.060s db6 5126529024
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-drivers--staging--silicom--bpctl_mod.ko-main.cil.out.c timeout 929.687s 554.178s db2 13274468352 true 61.401s 40.747s cs-sel-05 1980837888
ldv-consumption/32_7a_cilled_true_linux-3.8-rc1-drivers--video--aty--radeonfb.ko-main.cil.out.c timeout 930.144s 547.466s db3 13140918272 true 66.194s 48.112s db6 3884773376
../benchmarks/slicedItp/svcomp14/ status cputime walltime host memUsage status cputime walltime host memUsage
total files 49 44287.822 29102.146 - 592109875200 49 4267.789 3146.502 - 104483295232
correct results 0 - - - - 47 2433.156 1725.618 - 82360872960
false negatives 0 - - - - 0 - - - -
false positives 0 - - - - 0 - - - -
false properties 0 - - - - 0 - - - -
score (49 files, max score: 96) 0 - - - - 93 - - - -
Run set va_default__pred_sbe.DeviceDrivers64 va_domain__pred_sbe.DeviceDrivers64